[urbit] whitepaper question: [%meta vase]

[Bayle Shanks]

Hi, I'm reading thru section "Moves and ducts" of the whitepaper,
http://urbit.org/docs/theory/whitepaper#-moves-and-ducts

I think I understand most everything in that section except the following
paragraph, which I don't understand:

"One card structure that Arvo detects and automatically unwraps is [%meta
vase] - where the vase is the vase of a card. %meta can be stacked up
indefinitely. The result is that vanes themselves can operate internally at
the vase level - dynamically executing code just as Arvo itself does."

Would anyone be interested in explaining that paragraph to me? I think i
just need a wholesale re-explanation of the entire paragraph, but if you
want specific questions: (a) so the construct under discussion means that,
in some place where a card is expected and you have a card, instead of
providing that card, you provide "[%meta [span card]]", where 'span' is the
'span' of card, right? (b) what is the semantics of this, that is, what
does Arvo do differently when it sees [%meta vase] where it expected a
card? (c) perhaps the semantics is to 'quote' the vase of card? i don't see
why you'd need to do that, though (d) so is it correct for me to think of
this as a 'wrapper', in the same sense that Haskell's 'Maybe' "wraps" a
value with either "Just" or "Nothing"? (e) at what point does Arvo
'automatically unwrap' the %meta wrapper, and why is this important (and
why don't the vanes unwrap it themselves)? (f) what does it mean for a vane
to operate "at the vase level"; a vase is just a noun tagged with its span,
right? (g) how does adding this assist vanes to dynamically execute code?
(h) in the absence of %meta, wouldn't vanes already be able to dynamically
execute code just by using Nock instruction 2?

thanks,
bayle

[Anton Dyudin]

The concern here is type-checking:

a) yes.
b) normally, type safety is assured by using the [span noun] produced by
the first vane as the input span of the second vane.
e) For %meta however, the dynamically produced span in the card is used
instead, allowing one vane's vase-of-output to be type-checked against
another vane's input (h) which normal hoon code cannot do: you can .*, i.e.
nock 2, whatever you want, but the output static type is
(necessarily) noun.
(f) If you want to operate on this noun, you either have to revalidate that
it fits the desired type (prohibitively slow, except for things like "atom"
and "list of a dozen atoms"), or slam it against a gate that is itself a
vase, receiving once again a pair [span untyped-noun] as a result. This is
like (d) a wrapper, except you can never unwrap it properly; except, that
is, if (e) the code acting on the vase is itself in a vase, in which case
the outer layer can notice it received a [span [%meta cell]], and use the
cell as the [span value] for the next call.
(c) Thus, if the vase is considered a "quoted" value, %meta signals a
request for type-level eval. This way, the vast majority of code can be
written to operate on well-typed values, and the occasional place where
hoon is compiled and run can take the resulting vase-of-a-move, send it to
arvo, and have it arrive with the same type as a normal move produced by
the vane directly.

Post by Bayle Shanks
Hi, I'm reading thru section "Moves and ducts" of the whitepaper,
http://urbit.org/docs/theory/whitepaper#-moves-and-ducts
I think I understand most everything in that section except the following
"One card structure that Arvo detects and automatically unwraps is [%meta
vase] - where the vase is the vase of a card. %meta can be stacked up
indefinitely. The result is that vanes themselves can operate internally at
the vase level - dynamically executing code just as Arvo itself does."
Would anyone be interested in explaining that paragraph to me? I think i
just need a wholesale re-explanation of the entire paragraph, but if you
want specific questions: (a) so the construct under discussion means that,
in some place where a card is expected and you have a card, instead of
providing that card, you provide "[%meta [span card]]", where 'span' is the
'span' of card, right? (b) what is the semantics of this, that is, what
does Arvo do differently when it sees [%meta vase] where it expected a
card? (c) perhaps the semantics is to 'quote' the vase of card? i don't see
why you'd need to do that, though (d) so is it correct for me to think of
this as a 'wrapper', in the same sense that Haskell's 'Maybe' "wraps" a
value with either "Just" or "Nothing"? (e) at what point does Arvo
'automatically unwrap' the %meta wrapper, and why is this important (and
why don't the vanes unwrap it themselves)? (f) what does it mean for a vane
to operate "at the vase level"; a vase is just a noun tagged with its span,
right? (g) how does adding this assist vanes to dynamically execute code?
(h) in the absence of %meta, wouldn't vanes already be able to dynamically
execute code just by using Nock instruction 2?
thanks,
bayle
--
You received this message because you are subscribed to the Google Groups "urbit" group.
To unsubscribe from this group and stop receiving emails from it, send an
For more options, visit https://groups.google.com/d/optout.

...

[Curtis Yarvin]

What Anton said is correct, but let me put it slightly differently.

Suppose you have a function that makes foobars. It makes them in the
normal, healthy, statically typed way by returning a foobar.

Now suppose you have another function that makes foobars, but does it
by running a piece of code that some user typed in. Dynamic type in
Urbit means you run the compiler at runtime, basically. You can even
check that the user's code produces a foobar, because you can call the
type system on it - eg, (~(nest ut -:!>(*foobar)) & myspan).

But you still have a vase, which is not a foobar, but a cell [span
noun]. Hoon does not have dependent types and cannot statically
enforce a correct vase. And there is no way for statically typed code
to turn a vase of foobar into a foobar.

The foobar in this case is a move. If a vane wants to delegate the
task of producing moves to user-level code, the best it can do is
build a vase which it knows (non-statically) to be correct. But it
can't turn the vase of a move into a move, any more than it can turn
the vase of a foobar into a foobar.

But the Arvo kernel itself treats vanes as user-level code in this
sense -- the vane core is literally stored as a vase. So all we have
to do is return the vase of a move (with %meta), and than use what
would ordinarily be a *vase of a vase of a move* into a plain old vase
of a move. This requires the Arvo kernel to do things like using Nock
directly to call type-checking routines on plain nouns. Actually,
this is perfectly safe, we just don't have the power to verify that
it's perfectly safe.

This has to be n levels deep because it has to be at least 2 levels
deep - since `%gall` is a vase which runs the `:dojo` app, which runs
user-level code.

Points for noting this -- it should be fleshed out in a little more
detail. It's definitely one of the most rocket sciency things we do.
I hate rocket science and everyone else should too.

Post by Anton Dyudin
a) yes.
b) normally, type safety is assured by using the [span noun] produced by the
first vane as the input span of the second vane.
e) For %meta however, the dynamically produced span in the card is used
instead, allowing one vane's vase-of-output to be type-checked against
another vane's input (h) which normal hoon code cannot do: you can .*, i.e.
nock 2, whatever you want, but the output static type is (necessarily)
noun.
(f) If you want to operate on this noun, you either have to revalidate that
it fits the desired type (prohibitively slow, except for things like "atom"
and "list of a dozen atoms"), or slam it against a gate that is itself a
vase, receiving once again a pair [span untyped-noun] as a result. This is
like (d) a wrapper, except you can never unwrap it properly; except, that
is, if (e) the code acting on the vase is itself in a vase, in which case
the outer layer can notice it received a [span [%meta cell]], and use the
cell as the [span value] for the next call.
(c) Thus, if the vase is considered a "quoted" value, %meta signals a
request for type-level eval. This way, the vast majority of code can be
written to operate on well-typed values, and the occasional place where hoon
is compiled and run can take the resulting vase-of-a-move, send it to arvo,
and have it arrive with the same type as a normal move produced by the vane
directly.

Post by Bayle Shanks
Hi, I'm reading thru section "Moves and ducts" of the whitepaper,
http://urbit.org/docs/theory/whitepaper#-moves-and-ducts
I think I understand most everything in that section except the following
"One card structure that Arvo detects and automatically unwraps is [%meta
vase] - where the vase is the vase of a card. %meta can be stacked up
indefinitely. The result is that vanes themselves can operate internally at
the vase level - dynamically executing code just as Arvo itself does."
Would anyone be interested in explaining that paragraph to me? I think i
just need a wholesale re-explanation of the entire paragraph, but if you
want specific questions: (a) so the construct under discussion means that,
in some place where a card is expected and you have a card, instead of
providing that card, you provide "[%meta [span card]]", where 'span' is the
'span' of card, right? (b) what is the semantics of this, that is, what does
Arvo do differently when it sees [%meta vase] where it expected a card? (c)
perhaps the semantics is to 'quote' the vase of card? i don't see why you'd
need to do that, though (d) so is it correct for me to think of this as a
'wrapper', in the same sense that Haskell's 'Maybe' "wraps" a value with
either "Just" or "Nothing"? (e) at what point does Arvo 'automatically
unwrap' the %meta wrapper, and why is this important (and why don't the
vanes unwrap it themselves)? (f) what does it mean for a vane to operate "at
the vase level"; a vase is just a noun tagged with its span, right? (g) how
does adding this assist vanes to dynamically execute code? (h) in the
absence of %meta, wouldn't vanes already be able to dynamically execute code
just by using Nock instruction 2?
thanks,
bayle
--
You received this message because you are subscribed to the Google Groups "urbit" group.
To unsubscribe from this group and stop receiving emails from it, send an
For more options, visit https://groups.google.com/d/optout.

--
Cabmold delenda est
--
You received this message because you are subscribed to the Google Groups "urbit" group.
To unsubscribe from this group and stop receiving emails from it, send an
For more options, visit https://groups.google.com/d/optout.

...

[Bayle Shanks]

Okay, thank you both, it's a little clearer now, although i still have some
followup questions.

1) So my understanding from your replies is that a %meta wrapper occurs for
something whose type cannot be statically known, and its function is to
engage some sort of alternate form of type-checking or type-casting. Arvo
checks for a %meta and if it sees one, it engages the alternative
typechecking/casting and then unwraps the %meta, passing on the wrapped
value in its place. Is this correct?

2) Moves vs. cards: Both of you speak of a vase of a move, but the
whitepaper says "[%meta vase] - where the vase is the vase of a card". So
is the vase the vase of a move, or the vase of a card? Or are all cards
moves? Or are all moves cards? Upon further reflection, i see that the
whitepaper never defines exactly what data a move contains, nor the exact
relationship between moves and cards; it just says "A move has a duct,
which is a list a wires, each of which is analagous to a stack frame"; so
does a move contain any data besides a duct?

3) Why are vases sent even when %meta is absent: The whitepaper says,
"...Arvo manages both vanes and moves as vases, [span noun] cells. Every
dispatch is type-checked". Does this mean that typically, every move is
statically typechecked via the usual Hoon mechanisms, and that these
mechanisms are overridden in the case of %meta (like a C typecast)? But if
that were the case, why would the typical case need vases at all? Is the
concept of a 'vase' something Arvo is adding here, or are vases always
required for typechecking in Hoon? That is, does Hoon require every value
to be explictly passed around within a vase in order for it to typecheck
that value? For example, if i want to pass around "[3 3]", and i want Hoon
to recognize that this is in fact a pair of atoms, then must i explicitly
pass it as "[span [3 3]]" where 'span' is the span indicating pairs of
atoms? I would have assumed that either the type of values was checked at
compile-time (like in the language C), or alternately that the type tag
(the span, in this case) was hidden from the programmer by the runtime
(like many interpreted languages) so that internally the value would be
(pair-of-atoms, [3 3]) but the programmer sees it as just [3 3]?

4) Is the type being 'revalidated' even though that is 'prohibitively
slow', or is the sender being trusted to give the correct span, or
something else: Anton says, "If you want to operate on this noun, you
either have to revalidate that it fits the desired type (prohibitively
slow, except for things like "atom" and "list of a dozen atoms"), or slam
it against a gate that is itself a vase," and Curtis says, "And there is no
way for statically typed code to turn a vase of foobar into a foobar....it
can't turn the vase of a move into a move, any more than it can turn the
vase of a foobar into a foobar...This requires the Arvo kernel to do things
like using Nock directly to call type-checking routines on plain nouns.".
So are you saying that (a) when %meta is seen, at runtime the enclosed card
(or move?) is dynamically typechecked against the enclosed span to make
sure it is of the claimed type, despite the prohibitive slowness mentioned
by Anton, and then if it passes the check, Hoon is instructed to typecast?
Or, alternately, (b) is Arvo just assuming that the provided span is
correct without checking it, and instructs Hoon to typecast? Or is neither
(a) nor (b) correct?

thanks,
b

[Raymond Pasco]

A move contains a duct (its event-stack context) and some interesting data
(a "card").

Yours,
r

[Anton Dyudin]

1. Yes
3. Vases are always required for type-checking, or more specifically spans
are. /normally/, when you pass round a value, its type has already been
checked; however, in communication between vanes (or between a vased core
in a vane and the vane itself), this is done on every call(and then
memoized). Internally to the vane, the type tag is usually hidden, since
the output of slamming a vase of a move against a gate at an arm in a vase
of a core is also a vase.
4. By "revalidated" I meant calling a clam on a noun to ensure the noun
fits in the(clam's) span. What actually happens in (a) is that the type
checker is run against the /spans/ of the input and target. The span in
%meta is assumed to be correct, yes, having been provided directly by a
vane in a series of safety-preserving operations on vases: the first, of
course, being baked-in constant !>s and/or [%noun foo], followed by
dynamically compiling and executing twigs of various sorts.

Post by Bayle Shanks
Okay, thank you both, it's a little clearer now, although i still have
some followup questions.
1) So my understanding from your replies is that a %meta wrapper occurs
for something whose type cannot be statically known, and its function is to
engage some sort of alternate form of type-checking or type-casting. Arvo
checks for a %meta and if it sees one, it engages the alternative
typechecking/casting and then unwraps the %meta, passing on the wrapped
value in its place. Is this correct?
2) Moves vs. cards: Both of you speak of a vase of a move, but the
whitepaper says "[%meta vase] - where the vase is the vase of a card". So
is the vase the vase of a move, or the vase of a card? Or are all cards
moves? Or are all moves cards? Upon further reflection, i see that the
whitepaper never defines exactly what data a move contains, nor the exact
relationship between moves and cards; it just says "A move has a duct,
which is a list a wires, each of which is analagous to a stack frame"; so
does a move contain any data besides a duct?
3) Why are vases sent even when %meta is absent: The whitepaper says,
"...Arvo manages both vanes and moves as vases, [span noun] cells. Every
dispatch is type-checked". Does this mean that typically, every move is
statically typechecked via the usual Hoon mechanisms, and that these
mechanisms are overridden in the case of %meta (like a C typecast)? But if
that were the case, why would the typical case need vases at all? Is the
concept of a 'vase' something Arvo is adding here, or are vases always
required for typechecking in Hoon? That is, does Hoon require every value
to be explictly passed around within a vase in order for it to typecheck
that value? For example, if i want to pass around "[3 3]", and i want Hoon
to recognize that this is in fact a pair of atoms, then must i explicitly
pass it as "[span [3 3]]" where 'span' is the span indicating pairs of
atoms? I would have assumed that either the type of values was checked at
compile-time (like in the language C), or alternately that the type tag
(the span, in this case) was hidden from the programmer by the runtime
(like many interpreted languages) so that internally the value would be
(pair-of-atoms, [3 3]) but the programmer sees it as just [3 3]?
4) Is the type being 'revalidated' even though that is 'prohibitively
slow', or is the sender being trusted to give the correct span, or
something else: Anton says, "If you want to operate on this noun, you
either have to revalidate that it fits the desired type (prohibitively
slow, except for things like "atom" and "list of a dozen atoms"), or slam
it against a gate that is itself a vase," and Curtis says, "And there is no
way for statically typed code to turn a vase of foobar into a foobar....it
can't turn the vase of a move into a move, any more than it can turn the
vase of a foobar into a foobar...This requires the Arvo kernel to do things
like using Nock directly to call type-checking routines on plain nouns.".
So are you saying that (a) when %meta is seen, at runtime the enclosed card
(or move?) is dynamically typechecked against the enclosed span to make
sure it is of the claimed type, despite the prohibitive slowness mentioned
by Anton, and then if it passes the check, Hoon is instructed to typecast?
Or, alternately, (b) is Arvo just assuming that the provided span is
correct without checking it, and instructs Hoon to typecast? Or is neither
(a) nor (b) correct?
thanks,
b
--
You received this message because you are subscribed to the Google Groups "urbit" group.
To unsubscribe from this group and stop receiving emails from it, send an
.
For more options, visit https://groups.google.com/d/optout.

...

[Anton Dyudin]

To expand on the last sentence of 3, arvo has the vane as a vase, therefore
when arvo e.g. passes unix events to the vane it does so as a
vase(span %noun) and received the response as a vase, can then send the
moves in the response to other vanes as vases, etc.; as far as the vane(and
execution of any nock in the compiled core of the vane) is concerned, it
just got passed a well-typed card. But before execution occurs, the span of
the card is first checked against the vane(and then discarded), this being
the dynamic "compile time".

Post by Anton Dyudin
1. Yes
3. Vases are always required for type-checking, or more specifically spans
are. /normally/, when you pass round a value, its type has already been
checked; however, in communication between vanes (or between a vased core
in a vane and the vane itself), this is done on every call(and then
memoized). Internally to the vane, the type tag is usually hidden, since
the output of slamming a vase of a move against a gate at an arm in a vase
of a core is also a vase.
4. By "revalidated" I meant calling a clam on a noun to ensure the noun
fits in the(clam's) span. What actually happens in (a) is that the type
checker is run against the /spans/ of the input and target. The span in
%meta is assumed to be correct, yes, having been provided directly by a
vane in a series of safety-preserving operations on vases: the first, of
course, being baked-in constant !>s and/or [%noun foo], followed by
dynamically compiling and executing twigs of various sorts.

Post by Bayle Shanks
Okay, thank you both, it's a little clearer now, although i still have
some followup questions.
1) So my understanding from your replies is that a %meta wrapper occurs
for something whose type cannot be statically known, and its function is to
engage some sort of alternate form of type-checking or type-casting. Arvo
checks for a %meta and if it sees one, it engages the alternative
typechecking/casting and then unwraps the %meta, passing on the wrapped
value in its place. Is this correct?
2) Moves vs. cards: Both of you speak of a vase of a move, but the
whitepaper says "[%meta vase] - where the vase is the vase of a card". So
is the vase the vase of a move, or the vase of a card? Or are all cards
moves? Or are all moves cards? Upon further reflection, i see that the
whitepaper never defines exactly what data a move contains, nor the exact
relationship between moves and cards; it just says "A move has a duct,
which is a list a wires, each of which is analagous to a stack frame"; so
does a move contain any data besides a duct?
3) Why are vases sent even when %meta is absent: The whitepaper says,
"...Arvo manages both vanes and moves as vases, [span noun] cells. Every
dispatch is type-checked". Does this mean that typically, every move is
statically typechecked via the usual Hoon mechanisms, and that these
mechanisms are overridden in the case of %meta (like a C typecast)? But if
that were the case, why would the typical case need vases at all? Is the
concept of a 'vase' something Arvo is adding here, or are vases always
required for typechecking in Hoon? That is, does Hoon require every value
to be explictly passed around within a vase in order for it to typecheck
that value? For example, if i want to pass around "[3 3]", and i want Hoon
to recognize that this is in fact a pair of atoms, then must i explicitly
pass it as "[span [3 3]]" where 'span' is the span indicating pairs of
atoms? I would have assumed that either the type of values was checked at
compile-time (like in the language C), or alternately that the type tag
(the span, in this case) was hidden from the programmer by the runtime
(like many interpreted languages) so that internally the value would be
(pair-of-atoms, [3 3]) but the programmer sees it as just [3 3]?
4) Is the type being 'revalidated' even though that is 'prohibitively
slow', or is the sender being trusted to give the correct span, or
something else: Anton says, "If you want to operate on this noun, you
either have to revalidate that it fits the desired type (prohibitively
slow, except for things like "atom" and "list of a dozen atoms"), or slam
it against a gate that is itself a vase," and Curtis says, "And there is no
way for statically typed code to turn a vase of foobar into a foobar....it
can't turn the vase of a move into a move, any more than it can turn the
vase of a foobar into a foobar...This requires the Arvo kernel to do things
like using Nock directly to call type-checking routines on plain nouns.".
So are you saying that (a) when %meta is seen, at runtime the enclosed card
(or move?) is dynamically typechecked against the enclosed span to make
sure it is of the claimed type, despite the prohibitive slowness mentioned
by Anton, and then if it passes the check, Hoon is instructed to typecast?
Or, alternately, (b) is Arvo just assuming that the provided span is
correct without checking it, and instructs Hoon to typecast? Or is neither
(a) nor (b) correct?
thanks,
b
--
You received this message because you are subscribed to the Google Groups "urbit" group.
To unsubscribe from this group and stop receiving emails from it, send an
For more options, visit https://groups.google.com/d/optout.

--
Cabmold delenda est

...

[Bayle Shanks]

Thank you all for your help!

Post by Anton Dyudin
To expand on the last sentence of 3, arvo has the vane as a vase,
therefore when arvo e.g. passes unix events to the vane it does so as a
vase(span %noun) and received the response as a vase, can then send the
moves in the response to other vanes as vases, etc.; as far as the vane(and
execution of any nock in the compiled core of the vane) is concerned, it
just got passed a well-typed card. But before execution occurs, the span of
the card is first checked against the vane(and then discarded), this being
the dynamic "compile time".

Post by Anton Dyudin
1. Yes
3. Vases are always required for type-checking, or more specifically
spans are. /normally/, when you pass round a value, its type has already
been checked; however, in communication between vanes (or between a vased
core in a vane and the vane itself), this is done on every call(and then
memoized). Internally to the vane, the type tag is usually hidden, since
the output of slamming a vase of a move against a gate at an arm in a vase
of a core is also a vase.
4. By "revalidated" I meant calling a clam on a noun to ensure the noun
fits in the(clam's) span. What actually happens in (a) is that the type
checker is run against the /spans/ of the input and target. The span in
%meta is assumed to be correct, yes, having been provided directly by a
vane in a series of safety-preserving operations on vases: the first, of
course, being baked-in constant !>s and/or [%noun foo], followed by
dynamically compiling and executing twigs of various sorts.

Post by Bayle Shanks
Okay, thank you both, it's a little clearer now, although i still have
some followup questions.
1) So my understanding from your replies is that a %meta wrapper occurs
for something whose type cannot be statically known, and its function is to
engage some sort of alternate form of type-checking or type-casting. Arvo
checks for a %meta and if it sees one, it engages the alternative
typechecking/casting and then unwraps the %meta, passing on the wrapped
value in its place. Is this correct?
2) Moves vs. cards: Both of you speak of a vase of a move, but the
whitepaper says "[%meta vase] - where the vase is the vase of a card". So
is the vase the vase of a move, or the vase of a card? Or are all cards
moves? Or are all moves cards? Upon further reflection, i see that the
whitepaper never defines exactly what data a move contains, nor the exact
relationship between moves and cards; it just says "A move has a duct,
which is a list a wires, each of which is analagous to a stack frame"; so
does a move contain any data besides a duct?
3) Why are vases sent even when %meta is absent: The whitepaper says,
"...Arvo manages both vanes and moves as vases, [span noun] cells. Every
dispatch is type-checked". Does this mean that typically, every move is
statically typechecked via the usual Hoon mechanisms, and that these
mechanisms are overridden in the case of %meta (like a C typecast)? But if
that were the case, why would the typical case need vases at all? Is the
concept of a 'vase' something Arvo is adding here, or are vases always
required for typechecking in Hoon? That is, does Hoon require every value
to be explictly passed around within a vase in order for it to typecheck
that value? For example, if i want to pass around "[3 3]", and i want Hoon
to recognize that this is in fact a pair of atoms, then must i explicitly
pass it as "[span [3 3]]" where 'span' is the span indicating pairs of
atoms? I would have assumed that either the type of values was checked at
compile-time (like in the language C), or alternately that the type tag
(the span, in this case) was hidden from the programmer by the runtime
(like many interpreted languages) so that internally the value would be
(pair-of-atoms, [3 3]) but the programmer sees it as just [3 3]?
4) Is the type being 'revalidated' even though that is 'prohibitively
slow', or is the sender being trusted to give the correct span, or
something else: Anton says, "If you want to operate on this noun, you
either have to revalidate that it fits the desired type (prohibitively
slow, except for things like "atom" and "list of a dozen atoms"), or slam
it against a gate that is itself a vase," and Curtis says, "And there is no
way for statically typed code to turn a vase of foobar into a foobar....it
can't turn the vase of a move into a move, any more than it can turn the
vase of a foobar into a foobar...This requires the Arvo kernel to do things
like using Nock directly to call type-checking routines on plain nouns.".
So are you saying that (a) when %meta is seen, at runtime the enclosed card
(or move?) is dynamically typechecked against the enclosed span to make
sure it is of the claimed type, despite the prohibitive slowness mentioned
by Anton, and then if it passes the check, Hoon is instructed to typecast?
Or, alternately, (b) is Arvo just assuming that the provided span is
correct without checking it, and instructs Hoon to typecast? Or is neither
(a) nor (b) correct?
thanks,
b
--
You received this message because you are subscribed to the Google
Groups "urbit" group.
To unsubscribe from this group and stop receiving emails from it, send
For more options, visit https://groups.google.com/d/optout.

--
Cabmold delenda est

--
Cabmold delenda est

...

[Curtis Yarvin]

Thanks for reading! I swear, the whitepaper is actually there to be
read this way, not just to be large and dense and imposing... I hope
it's been reasonably clear.

Post by Bayle Shanks
Thank you all for your help!

Post by Anton Dyudin
To expand on the last sentence of 3, arvo has the vane as a vase,
therefore when arvo e.g. passes unix events to the vane it does so as a
vase(span %noun) and received the response as a vase, can then send the
moves in the response to other vanes as vases, etc.; as far as the vane(and
execution of any nock in the compiled core of the vane) is concerned, it
just got passed a well-typed card. But before execution occurs, the span of
the card is first checked against the vane(and then discarded), this being
the dynamic "compile time".

Post by Anton Dyudin
1. Yes
3. Vases are always required for type-checking, or more specifically
spans are. /normally/, when you pass round a value, its type has already
been checked; however, in communication between vanes (or between a vased
core in a vane and the vane itself), this is done on every call(and then
memoized). Internally to the vane, the type tag is usually hidden, since the
output of slamming a vase of a move against a gate at an arm in a vase of a
core is also a vase.
4. By "revalidated" I meant calling a clam on a noun to ensure the noun
fits in the(clam's) span. What actually happens in (a) is that the type
checker is run against the /spans/ of the input and target. The span in
%meta is assumed to be correct, yes, having been provided directly by a vane
in a series of safety-preserving operations on vases: the first, of course,
being baked-in constant !>s and/or [%noun foo], followed by dynamically
compiling and executing twigs of various sorts.

Post by Bayle Shanks
Okay, thank you both, it's a little clearer now, although i still have
some followup questions.
1) So my understanding from your replies is that a %meta wrapper occurs
for something whose type cannot be statically known, and its function is to
engage some sort of alternate form of type-checking or type-casting. Arvo
checks for a %meta and if it sees one, it engages the alternative
typechecking/casting and then unwraps the %meta, passing on the wrapped
value in its place. Is this correct?
2) Moves vs. cards: Both of you speak of a vase of a move, but the
whitepaper says "[%meta vase] - where the vase is the vase of a card". So is
the vase the vase of a move, or the vase of a card? Or are all cards moves?
Or are all moves cards? Upon further reflection, i see that the whitepaper
never defines exactly what data a move contains, nor the exact relationship
between moves and cards; it just says "A move has a duct, which is a list a
wires, each of which is analagous to a stack frame"; so does a move contain
any data besides a duct?
3) Why are vases sent even when %meta is absent: The whitepaper says,
"...Arvo manages both vanes and moves as vases, [span noun] cells. Every
dispatch is type-checked". Does this mean that typically, every move is
statically typechecked via the usual Hoon mechanisms, and that these
mechanisms are overridden in the case of %meta (like a C typecast)? But if
that were the case, why would the typical case need vases at all? Is the
concept of a 'vase' something Arvo is adding here, or are vases always
required for typechecking in Hoon? That is, does Hoon require every value to
be explictly passed around within a vase in order for it to typecheck that
value? For example, if i want to pass around "[3 3]", and i want Hoon to
recognize that this is in fact a pair of atoms, then must i explicitly pass
it as "[span [3 3]]" where 'span' is the span indicating pairs of atoms? I
would have assumed that either the type of values was checked at
compile-time (like in the language C), or alternately that the type tag (the
span, in this case) was hidden from the programmer by the runtime (like many
interpreted languages) so that internally the value would be (pair-of-atoms,
[3 3]) but the programmer sees it as just [3 3]?
4) Is the type being 'revalidated' even though that is 'prohibitively
slow', or is the sender being trusted to give the correct span, or something
else: Anton says, "If you want to operate on this noun, you either have to
revalidate that it fits the desired type (prohibitively slow, except for
things like "atom" and "list of a dozen atoms"), or slam it against a gate
that is itself a vase," and Curtis says, "And there is no way for statically
typed code to turn a vase of foobar into a foobar....it can't turn the vase
of a move into a move, any more than it can turn the vase of a foobar into a
foobar...This requires the Arvo kernel to do things like using Nock directly
to call type-checking routines on plain nouns.". So are you saying that (a)
when %meta is seen, at runtime the enclosed card (or move?) is dynamically
typechecked against the enclosed span to make sure it is of the claimed
type, despite the prohibitive slowness mentioned by Anton, and then if it
passes the check, Hoon is instructed to typecast? Or, alternately, (b) is
Arvo just assuming that the provided span is correct without checking it,
and instructs Hoon to typecast? Or is neither (a) nor (b) correct?
thanks,
b
--
You received this message because you are subscribed to the Google
Groups "urbit" group.
To unsubscribe from this group and stop receiving emails from it, send
For more options, visit https://groups.google.com/d/optout.

--
Cabmold delenda est

--
Cabmold delenda est

--
You received this message because you are subscribed to the Google Groups "urbit" group.
To unsubscribe from this group and stop receiving emails from it, send an
For more options, visit https://groups.google.com/d/optout.

...