The last cell (blue) of the list is mutable
Mezzo is now available via OPAM. To install Mezzo, just run opam install mezzo.
mezzo binaryMezzo files end with .mz. Open your favorite editor, and edit ex1.mz. Put the following contents into the file:
val x = 1
val _ =
print x
Next, assuming the mezzo binary is available in your PATH, run mezzo ex1.mz. The output is as follows:
val x @ int::int
The syntax of Mezzo is reminiscent of ML, which we assume the reader is familiar with. We will introduce syntax on-the-fly, presenting the language constructs as we make progress through this tutorial. Top-level values are introduced using the val keyword; intermediate definitions are introduced using the usual let keyword.
By default, mezzo type-checks the program, then prints the type of the top-level values. Here, mezzo judiciously type-checked x as being an integer. More precisely, x has the int type, from the int module.
In Mezzo, names are qualified using ::. By writing m::x, you refer to the name x from module m. The int module is bundled with Mezzo; it is found in the corelib directory, and exports the int type as well as arithmetic operators.
Mezzo programs can be interpreted, using the built-in interpreter. Interpreting a program is as simple as passing a -i argument ("interpret") to the mezzo binary.
$ mezzo -i ex1.mzThe output will be:
1
Compiling a Mezzo program is done by "translating" it into an OCaml program1.
This is done by passing the -c argument ("compile") to the mezzo binary.
$ mezzo -c ex1.mzThis creates mzex1.ml, the translated version of ex1.mz. We now need to compile mzex1.ml.
Mezzo programs need to be linked with the mezzo runtime library. The runtime library of mezzo is distributed as an ocamlfind package called mezzo.rtlib. Our program also uses the "print" function, which is bundled in the Mezzo core library. The Mezzo core library is distributed with mezzo, and is available as mezzo.corelib. Similarly, the standard library is available as mezzo.stdlib. These two packages are made up of Mezzo modules which have been translated to OCaml, compiled, and packaged as libraries.
Running ls $(ocamlfind query mezzo) reveals the existence of a whole variety of files. First of all, there are the interface files (.mzi) for all the modules in the core and standard libraries. These interface files are useful for the Mezzo type-checker when type-checking your own modules. These interface files are also useful for the user, to check which functions are available. We do not distribute the .mz sources: these modules have been translated and compiled already; they are packaged into the various .cma and .cmxa files. For each .mzi, we also distribute the correponsding .cmi and .cmx files, which is are required for linking against them. Finally, there's the runtime support library.
We can compile our original example using:
$ ocamlbuild -use-ocamlfind -package mezzo.rtlib \
-package mezzo.corelib mzex1.byteBarring any errors, the resulting program can be launched.
$ ./mzex1.byteUnsurprisingly, the output is:
1One may want to automate all these steps. We provide a sample project.
One thing that we didn't mention is the mezzo.build package. It provides a set of rules that enable ocamlbuild to generate .ml from .mz files by calling mezzo -c, thus automating the whole process. This rule is only triggered if the file is tagged with the mezzo OCamlbuild tag.
In order to use these rules, you can add the -plugin-tag package(mezzo.build) option to your ocamlbuild invocation. This is a fairly recent feature that requires OCaml 4.01.0. It makes sure that when compiling your myocamlbuild.ml file, the mezzo.build package will be available. Then, you can use:
Ocamlbuild_mezzo.init ~boot:false ();;in your myocamlbuild.ml file. This will enable the standard Mezzo compilation rules. Finally, you need to tag the files with the mezzo tag to enable to .mz -> .ml rule, which can be done using the following _tags file:
<**/mz*>: package(mezzo.rtlib), package(mezzo.corelib), \
package(mezzo.stdlib)This line also activates the runtime-library, as well as the core and the standard libraries of Mezzo.
All this is taken care of in the sample project above. Please do clone it!
TODO
MezzoLib.t and an OCaml type.The type system is central in the design of Mezzo. It is novel, sometimes complex, and certainly does require some effort to fully understand. We thus devote a section to the type system itself, before showing how to write programs in the language.
Mezzo is a language that helps the programmer reason about state. State is a pervasive notion in computer programs. Consider the following pseudo-code:
int main () {
int* x = new int;
// x is a _valid_ pointer to an integer
...
delete x;
// x is an _invalid_ pointer that should not be used
}The variable x changes state: it goes from the "valid pointer" state to the "invalid pointer" state. When x is "valid", it can be safely dereferenced. Once x is delete'd, one must no longer use it. A traditional type system, however, will just assert that x is a pointer to an integer: it is up to the programmer to make sure they only use x when it is valid. The type system provides no help for reasoning about the state that x is in.
What if we had a type system that allows one to reason about state? This seems simple enough. However, reasoning about state is tricky because of aliasing. Imagine we start thinking about state in a naïve fashion.
int main() {
int* x = new int;
// x has type "valid int*"
...
int* y = x;
// x and y have type "valid int*"
...
delete x;
// x has type "invalid int*", y has type "valid int*"
...
delete y;
// crash!
}The type system sees two different names, x and y, and gives each one of them a type. Even if we were to track the state change of x, because y is actually a synonym for x, the call to delete y would still crash the program. We say that x and y are aliases.
Aliasing is closely related to the problem of ownership. If one part of the program sees x as a "valid integer", then tracking state changes for x only makes sense if no other part of the program sees x. Thus, we should be able to say that we "own" x.
Mezzo blends in several concepts from the literature; it incorporates mechanisms that speak about aliasing and ownership, so as to obtain a type system that is able to deal with state.
In this section, we used examples in a C-like language. Mezzo is a language that draws inspiration from ML; it has first-class functions, pattern matching, and a garbage-collector. The syntax of Mezzo is thus very similar to that of ML, and we will forget about C-like snippets in the remainder of this tutorial.
We introduce the foundational notion of Mezzo, permissions, through an informal presentation of the type system. We anticipate on the following section, which will exhaustively introduce all the constructs in the type system of Mezzo.
In a traditional, strongly-typed programming language, such as ML, one may say that "x has type ref int", which is the type of integer references. This implies, in particular, that the type of x is valid for the rest of x's scope. Conversely, in Mezzo, x may "have type" ref int, but it may also have, later on, type ref string. Thus, we need to come up with a new way to talk about "the" type of a variable.
We talk about types using permissions. A permission is written x @ t, where x is a program variable, and t is a type. One may think of a permission as an access token that grants its owner the right to use x as a variable of type t. Permissions are transient: this permission may disappear, to be replaced by x @ u at a later program point.
Obtaining a fresh permission is easy. Writing let x = 1 in ... makes x @ int available in the continuation ....
The permission mechanism is our type system. It is pervasive, in the sense that at any program point, a current permission is available. When the program starts, the current permission is empty. As execution progresses, the current permission evolves to become a conjunction of permissions, which we write p * q. Permissions do not exist at run-time.
The current set of permissions tells the programmer what they can do with variables. For the expression x + y to be well-typed, the conjunction x @ int * y @ int has to be available at that program point.
Earlier, we type-checked the following program:
val x = 1
val _ =
print x
The permission val x @ int::int that the type-checker outputs is the conjunction that remains after program execution.
In the case of function, permissions describe the assumptions that a function makes on its arguments, and the guarantees that it provides on its return value. In other words, permissions describe the pre- and post-conditions of functions. Let us consider the following function signature.
val length: [a, b] (x: list a) -> int
The type of the length function looks like the one from ML. It expresses a precise invariant, though: the function will consume a permission x @ list a from its caller. That is, if one wishes to call length x, then one must give up x @ list a. Conceptually, the length function will use that permission to access x as a list of elements, then, once it is done with it, the permission will be returned to the caller, along with a result of type int.
As a syntactic convention, and unless otherwise specified, permissions for the arguments of functions are understood to be taken and returned to the caller.
What happens, in practice, is the following, where comments denote the set of available permissions at a given program point.
(* x @ list a *)
let l = length x in
(* l @ int * x @ list a *)
...
Let us now consider a different function signature. The function called mswap swaps in-place the two components of a mutable pair (mpair).
val mswap: [a, b] (consumes x: mpair a b) -> (| x @ mpair b a)
The presence of the consumes keyword indicates the function takes a permission x @ mpair a b from the caller, and does not return it. What is returned is the unit type (), along with a permission x @ mpair b a. We write the conjunction of a type t and a permission p as (t | P), but the example above uses syntactic sugar for the case where t = ().
This signature expresses the fact that the function changes the type of its argument. What happens, from the caller's perspective, is as follows.
(* x @ mpair a b *)
mswap x;
(* x @ mpair b a *)
...
The variable x went from mpair a b to mpair b a. This is a type-changing update, which the permission mechanism accurately describes.
For the example above to be sound, no one else must own a copy of x @ mpair a b, since this information would be invalidated by the call to mswap. The type system of Mezzo guarantees that permissions that denote mutable data, such as x @ mpair a b are uniquely-owned. We say that these permissions are exclusive. In practice, this means that it is impossible to obtain another copy of x @ mpair a b.
Conversely, the val x @ int::int permission that we saw earlier denotes immutable, permanent knowledge. It is therefore safe to share that information with "others" (other parts of the program, other threads), and we say that this permission is duplicable. In other words, one can obtain as many copies of it as desired.
As we will see later on, both Mezzo and the user can always tell whether a permission is exclusive or duplicable. This is done by looking up the definition of t in x @ t.
We just saw read-write, uniquely-owned permissions ("exclusive") and read-only, shared permissions ("duplicable"). Permissions which are neither exclusive or duplicable are said to be affine. Affine permissions are a strict superset of exclusive and duplicable permissions.
Permissions can express two kinds of aliasing information: must-alias constraints, and must-not-alias constraints.
Consider the following code snippet:
val _ =
let x = newref 3 in
let y = x in
assert y @ ref int
The first line gives rise to x @ ref int, as we saw earlier. The second line is more interesting. Instead of reasoning about which one of x and y gets to own the reference, we generate a permission that embodies the fact that x and y are synonyms: the permission embodies a must-alias constraint. This permission is y @ (=x).
The type =x is a singleton type, a type whose only inhabitant is x itself. Saying that y "has type" =x amounts to saying that x and y are actually the same thing; that is, that they're aliases. We use syntactic sugar for that special form of permissions, and write y = x.
The interesting point is that we dont't have to assign ownership of the reference to either x or y: the system just records the aliasing information and knows that it can substitute x for y wherever needed. In particular, when the user asserts that y is a reference to an integer at line 3, Mezzo automatically figures out that it can rewrite x @ ref int * y @ (=x) into y @ ref int * y @ (=x), thus satisfying the assertion.
Singleton types are also used in structural types. Whenever one obtains a permission for, say, a tuple, the type-checker automatically introduces names for the components. For instance, instead of having x @ (ref int, ref int), the type-checker will introduce internal names l and r, and transform this into x @ (=l, =r) * l @ ref int * r @ ref int. This is, again, useful to reason about ownership. Consider the example below.
val _ =
let x = newref 5, newref 7 in
let y, z = x in
assert y @ ref int * z @ ref int;
assert x @ (ref int, ref int);
assert x @ (unknown, ref int) * y @ ref int;
Since we have an expanded form for x, type-checking the let-binding merely amounts to adding y = l * z = r into the current conjunction: we don't have to reason about whether the references are owned by x or by y and z individually.
Permissions also implicitly contain must-not-alias information. This stems from the unique owner policy. Having, for instance, a conjunction such as y @ ref int * z @ ref int tells you that y and z must be distinct; otherwise, it would violate the unique owner guarantee of Mezzo. This is a must-not-alias constraint. Similarly, having y @ ref int * z @ int also guarantees that y and z are distinct.
Not all conjunctions are informative: having, for instance, y @ int * z @ int doesn't tell anything. The two variables may or may not be aliases. This is due to the fact that int is a duplicable type.
val _ =
let x = 11 in
let y = x in
assert x @ int * y @ int;
The assertion above would fail with a reference to an integer.
As a side note, some conjunctions embed a very strong meaning. A conjunction such as x @ ref int * x @ ref int violates the unique owner policy of Mezzo. This is impossible! Therefore, execution can never reach such a program point. The conjunction denotes dead code, that is, code that is never run.
Before giving a thorough presentation of the type system of Mezzo, we illustrate type-checking on two simple examples. The map function will be our running example: we first write a trivial implementation, and show how to perform type-checking in Mezzo. We then write a tail-recursive version of map, something which cannot be done in ML. We show how the type system of Mezzo allows us to type-check it.
This section anticipates a little bit on the syntax of both types an expressions. These will be described in the following sections.
The way one would write the map function in, say, OCaml, is as follows:
let rec map f l =
match l with
| hd :: tl ->
f hd :: map f tl
| [] ->
[]One can write the same simple function in Mezzo. Note the consumes annotation that leaves it up to the caller to duplicate the permission on the list, if possible.
open list
val rec map [a, b] (f: (consumes a -> b), consumes xs: list a): list b =
match xs with
| Cons { head = h; tail = t } ->
let h' = f h in
let t' = map (f, t) in
Cons { head = h'; tail = t' }
| Nil ->
xs
end
Let us see how this function is type-checked. In the snippet above, comments denote the currently available conjunction, as well as the reasoning steps that the type-checker performs. Comments omit the permission for f which remains available all throughout the body of map.
Initially, when execution enters the function body, xs @ list a * f @ (consumes a) -> b is available. Matching on xs refines the permission for xs into a structural one.
In the first branch, we learn that xs is a Cons cell: the permission for xs is updated in place to reflect this. Moreover, the type-checker introduces names for the fields of xs: it expands the structural permission. This is, as we saw, a must-alias constraint.
Calling f consumes the permission for h and gives a new one for h'. Similarly, calling map consumes the permission for t and produces a fresh permission for t'. Finally, we return: we call ret the return value of the function. The permission for ret is, again, a structural one, since we know it is a Cons block. The type-checker performs various rewritings and foldings to finally obtain ret @ list b, which satisfies the declared return type for map.
In the second branch, we just learn that xs is a Nil branch; returning xs actually creates a new equation, which the type-checker uses to rewrite the current conjunction, so as to make ret @ Nil appear. It turns out that Nil can also be seen as a value of type list b, and the type-checker is aware of that fact.
The function above has to wait for the recursive call to map to complete before constructing the mapped list. Therefore, it uses linear stack space: it is not tail-recursive. There is, however, one way to write this function in a tail-recursive style, called destination-passing style.
The last cell (blue) of the list is mutable
The next step consists in mapping the next element; the blue cell is frozen
The procedure continues until it reaches the end of the list and the entire list has been mapped
The algorithm, as illustrated above, uses an unfinished list. The yellow cells are immutable, but the last cell is mutable (blue). Mapping the next element amounts to allocating a fresh blue cell, wiring the old blue cell to the new one, freezing the old, mutable blue cell, into an immutable yellow cell.
A traditional type system such as that of ML cannot express this situation: the in-progress, unfinished list is not representable in a traditional data type. Moreover, since the type of the blue cells moves from mutable, unfinished cells, to finished, well-formed cells, there must be reasoning about ownership, to justify why changing the type of a memory block is sound.
Here's how one would do it in Mezzo.
(* This file implements a destination-passing style, tail-recursive
* version of [List.map] for immutable lists. It uses a temporary mutable cell
* that is later on "frozen" when it's ready. *)
data list a = Cons { head: a; tail: list a } | Nil
data mutable cell a = Cell { head: a; tail: () }
(* This is the recursion loop, which turns [c0], an unfinished, mutable list
cell, into a well-formed, immutable list. *)
val rec map1 [a, b] (
f: (consumes a) -> b,
consumes c0: cell b,
consumes xs: list a
): (| c0 @ list b)
=
match xs with
| Nil ->
c0.tail <- xs;
tag of c0 <- Cons
| Cons { head = h; tail = t } ->
let h' = f h in
let c1 = Cell { head = h'; tail = () } in
c0.tail <- c1;
tag of c0 <- Cons;
map1 (f, c1, t)
end
(* We need to unroll the recursion to take into account empty lists. *)
val map [a, b] (f: a -> b, consumes xs: list a): list b =
match xs with
| Nil ->
xs
| Cons { head; tail } ->
let c = Cell { head = f head; tail = () } in
map1 (f, c, tail);
c
end
The data type of lists is recalled. We define the cell type that represents an unfinished, mutable list cell.
The heart of the algorithm is map1, a recursive function that implements the main loop. This function transforms c0, an unfinished, mutable list cell, into the head of a well-formed, immutable list. Just like the standard definition of map, it consumes the original, to-be-mapped list.
The start of the algorithm is map, which unrolls the recursion. If the original list is non-empty, map creates a fresh cell to stand for the first element of the new, mapped list, then calls map1 on it. Per the semantics of map1, after the call to map1 returns, c now points to a well-formed, immutable list of b.
Let us now focus on the heart of the algorithm, namely, the body of map1. In the case where the to-be-mapped list xs is empty, we can finish the mapping procedure by putting xs (which is Nil) into the last cell's tail. Once this is done, we turn it into an immutable list cell, by changing its tag from Cell to Cons. The list is now fully mapped.
In the case where the to-be-mapped list xs is not empty, we allocate a new, mutable cell c1, whose head has been mapped through f. The old, still-mutable blue cell c0 is modified: its tail is made to point to c1, and it is frozen into an immutable Cons cell.
At this stage, c0 is not yet a valid list b: its tail points to an unfinished cell, namely c1. We call map1 recursively on c1. Per the semantics of map1, c1 is now a list b, which allows us to deduce that c0 also is a list b.
It is interesting to note that while the execution of the code is tail-recursive, the reasoning is not: an extra reasoning step takes place after the recursive call to map1, and is needed to justify why c0 has become a well-formed list.
We provide an interactive feature where you can see the permissions evolving in real-time, as the execution progresses through the example. This should (hopefully) help illustrate the way permissions work on a concrete example.
We now present the whole zoology of types in Mezzo. This allows us to provide a reference before going into further discussion; this also allows us to talk about our syntactic conventions for function types in greater detail.
Before going any further, we need to mention that types have kinds. Kinds classify types into three categories. A type is either:
x, at kind termx @ t, p * q, empty, at kind permint -> int, or ref int, at kind typeWe sometimes mention the well-kindedness judgement informally in the syntax of types.
Structural types talk about the structure of a memory location. Structural types are either tuples types of the form (t1, ..., tn), or constructor types of the form A { f1: t1 ...; fn: tn }.
Structural types are always expanded by the type-checker, meaning that in practice, the type-checker will introduce names so that it manipulates types of the form (=x1, ..., =xn) or A { f1 = x1, ...; fn = xn }, as stated earlier.
Structural types always have kind type.
The unit type is the empty tuple, which we write ().
One may also encounter types variables such as a or int and type applications such as list a. Their kinds depend on how the variable was defined: a may be introduced with a quantification such as [a: k] ... (it has kind k), int may be defined as abstract int: type (it has kind type), and list a is a data type, meaning it has kind type.
A type can be packed along with a permission, by using the type / permission conjunction, written (t | p), where t has kind type and p has kind perm. This is of particular importance, especially in function types. In the case where t is the unit type (), we offer syntactic sugar, so that the user can write (| p).
Mezzo offers universal quantification, written as [a: k] t, and existential quantification, written as {a: k} t. The kind k is optional and defaults to type.
Singleton types of the form =x requires that x be a program variable (hence, at kind term). A singleton type has kind type.
The anchored permission x @ t, where x is a program variable (thus, at kind term) and t has kind type, is a permission, hence at kind perm. The conjunction of permissions p * q as well as the empty permission empty are also naturally at kind perm.
Type variables and type applications may also be at kind perm.
Is it sometimes convenient to use unknown, the top type at kind type.
Function types benefit from special syntactic conventions, which makes expressing their pre- and post-conditions easier. We thus devote an entire section to function types. Function types have kind type.
A basic function type is of the form t -> u. For instance, here is the signature of the list::length function, which we saw earlier.
val length: [a] (list a) -> int
We said that the permission for the argument was understood to be taken and returned to the caller, which embodies the fact that the ownership of the list is temporarily transferred to length, so that it computes the length, and then returned to the caller.
(* x @ list a *)
let l = length x in
(* l @ int * x @ list a *)
Permissions are not always returned to the caller. Let us take the list::concat function as an example. The function takes two lists and concatenates them. In order to be sound, that function must consume the ownership of the two original lists, so as to to build their concatenation. Failing to do that would mean that the caller could access an element both through the original list and the concatenated list, thus breaching soundness.
One can express this transfer of ownership using the special consumes keyword.
val concat: [a] (consumes list a, consumes list a) -> (list a)
The consumes keyword can appear only on the left-hand side of a function type. It can appear at arbitrary depth, several times; consumes may refer to a type with kind type or perm; consumes keywords cannot be nested. The example above would also work with:
val concat: [a] (consumes (list a, list a)) -> (list a)
Intuitively, all the parts of the argument that are not marked as consumes are preserved through the function call.
Formally, the consumes keyword is interpreted as follows. If the function has type t -> u, then we take t1 to be t where consumes v is replaced by v. We also take t2 to be t where consumes v is replaced by unknown or empty. We then understand the function type to mean (root: t1) -> (u | root @ t2). That is, the function preserves the sub-parts of t that are not consumed.
Names can be introduced in function types using the name introduction construct. It is of the form x: t.
Any name introduced in the domain of a function type is available in the domain and the codomain. For instance, in the example below, both t and u may refer to x.
val f: (x: int, t) -> u
Any name introduced in the codomain of a function type is available in the codomain only. For instance, in the example below, only u may refer to x.
val g: t -> (x: int, u)
Name introductions may appear at arbitrary depth. Name introductions are hidden by function types and quantifiers. For instance, in the example below, t may not refer to x or y.
val h: (
t,
((x: int) -> int),
{u} (y: u)
) -> int
Internally, name introductions in the domain of a function type translate to universal quantifiers over the function type, while name introductions in the codomain of a function translate to existential quantifiers over the codomain. The name introduction constructs are replaced by a conjunction of a singleton type and a permission. Thus, the three functions above are understood as:
val f: [x: term] ((=x | x @ int), t) -> u
val g: t -> ({x: term} ((=x | x @ int), u))
val h: (
t,
([x: term] (=x | x @ int) -> int),
{u} (=y | y @ u)
) -> int
Name introduction constructs may also appear in data types and type annotations.
Please note that the function type above for concat use a tuple for its argument, instead of being a curried function. We strongly encourage users to write functions that take tuples. Indeed, function types are duplicable, meaning that they can't close over (capture) non-duplicable data. Thus, if one were to write the concat function above in a curried style, they would need the following signature:
val concat: [a] (xs: list a) -> (
consumes (list a | xs @ list a) -> (list a)
)
We name the first list xs. The function type above expresses the fact that applying the function to its first argument will actually not modify or consume xs; rather, all the action will happen when applying the second argument. Thus, when calling the function on its second argument, the permission for the first argument is required for the function call to succeed.
Writing curried function types is difficult, and the resulting types generate extra work for the type-checker, so currying shouldn't be used unless absolutely necessary.
It is important, when reasoning about ownership, to understand whether a permission is duplicable or not.
Back to the concat example, from the point of view of the caller, permissions evolve as follows.
(* xs @ list a * ys @ list a *)
let zs = concat (xs, ys)
(* zs @ list a *)
Here, we set ourselves in the case where a is still a type variable, which is non-duplicable (a could be anything). Incidentally, this means that a list of a is also non-duplicable, as duplicating the list would duplicate the ownership of the elements.
What happens if we pick concrete values for a? If a = ref int, the story remains the same, since list ref int is not duplicable either.
(* xs @ list (ref int) * ys @ list (ref int) *)
let zs = concat (xs, ys)
(* zs @ list (ref int) *)
If, however, we pick a = int, the story becomes different. The list type denotes immutable lists; int also denotes immutable data. Therefore, list int denotes an immutable fragment of the heap; it is therefore a duplicable permission. Hence, the type-checker will automatically save a copy of xs @ list int * ys @ list int before it performs the call to length, meaning that the conjunction is preserved through a call to length.
(* xs @ list int * ys @ list int *)
let zs = concat (xs, ys)
(* zs @ list int *)
This is call-site polymorphism over the duplicability of the argument. Thus, when writing a function type in Mezzo, it is generally advisable to consume your arguments; this puts no extra burden on the caller, and allows them to save a copy of the permission if they have the ability to do so.
Here is an informal set of rules to help you determine whether a type is duplicable or not.
=x is duplicable, as it is just a pointer that contains not ownership information.unknown and empty are both duplicable.(t1, ..., tn) is duplicable if all of its components are.A { f1: t1; ...; fn: tn } is duplicable if A belongs to an immutable data type, and all of its fields are duplicable. B { f1: t1; ...; fn: tn } is exclusive if B belongs to an exclusive data type.a, a type variable introduced by a quantifier, is initially considered affine, that is, neither duplicable or exclusive (as mentioned earlier).ref int are exclusive.(t | P) is duplicable if both t and P are.[a: k] t and {a: k} t are duplicable if, assuming the variable a is affine, the type t is still duplicable.p * q is duplicable if both p and q are.x @ t is duplicable if t is.t -> u are always duplicable.Immutable data types are not mentioned in the list above. They get a special treatment that requires a fixpoint computation. For instance, Mezzo knows that list a is duplicable as long as a itself is duplicable. We omit the details.
Since Mezzo is such a strongly typed language, we devote an entire section on how types are defined in Mezzo.
Data type definition may appear at any top-level position in a .mz file.
Let us start with lists, the classical example of a data type.
data list a =
| Nil
| Cons { head: a; tail: list a }
Data type definitions are introduced by the data keyword; branches are separated using a vertical pipe |. Each branch has a tag, in our case, Nil or Cons, along with a number of fields, listed between braces { ... }. In the case where there are no fields, the { ... } may be omitted.
Defining the list data type allows one to write types such as x @ list int; it also allows one to write two new concrete types. Concrete types describe the in-heap structure of a block; after defining list, one can write x @ Cons { head: ...; tail: ... } to express the fact that x is a memory block of size 3, with a Cons tag, and two fields head and tail. Similarly, after defining the list type, writing x @ Nil also becomes possible.
Unless specified, a data type is considered to be immutable. One can define mutable data types using the mutable keyword. Here is the definition of mutable lists.
data mutable mlist a =
| MNil
| MCons { head: a; tail: mlist a }
Field names can be shared between data types, but constructors shadow each other. We thus use MNil and MCons to make sure one can still talk about Nil and Cons, which belong to list.
Data types are recursive by default. There is currently no option to make a data-type non-recursive. Data types in Mezzo are inductive.
Mutually recursive data types can be defined using the and keyword. Here is a (slightly artificial) example.
data tree a = Tree { size: int; node: node a }
and node a = Empty | Node { left: tree a; contents: a; right: tree a }
The list example admits a parameter. Parameters take a kind annotation. When omitted, the kind defaults to type.
data mutable treeMap k (c : term) a =
TreeMap { tree: tree k a; cmp: =c | c @ (k, k) -> int }
The example above, taken from Mezzo's standard library, showcases a fairly sophisticated data type definition. This is the type of mutable tree maps; it is parameterized of the type of keys k and the type of values a; it also happens to be parameterized by a certain identifier c, which, being a program variable, has kind term.
The program variable c is the comparison function for keys; by parameterizing tree maps over their comparison function, we make sure that the "right" comparison function is always wired to the data type itself, rather than relying on the user providing the correct comparison function at each call of a function operating on tree maps.
A tree map also needs to embed information about the comparison function, namely, that it is a function that compares keys, with type (k, k) -> int. This is done by packing a permission inside the branch, using a vertical bar between braces { ... | ... }. Anything left of the bar is fields; at the right of the bar is a permission.
A canonical example of a type using packed permissions is rich booleans. Rich booleans embed permissions in their False and True branches. Their definition, taken from the Mezzo standard library, is shown below. Note the kind annotations on the type's parameters.
data rich_bool (p : perm) (q: perm) =
| False { | p }
| True { | q }
Since we've defined the list data type, we can now write types of the form Cons { head: a; tail: list a }. This is tedious, though. Fortunately, we can define a type abbreviation.
alias cons a = Cons { head: a; tail: list a }
Type abbreviations are introduced by the alias keyword. They are not recursive. They accept type parameters the same way data type definitions do.
While data types always have kind type, type abbreviations can have kind perm or type. Thus, they take an optional kind annotation.
alias stashed (p: perm) : perm = p
The sections above contain enough information to work define types in Mezzo. We present a few extra features of type definitions; these contain quite a few forward references, so a casual reader may want to skip these upon a first reading of the tutorial. Most of the code snippets from this section are taken from Mezzo's standard library.
Both data type branches and type abbreviations can be prefixed with a succession of existential bindings.
alias channel a =
{q: term} (=q, l: lock (q @ fifo a), condition l)
The definition above also uses a name introduction construct which is syntactic sugar for introducing a type variable. Writing l: ... introduces a new binding for l. The binding is interpreted as being an existential one, and is located as high as possible, while still not crossing any other binders. In the example above, l is bound below q. Thus, the example above is equivalent to:
alias channel a =
{q: term, l: term} (=q, =l, condition l | l @ lock (q @ fifo a))
Both data types and type abbreviations accept variance annotations for their type parameters. Consistently with OCaml, we use + for covariance, - for contravariance. Mezzo automatically computes variance using the definition; annotations in implementations serve as an assertion that the type has the expected variance. Variances annotations mostly appear when defining interfaces.
data mutable fifo +(a: type) =
Empty { length: int; tail: () }
| NonEmpty { length: int; tail: dynamic }
adopts cell a
Mezzo makes it possible to define abstract types. This is useful to axiomatize predicates.
abstract nests (x : term) (p : perm) : perm
fact duplicable (nests x p)
Just like type abbreviations, abstract types take a return kind annotation. They also take an optional fact.
Types can be locally defined via a let-binding. Note the let alias in the snippet below.
val new_generic_iterator [a] (consumes l: list a):
iterator::iterator a (l @ list a) =
let alias post: perm = l @ list a in
iterator::wrap [a, (iterator a post), post]
(new_iterator l, next [a, post], stop [a, post])
This is useful for advanced code that requires a lot of type annotations; defining a local alias avoids repeating the same type too many times.
It is actually possible to define local data types.
alias adopter_ t = ref (list t)
alias dynamic_ = unknown
val take2_ [t] exclusive t => (
parent: adopter_ t,
child: dynamic_
): rich_bool empty (child @ t) =
let data outcome =
| Found { contents: list t | child @ t }
| Not_found { contents: list t }
in
...
The function above needs to perform a search in parent, which is a reference to a list of t. The search is not a classical one, so using list::find is not possible here. We could use the either::either type from the Mezzo standard library, by instantiating it into either::either (list t | child @ t) (list t). For clarity, however, we define a local data type with more meaningful constructor names, namely Found and Not_found.
This feature is to be used with care. Remember that local data types cannot escape their scope.
val x =
let data t = A | B in
A
The example above, when executed, will give the following output:
val x @ A
This is misleading: the constructor A is no longer in scope, so it can't be referenced. The Mezzo printer is currently unable to account for that.
Also, it is unclear what the type of x should be in the example below, since in each branch, the type definitions are distinct.
val x =
if true then begin
let data t = A in
A
end else begin
let data t = A in
A
end
In that case, the type-checker will just keep x @ unknown.
Instead of putting the mutable keyword in front of the data type, one can be more precise.
data tree k a =
| Empty
| mutable Node { left: tree k a; key: k; value: a; right: tree k a; height: int }
This refines the "is duplicable" check for the constructor types of tree, and also limits assignments to the Node case.
A .mz file is made up of an succession of top-level definition. Top-level definitions can be either one of:
Value definitions are introduced by the keyword val, followed by a pattern.
val x, y = 1, 2
Value definitions do not require type annotations.
A function definition is introduced by the val keyword, followed by the function name. Function types are always annotated, meaning that if the function is polymorphic, universal quantifiers should be explicitly specified. The type of the argument is mandatory, as well as the return type of the function. The general form of a function definition is thus:
val f quantifiers? arg_type: return_type =
function_bodyFor instance, here are the first few lines of the list::concat function.
val concat [a] (consumes xs: list a, consumes ys: list a): list a =
...
The type of the argument deserves some explanation. The name introductions, such as xs and ys in the example above, follow the same binding conventions that we explained before. However, they are also interpreted as a pattern that binds new names available in the function body. In other words, xs and ys are names that one can use in a function_body because the example above is understood to be:
val concat [a, r: term] (=r | r @ (list a, list a)): list a =
let xs, ys = r in
...
Pattern are either one of:
(p1, ..., pn)A { f1 = p1; ...; fn = pn }p as xp: t_Mezzo features punning, meaning that a constructor pattern A { f1; ...; fn } will be understood as A { f1 = f1; ...; fn = fn }.
Matches in Mezzo are terminated by an end keyword. We do not (yet) provide special facilities for matching on lists, meaning that the user has to write:
(* x @ list a *)
match x with
| Cons { head; tail } ->
(* x @ Cons { head; tail } * head @ a * tail @ list a *)
...
| Nil ->
(* x @ Nil *)
...
end
The example above uses punning. Matching refines permissions in-place, meaning that in the branch of a match expression, the permission for the expression being match is refined to a more precise one that uses a constructor type. Once a constructor permission is available for x, one may attempt to read and write fields from x.
One can read the field f of variable x by writing f.x. This is well-typed if a permission x @ A { ...; f: t; ... } is available in the environment. The type-checker always expands structural permissions, meaning that reading always consists in adding a new equation into the environment.
let x = Cons { head = 1; tail = Nil } in
(* x @ Cons { head = h; tail = t } * h @ int * t @ Nil *)
let y = x.head in
(* x @ Cons { head = h; tail = t } * h @ int * t @ Nil * y = h *)
...
A constructor B is said to be mutable if the data type is mutable or if the branch it belongs to is declared as mutable.
One can assign an expression e to the field f of variable x by writing f.x <- e. This is well-typed if a permission x @ B { ...; f: t; ... } is available and if constructor B is mutable. In a similar fashion to reading, performing an assignment changes the singleton type for the field of a constructor permission, meaning we preserve the invariant that all types are in expanded form.
let x = MCons { head = 1; tail = Nil } in
(* x @ MCons { head = h; tail = t } * h @ int * t @ Nil *)
x.head <- 2;
(* x @ MCons { head = h'; tail = t } * h @ int * t @ Nil * h' @ int *)
...
One can also change the tag of a constructor. That is, transform x @ A { ... } into x @ B { ... }. This is well-typed as long as A is mutable and both A and B have the exact same number of fields. If B is immutable, the operation turns a mutable piece of memory into an immutable one. This is useful for patterns such as progressive initialization, which we saw in the tail-recursive map example.
(* c0 @ Cell { head = c0_h; tail = c0_t } * c0_h @ b * c0_t @ () * xs @ Nil *)
c0.tail <- xs;
(* c0 @ Cell { head = c0_h; tail = xs } * c0_h @ b * c0_t @ () * xs @ Nil *)
tag of c0 <- Cons
(* c0 @ Cons { head = c0_h; tail = xs } * c0_h @ b * c0_t @ () * xs @ Nil *)
In the example above, c0 is a Cell that is initialized in a gradual fashion: initially, the tail field is not ready. It contains a dummy value: the unit () type. Then, we selectively initialize the tail field of c0, meaning that we are then free to turn it into a Cons cell.
In the examples above, we use constructor types that represent the precise layout of a memory block. These constructor types do not necessarily correspond to a projection of a nominal type. That is, one can write:
let x = Cons { head = (); tail = () } in
(* x @ Cons { head: (); tail: () } *)
...
The permission for x is a perfectly legit one: it represents a memory block of size three. However, it can't be turned into any sort of valid list. One can think of these intermediary states as temporarily broken invariants that are restored when matching a type annotation of the form list a. The type annotation could stem, as an example, from the return type of a function.
Mezzo provides if-then-else expressions. Unlike OCaml, we do not allow the following form:
if e then
let y = ... in
(* sequence of instructions that are parsed into the then-branch *)
else
...In that situation, we require you to use the begin and end keywords for the contents of the then-branch.
Mezzo provides for and while-based loops. The syntax is as follows:
preserving p while e do e;
preserving p for x = e to/downto/below/above e do e;
Both loop constructs are desugared into recursive functions. Since functions cannot close over non-duplicable data, one may want to indicate a permission that will be used and preserved by the loop. This is the purpose of the optional preserving keyword.
Unlike OCaml, we do not use a special do / done construct. If the loop bodies are sequences, they will have to be enclosed in begin / end constructs.
Here are examples of loops.
val square_naive (x: int, p: int): int =
let res = newref 1 in
preserving res @ ref int for i = 1 to p do begin
res := !res * x;
end;
!res
val square_binary (x: int, p: int): int =
let res = newref 1 in
let i = newref 1 in
preserving i @ ref int while !i < p do i := !i * 2;
preserving res @ ref int * i @ ref int while !i > 0 do begin
res := !res * !res;
if (!i & p) <> 0 then
res := !res * x;
i := !i / 2;
end;
!res
In general, loops are less powerful than recursive functions. The usual style in Mezzo consists in using recursive functions wherever possible.
A closure may be introduced either using an anonymous function;
let f = fun (x: int): int = x * x in
...
or using the more traditional form:
let f (x: int): int = x * x in
...
We strongly encourage the user to write functions in an uncurried style, for it makes reasoning about permissions easier.
Functions can only close over immutable data; if a function wants to mutate a piece of data, it should require an extra permission.
val _ =
let x = newref 0 in
let bump_x (| x @ ref int): () =
x := !x + 1;
in
bump_x ();
bump_x ()
The bump_x function above would, in OCaml, be a function from unit () to unit. Here, we need to specify that the function requires an extra permission in order to run; we take advantage of the special syntactic sugar for (() | P) in order to write a concise function signature. Please note that since the consumes keyword is not used, the permission is understood to be preserved by the function, meaning that we can call it several times.
Any sub-expression can be annotated using the : colon operator. We do not support nested type annotations, that is, if there already is a type provided by the context, we won't allow you to re-annotate under it.
Any program can fail at run-time by using the special fail instruction. The programmer can assert the existence of a given permission p by writing assert p.
In the presence of a polymorphic function call, the Mezzo type-checker will try to guess (infer) the value of the polymorphic variable.
open list
val _ =
let l = cons ((1, 2), nil) in
print (length l)
The program above, when run with -warn-error +5 will give:
File "/tmp/snippetf74d11.mz", line 5, characters 15-28:
We instantiated a as (inst→((inst→int::int), (inst→int::int)))
File "/tmp/snippetf74d11.mz", line 6, characters 16-17:
We instantiated a as (inst→((inst→int::int), (inst→int::int)))
File "/tmp/snippetf74d11.mz", line 6, characters 8-18:
We instantiated a as (inst→int::int)
These functions are all polymorphic:
cons @ [a] (a, list a) -> aprint @ [a] a -> ()length @ [a] list a -> intThe type-checker (accurately) guessed that cons was used with type (int, int), just like length. It also guessed that the value we wanted to print was an int.
This mechanism sometimes doesn't work quite well. Because showing a real-world example here would probably scare the reader off, let us consider the example below:
data option a =
| None
| Some { contents: a }
val some [a] (consumes contents: a): option a =
Some { contents }
val x =
let r = newref () in
some [(int | r @ ref ())] 1
Here, the type-checker has no way of figuring out that we wish to obtain x @ option (int | r @ ref ()). The natural choice is having x @ option int. Thus, we perform a type application by providing the expected value for option::some.
The syntax of type applications is either [t1, t2, ...] to instantiate type parameters in the order they were declared. An alternative syntax is available, for convenience: if one wishes to instantiate only the type variable named a, then one can write [a: t].
Existential types are automatically unpacked when added into the context. This means there is no way to refer to "the" existential, as it doesn't have a name.
val f (): {t, u} (t, u) =
1, 2
The function above returns a pair whose two elements have existentially-quantified, distinct types. If one calls f...
val _ =
let z = f () in
(* z @ (t, u) *)
... then types t and u are automatically existentially-quantified and the user has no way to refer to them. This can be fixed by using let flex.
The let flex construct introduces a new unification variable that will be instantiated as needed.
val f (): {t, u} (t, u) =
1, 2
val _ =
let x, y = f () in
(* x @ t * y @ u *)
let flex t' in
assert x @ t';
let flex u' in
assert y @ u'
In the example above, one binds fresh type variables t' and u'; they could serve for anything, but we require them to satisfy x @ t' and y @ u' respectively. This means that they have no choice2 but to instantiate into the existentially-quantified, anonymous variables t and u introduced by the call to f. This henceforth gives us a name that allows us to refer to these variables.
-warn-error +5 command-line argument:
File "/tmp/snippetc78aa2.mz", line 11, characters 2-15:
We instantiated u' as (inst→u)
File "/tmp/snippetc78aa2.mz", line 9, char 2 to line 11, char 15:
We instantiated t' as (inst→t)
val f @ (consumes /root33: ()) -> ({t} {u} (t, u) | /root33 @ ())
If one wants to perform the converse operation, that is, turning a regular type into an existentially-quantified one, one can use the pack instruction.
alias extpair = {t} (t, t)
val f (): extpair =
let z = 1, 2 in
pack z @ extpair witness int;
z
Error messages can be tamed using the -warn-error command-line flag. It follows the OCaml convention: it is a sequence of warning specifiers.
+num enables warning number num-num disables warning number num@num enables and marks as fatal warning number num+num enables warnings in the given range-num disables warnings in the given range@num enables and marks as fatal warnings in the given rangeThe current set of warnings is:
1 (disabled by default) uncertain merge operation, see the paper "The implementation of Mezzo".2 (enabled by default) resource allocation conflict, see the paper "The implementation of Mezzo".3 (enabled by default) no multiple arguments, triggered when performing a curried function application4 (enabled by default) local type, triggered when a permission is dropped because a type would escape its scope,5 (disabled by default) instantiation, prints out the value of an flexible variable when instantiated; the location is the scope of the variable,6 (enabled by default) multiple function types, triggered when several permissions are available for the same function and a function call would work with several of them: the type-checker makes an arbitrary decision then.Error messages are possibly the main weakness of Mezzo. First of all, the Mezzo type-checker is not complete. That is, an error could mean two things: either that your code is ill-typed, or that the inference of the Mezzo type-checker failed. Fortunately, the latter case is rare, and by the time you write such examples, you'll probably be in touch with us. In this section, we focus on error messages that happen when the programmer makes a mistake.
Let's see what happens if we call an uncurried function in a curried style.
File "/tmp/snippetc57b2f.mz", line 6, characters 2-7:
Functions take only one (tuple) argument
File "/tmp/snippetc57b2f.mz", line 6, characters 4-5:
Could not extract from this subexpression (named /x_50) the following type:
(=/root33* | /root33* @ ((=x* | x* @ int::int), (=y* | y* @ int::int)))
some explanations follow:
could not from /x_50 subtract (
=/root33*
| /root33* @ ((=x* | x* @ int::int), (=y* | y* @ int::int))) because none of the following worked:
rule Must-Be-Singleton,
could not subtract: =/x_50 - (
=/root33*
| /root33* @ ((=x* | x* @ int::int), (=y* | y* @ int::int))) because none of the following worked:
rule Wrap-Bar-L,
could not subtract: (=/x_50 | empty) - (
=/root33*
| /root33* @ ((=x* | x* @ int::int), (=y* | y* @ int::int))) because none of the following worked:
rule Bar-vs-Bar,
subtract: =/x_50 - =/root33* using rule Singleton,
subtract: /x_50 - /root33* using rule Flex-R,
prove equality: /root33* = /x_50 using rule Instantiate,
could not subtract: empty - (inst→/x_50) @ (=x*, =y*) ∗
y* @ int::int ∗
x* @ int::int because none of the following worked:
rule Add-Sub,
debug info: t1 = empty t2 = (inst→/x_50) @ (=x*, =y*) ∗
y* @ int::int ∗
x* @ int::int using rule Remaining-Add-Sub,
perform: P = P ∗ empty using rule Add-Sub-Add,
could not subtract a set of permissions (inst→/x_50) @
(=x*, =y*) ∗
y* @ int::int ∗
x* @ int::int because none of the following worked:
rule Perms,
could not subtract permission (inst→/x_50) @ (=x*, =y*) because none of the following worked:
rule Sub-Anchored,
could not from /x_50 subtract (=x*, =y*) because none of the following worked:
rule Try-Perms,
could not subtract: unknown - (=x*, =y*) because no rule was found
rule Try-Perms,
could not subtract: =/x_50 - (=x*, =y*) because no rule was found
rule Try-Perms,
could not subtract: int::int - (=x*, =y*) because no rule was found
The error message above is triggered by trying to type-check the following program:
val f (x: int, y: int): int =
x + 2 * y
val _ =
f 4 5
There are two parts to this error message. The first one is warning 3, which gives us a hint as to what's wrong exactly. We're being lucky.
The second part is the default style of error messages. Indeed, when encountering a type error, the type-checker prints out a typing derivation, that is, it prints a sequence of all the typing rules that it tried to apply in order to justify why a particular operation, in this case a function call, is well-typed.
This error message is difficult to read.
(x: int, y: int) -> int type has been translated into the internal syntax that doesn't have the name introduction construct or the consumes keyword. The internal version of the type of f is the following:
[root33: term, x: term, y: term]
(=root33 | root33 @ ((=x | x @ int), (=y | y @ int)) ->
(int | root33 @ ((=x | x @ int), (=y | @ int)))
4 is given an internal name (/x_50), and the internal name appears.*, this is a type variable whose value we're trying to guess./x_50 @ (=x*, =y*).So, what is happening here? Seeing that f is a function, the type-checker isolates the domain of the function type, that is, the expected type of the argument: (=root33 | root33 @ ((=x | x @ int), (=y | y @ int)). Because root33, x and y are universally quantified, the type-checker turns them into flexible variables. Flexible variables are an implementation tool that makes a type variable "waiting to be instantiated". In practice, we're trying to guess what root33, x and y should be.
The argument is the constant 4 expression, named /x_50. If that function call is going to work, then /x_50 must have type (=root33* | root33* @ ((=x* | x* @ int), (=y* | y* @ int)). In other words, the argument of the function must have the type expected by the function. And that's the operation that failed.
Could not extract from this subexpression (named /x_50) the following type:
(=/root33* | /root33* @ ((=x* | x* @ int::int), (=y* | y* @ int::int)))
some explanations follow:
If we rephrase that error message, the type-checker is merely saying: I cannot obtain the permission /x_50 @ (=/root33* | /root33* @ ((=x* | x* @ int::int), (=y* | y* @ int::int))).
The type-checker is not stuck immediately, though: it figures out that if /x_50 @ (=root33* | ...) must be shown, then we have to instantiate the flexible variable root33 into /x_50:
rule Must-Be-Singleton,
... (more intermediate steps) ...
subtract: =/x_50 - =/root33* using rule Singleton,
subtract: /x_50 - /root33* using rule Flex-R,
prove equality: /root33* = /x_50 using rule Instantiate,
The error happens later on:
could not subtract: empty - (inst→/x_50) @ (=x*, =y*) ∗
Namely, the type-checker can't show /x_50 @ (=x*, =y*), that is, that the argument passed to f is a tuple. This is normal: that's where we made a mistake. The type-checker thus goes through more intermediate steps, then chockes on the final step:
could not from /x_50 subtract (=x*, =y*) because none of the following worked:
rule Try-Perms,
could not subtract: unknown - (=x*, =y*) because no rule was found
rule Try-Perms,
could not subtract: =/x_50 - (=x*, =y*) because no rule was found
rule Try-Perms,
could not subtract: int::int - (=x*, =y*) because no rule was found
Several permissions indeed were available for /x_50: /x_50 @ unknown, /x_50 @ =x_50, as well as /x_50 @ int. None of them allows the type-checker to deduce that /x_50 is a tuple.
TODO
map examplemagic-map exampletail-rec-map exampleTODO
Re-use some example, say, the FIFO.Mezzo is equipped with a primitive module system. A module is comprised of an implementation (a .mz file) and a mandatory interface (a .mzi file).
A signature is made of a succession of items, namely:
val x: t, orFunctions are duplicable values, meaning they can be exported without restrictions. Be aware that the colon in an implementation is replaced by an arrow in an interface:
val f (x: int, y: int): int =
...
becomes, in the interface:
val f: (x: int, y: int) -> int
Type definitions include abstract type definitions, which we saw earlier as a means to axiomatize predicates. They have a more natural use in an interface: using the abstract keyword in an interface makes the corresponding type in the implementation, well, abstract.
(* mutableTreeMap.mz *)
data tree k a =
| Empty
| mutable Node { left: tree k a; key: k; value: a; right: tree k a; height: int }
(* mutableTreeMap.mzi *)
abstract treeMap k (cmp: term) +a
As mentioned earlier, we may want to reveal facts about data types. For instance, we may want to reveal that treeMap is exclusive, or that list a is duplicable as long as a is duplicable. This can be done using the fact mechanism.
fact exclusive (treeMap k cmp a)
Variance annotations can be specified just like we did earlier.
One can refer to a type, value, or constructor defined in another module using m::t, m::x or m::A. One can import all the items defined by module m using open m, a top-level directive.
Unlike OCaml, module names exactly follow the case of the corresponding file.
Interfaces are mandatory. Because of the expressiveness of Mezzo, using strong updates, one may end up with an implementation whose interface cannot be represented using the interface language (e.g. mutual recursion between a value and a type). We feel like extending the interface language to account for that would be a poor design choice; moreover, writing code that prints the inferred signature while detecting non-representable signatures is non-trivial. We thus went for the easy route and require an interface to be present.
Exporting non-duplicable values is tricky. For instance, if the module dependency graph is as follows:
M
/ \
N O
\ /
PLet us now imagine the following contents:
(* m.mzi *)
val r: ref int
(* n.mz *)
open m
val _ =
print (!r + 1);
r := true
(* o.mz *)
open m
val _ =
print (!r + 1);
r := !r + 1
(* p.mz *)
open n
open o
Depending on the linking order, this program may or may not run into a segmentation fault! Thus, we must require that if module n imports module m, then n must not alter the signature of m.
We used to have this check in place, but it turns out that exporting non-duplicable values is never used in practice. We thus removed it.
TODO
Interacting through the MezzoLib. Runtime representation of Mezzo (time to implement slim / fat)?TODO
In-place zipper exampleTODO
existentials (using them, packing them, the auto-unpack feature), let flex, point to articles, etc. Also, mode constraints. Variance, how a -> unit is not covariant (because of the surface syntax hacks). Interaction between OCaml and Mezzo (the restrictions). Declaring environments as inconsistent. Annotation propagation. When to annotate? Merges.TODO
Nesting (use the union-find example). Channels. Locks. Weak references. Etc. etc.Since the type-system of Mezzo is more powerful than that of OCaml, some programs that Mezzo "understands" will not be "understood" by OCaml. In other words, a Mezzo program will generally not type-check in OCaml. We must therefore bypass the OCaml type-checker: this is done by emitting code that uses Obj, the unsafe module of OCaml, which allows one to manipulate the internal representation of objects.↩
Actually, there are several choices for instantiating t': unknown would be a valid choice, just like =x. The type-checker arbitrarily discards these two.↩