A $vase is a pair of $type and $noun, where the type describes the noun. They're used all over Urbit, to represent data whose type we can't know ahead of time. This often comes up when being asked to compile and run other Hoon code. It's also used to store data that could be any type, but where we want to know the type, so we tag the value with its type to form a vase.
A Hoon $type is a data structure that specifies a set of nouns. Remember, everything in Urbit is a noun, so a $type can be thought of as a way of representing a boolean predicate that determines whether some noun is within the set.
Types are not just used for this purpose, though. They're also used to represent the type of the "subject", which is the "scope" or "environment" that some Hoon code can access. This means that Hoon's equivalent of a symbol table lives in the type.
The programmer can name parts of a type, including the type of the subject. Once part of a type has a name, Hoon code can refer to any named field within that type. Since the subject of any Hoon expression always has a known type at compile time, a reference (a "wing", like foo.+<.bar.|3.baz) to a field within that subject is compiled to a Nock 0 operation (subtree lookups) at a known constant axis (tree slot).
%noun refers to the set of all nouns.[%atom %$ ~] refers to the set of all atoms (numbers).[%cell %noun %noun] refers to the set of all cells (pairs).[%face %foo %noun] refers to the set of all nouns, tagged with the %foo face. This refers to the same set as %noun.All executable Hoon code is found in a "core". This core stores a map from "arm" name (like an OOP getter function) to result type, along with some other information about the core. If the core is a "door" (like an OOP object) or a "gate" (like an anonymous function), then slot 6 (the head of the tail) of the core is a "sample" slot, which is overwritten with instance data or function argument, respectively. Whether this core expects a sample, and if so, what the sample's type is, is represented in the $type data structure for cores of that type.
Core types are more complex than this simplified explanation, but this description is hopefully enough detail to be able to work with cores from vase mode.
A Hoon $type is defined by this (pronounced "buc type", also called "the type of type"):
+$ type $~ %noun ::
$@ $? %noun :: any nouns
%void :: no noun
== ::
$% [%atom p=term q=(unit @)] :: atom / constant
[%cell p=type q=type] :: ordered pair
[%core p=type q=coil] :: object
[%face p=$@(term tune) q=type] :: namespace
[%fork p=(set type)] :: union
[%hint p=(pair type note) q=type] :: annotation
[%hold p=type q=hoon] :: lazy evaluation
== ::
This is a union, meaning a type can be one of several different things. It's a discriminable union, meaning a piece of code can tell which kind of thing a type is by inspecting it.
If an instance of $type is an atom, it's either the value %noun, referring to any noun (the set of all nouns), or %void, referring to nothing (the empty set, so no noun will ever be part of this set). %void is mostly there for mathematical completeness, so the compiler can represent the null set internally -- any "inhabited" type will not be %void.
Otherwise, an instance of $type is a cell, in which case the head is a tag (e.g. %atom, %cell, or %core) that says what kind of type this is. The values to the right of the tag contain the information used to specify the variable lookup namespace for this type (i.e. the mapping from wing to axis, or axis and core arm) and constraints that limit the set of nouns described by this type.
An %atom type describes a set of numbers. The p=term in an atom type is its "aura", a name for a kind of value that can be stored as an atom -- %da for date, %ux for hexadecimal number, %t for text, etc. The q=(unit @) is either ~, meaning any value, or [~ value], in which case this type has only a single member. The type %foo refers to the set whose only instance is the atom %foo.
The %cell type refers to cells whose heads have type p and tails have type q.
When working with types, %hold types are particularly important to understand. A %hold is a lazily evaluated type. This is used for recursive types and polymorphism (wetness). A hold contains a p=type, referring to a subject type, and a q=hoon, a hoon expression intended to be run on a value of that type.
One can "evaluate" a hold by asking the compiler to "play" the hoon against the subject type, meaning to infer what type of value would result from running that hoon against a value of the subject type. For a recursive type, this result type refers to the same hold, usually in one or more of the cases of a %fork.
Consider the type (list @ud). This is a hold. Just as any instance of this list type is either ~ or a non-null list [i=@ud t=(list @ud)], when you evaluate the list's hold, you get a fork of [%atom %n [~ ~]] and [%cell [%face %i [%atom %ud ~]] [%face %t [%hold ...]]], where the hold is the same as the original hold.
The primary introduction form for a vase is the !> rune, which produces a vase of its input. A vase can also be constructed manually as a cell whose head nests in $type, like [[%atom %ud ~] 3].
An elimination form for a vase is something that converts a vase to a statically typed value.
One unsafe elimination form is the !< rune, which takes a mold and a value and (unsafely) converts the value to a typed value. The more traditional elimination form has no syntactic support, but involves pattern-matching on the type data structure, e.g. dispatching based on whether the type is atom, cell, or something else, and coercing the value to a specific type using a mold function.
The lack of a safe general-purpose elimination form stems from the fact that Hoon's structural type system cannot guarantee that the value in a vase's tail is an instance of the type in the vase's head, i.e. is an instance of that type. If not, the vase is said to be "evil".
Despite this limitation, it's relatively straightforward to convert vases to statically typed outputs safely, and plenty of Hoon code does it, in both kernelspace and userspace.
+slopThe +slop gate combines a cell of vases into a vase of a cell. It does this by making a cell [q.hed q.tal] of the values of the two input vases, and it constructs the type of the output vase as [%cell p.hed p.tal], i.e. a cell whose head has the same type as the first vase and whose tail has the same type as the second vase.
Definition:
:: in /sys/hoon/hoon
::
++ slop :: cons two vases
|= [hed=vase tal=vase]
^- vase
[[%cell p.hed p.tal] [q.hed q.tal]]
+slop Examples:
> (slop !>(3) !>(4))
[#t/[@ud @ud] q=[3 4]]
> (slop !>(foo=3) !>(4))
[#t/[foo=@ud @ud] q=[3 4]]
> (slop !>(foo=3) !>(bar=4))
[#t/[foo=@ud bar=@ud] q=[3 4]]
> (slop !>(foo=3) !>([bar=4 baz=5]))
[#t/[foo=@ud bar=@ud baz=@ud] q=[3 4 5]]
> (slop !>(foo=%foo) !>([bar=[4 5] baz=%baz]))
[#t/[foo=%foo bar=[@ud @ud] baz=%baz] q=[7.303.014 [4 5] 8.020.322]]
+slapThe +slap gate runs a hoon expression against a vase, producing a vase of the result. This happens in two steps: first, compile the hoon expression to Nock using the head of the input vase as the compilation subject type, then run the resulting compiled Nock formula against the tail of the input vase as the subject value. The compiler returns both Nock and the type of the result of running that Nock formula against any value of the input subject type, so the resulting vase is constructed using that as the head (type) and the result of running the compiled Nock formula as the tail (value).
Definition:
::
++ slap
|= [vax=vase gen=hoon] ^- vase :: untyped vase .*
=+ gun=(~(mint ut p.vax) %noun gen)
[p.gun .*(q.vax q.gun)]
+slap first compiles a parsed Hoon expression (gen) to Nock by calling the compile function +mint:ut, passing in the type from the input vase to use as the compilation subject type -- this informs how the Hoon expression gets compiled. Compilation returns gun, a pair of the inferred product type and a compiled Nock formula. Note that there are two steps here: after compiling the Hoon expression to a Nock formula, that Nock formula must be run against a subject noun whose type matches the subject type passed to +mint. The tail of the resulting vase comes from running the compiled Nock formula q.gun against the value of the subject q.vax using the .* raw Nock execution rune, producing the untyped value of the result. The head of the resulting vase is the inferred product type resulting from +mint.
Note that a Hoon expression cannot be compiled to a Nock formula without also specifying the type of the subject, which affects the compilation. Specifically, variable lookups, including arms, faces, and raw subject axes, all need to be resolved according to the type of the subject. The following examples show the resulting Nock formula from compiling foo against different subjects, using the != rune to return a quoted Nock formula derived from compiling the enclosed Hoon expression against the type of the subject. => sets the subject (including its type), so we see how the compilation results differ:
> => foo=3 != foo
[0 1]
> => [foo=3 bar=4] != foo
[0 2]
Not only the Nock formula, but also the inferred output type from compilation varies based on the subjec type. The following examples show the output type from compiling the Hoon expression . that returns the subject unchanged:
> p:(~(mint ut -:!>(*foo=@ud)) %noun (ream '.'))
#t/foo=@ud
> p:(~(mint ut -:!>(*foo=@tas)) %noun (ream '.'))
#t/foo=@tas
+slap Examples:
> (slap !>(3) (ream '.'))
[#t/@ud q=3]
> (slap !>(3) (ream '+(.)'))
[#t/@ q=4]
> (slap !>(3) (ream '[33 44]'))
[#t/[@ud @ud] q=[33 44]]
> (slap !>(3) (ream '%foo'))
[#t/%foo q=7.303.014]
> (slap !>([33 44]) (ream '.'))
[#t/[@ud @ud] q=[33 44]]
> (slap !>([33 44]) (ream '-'))
[#t/@ud q=33]
> (slap !>([33 44]) (ream '+'))
[#t/@ud q=44]
> (slap !>([foo=33 bar=44]) (ream '.'))
[#t/[foo=@ud bar=@ud] q=[33 44]]
> (slap !>([foo=33 bar=44]) (ream 'foo'))
[#t/@ud q=33]
> (slap !>([foo=33 bar=44]) (ream 'bar'))
[#t/@ud q=44]
> (slap !>([foo=33 bar=44]) (ream '+(foo)'))
[#t/@ q=34]
+slap and +slop operations can be composed arbitrarily, and higher-level operations can be built out of them, forming a relatively simple algebra. This algebra can be thought of as a dynamically typed programming language. Each value in the language is a vase (a dynamically typed datum), and the basic operations are +slap and +slop.
For example, the Hoon expression (slap (slop v1 (slop v2 (slap v3 h1))) h2) takes in four vases and two hoon expressions, and produces a vase. A pseudocode version of this would be h2([v1 v2 h1(v3)]). A visual representation of this expression looks like this:
+slap
/ \
+slop h2
/ \
v1 +slop
/ \
v2 +slap
/ \
v3 h1
Here's a Hoon example:
=/ v1=vase !>(%foo)
=/ v2=vase !>(%bar)
=/ v3=vase !>(%baz)
=/ h1=hoon (ream '%qux')
=/ h2=hoon (ream '[%result .]')
::
%+ slap
%+ slop v1
%+ slop v2
(slap v3 h1)
h2
:: result
[#t/[%result %foo %bar %qux] q=[128.009.175.786.866 7.303.014 7.496.034 7.894.385]]
There are a lot of higher-level operations on vases, mostly in /sys/hoon/hoon and some in /sys/arvo/hoon. Here's a sampling for instructional purposes.
:: note: current implementation looks different
::
++ slam
|= [gat=vase arg=vase]
^- vase
(slap (slop gat arg) !,(*hoon (- +)))
::
++ slot :: got axis in vase
|= [axe=@ vax=vase] ^- vase
[(~(peek ut p.vax) %free axe) .*(q.vax [0 axe])]