This document is a book that describes Motoko, a programming language for the Internet Computer, and more.

Chapter: Introduction

All sections in this chapter are ready for review.

Motoko is a modern language designed to be approachable for programmers who have some basic familiarity with modern object-oriented and/or functional programming idioms in either JavaScript, or another modern programming language, such as Rust, Swift, TypeScript, C# or Java.

Motoko permits modern programming idioms, including special programming abstractions for distributed applications. Each application consists of an actor that communicates with other actors without using shared state, but instead by using (asynchronous) message passing. The actor-based programming abstractions of Motoko permit human-readable message-passing patterns, and they enforce that each network interaction obeys certain rules and avoids certain common mistakes.

Specifically, Motoko programs are type sound since Motoko includes a practical, modern type system that checks each one before it executes. The Motoko type system statically checks that each Motoko program will execute safely, without internal type errors, on all possible inputs. Consequently, entire classes of common programming pitfalls that are common in other languages are ruled out, including null pointer errors, mis-matched argument and result types and many others.

To execute, Motoko statically compiles to WebAssembly, a portable binary format that abstracts cleanly over modern computer hardware, and thus permits its execution broadly on the Internet, and the Internet Computer.

Each microservice as an actor

Motoko provides an actor-based programming model to developers to express server behavior, including that of micro services on the Internet and the Internet Computer.

An actor is similar to an object, but is special in that its isolated state exists remotely, and its interactions with the world are asynchronous.

All communication with and between actors involves passing messages asynchronously over the network using the Internet Computer’s messaging protocol. An actor’s messages are processed in sequence, so state modifications never cause race conditions.

The underlying computing platform provided by the Internet Computer ensures that each message-based synchronization will reach a close, but in doing so each one may also fail due to the usual reasons that arise in distributed systems, including time out.

Asynchronous actors

Like other modern programming languages, Motoko permits an ergonomic syntax for asynchronous communication among components.

In the case of Motoko, each communicating component is an actor.

As an example of using actors, perhaps as an actor ourselves, consider this three-line program:

let result1 = service1.computeAnswer(params);
let result2 = service2.computeAnswer(params);
finalStep(await result1, await result2)

We can summarize the program’s behavior with three steps:

  • i. First, the program makes two requests (lines 1 and 2), to two distinct services, each implemented internally as an actor (object).

  • ii. Next, on line 3, the program waits for these two results to each be ready, using the keyword await on each result value.

  • ii. Finally, on line 3, when both results are available, the program uses them in the final step, calling the function finalStep.

Generally speaking, the services interleave their executions rather than wait for one another, since doing so reduces overall latency. However, if we try to reduce latency this way without special language support, such interleaving will quickly sacrifice clarity and simplicity.

Even in cases where there are no interleaving executions (for example, if there were only one call above, not two), the programming abstractions still permit clarity and simplicity, for the same reason. Namely, they signal to the compiler where to transform the program, freeing the programmer from contorting the program’s logic in order to interleave its execution with the underlying system’s message-passing loop.

Here, the program uses await in step ii (line 3) to express that interleaving behavior in a simple fashion, with human-readable syntax that is provided by Motoko.

In language settings that lack these abstractions, developers would not merely call these two functions directly, but would instead employ very advanced programming patterns, possibly registering developer-provided “callback functions” within system-provided “event handlers”. Each callback would handle an asynchronous event that arises when an answer is ready. This kind of systems-level programming is powerful, but very error-prone, since it decomposes a high-level data flow into low-level system events that communicate through shared state. Sometimes this style is necessary, but here it is not.

Our program instead eschews that (cumbersome, indirect) programming style for this more natural, direct style, where each request resembles an ordinary function call. This simpler, stylized programming form has become increasingly popular for expressing practical systems that interact with an external environment, as most modern software does today. However, it requires special compiler and type-system support, as we discuss in more detail below.

Support for asynchronous behavior

In an asynchronous computing setting, a program and its running environment are permitted to perform internal computations that occur concurrently with one another.

Specifically, asynchronous programs are ones where the program’s requests of its environment do not (necessarily) require the program to wait for the environment. In the meantime, the program is permitted to make internal progress within this environment while it waits, perhaps actively. In the example, above, the program makes the second request while still waiting for the first micro service.

Symmetrically, the environment’s requests of the program do not (necessarily) require the environment to wait for the program’s answer to make external progress around it while it waits for this answer.

We do not show an example of this “notify” pattern above, since it uses callbacks (and higher-order functions and control flow) and is thus more complex. However, we discuss a detailed example later in this text.

Syntactic forms async and await

To address the need for clarity and simplicity, Motoko adopts the increasingly-common program constructs async and await, which afford the programmer a structured language for describing potentially-complex asynchronous dependency graphs.

The syntax async introduces the "`promise`" of asynchronous data in the future (not shown in the first example above). We discuss the introduction of asynchronous promises when we introduce actors.

Here, we merely use the ones that arise from calling service1.computeAnswer(params) and service2.computeAnswer(params).

The syntax await synchronizes on a previously-made promise, and potentially blocks until the future when this promise is fulfilled by its producer. We show two uses of the await form in the example above, which await the results of the two services.

When the developer uses these keywords, the compiler transforms the program as necessary, often doing complex transformations to the program’s control- and data-flow that would be tedious to perform by hand. Meanwhile, the type system of Motoko enforces certain correct usage patterns for these constructs, including that types flowing between consumers and producers always agree, and that the types of data sent among services are permitted to flow there, and do not (for example) contain private mutable state.

Types are static

Like other modern programming languages, Motoko permits each variable to carry the value of a function, object, or a primitive datum (e.g., a string, word or integer). Other types of values exist too, including records, tuples, and “tagged data” called variants.

Motoko enjoys the formal property of type safety, also known as type soundness. We often summarize this idea with the phrase: “Well-typed Motoko programs don’t go wrong”, meaning here that they do not misuse program constructs by treating them as if they have the wrong type.

For example, each variable in a Motoko program carries an associated type, and this type is known statically, before the program executes. Each use of each variable is checked by the compiler to prevent runtime type errors, including null pointer errors.

In this sense, Motoko types provide a form of trusted (compiler-verified) documentation in the program source code.

As usual, dynamic testing can check properties that are beyond the reach of the Motoko type system. While modern, the Motoko type system is intentionally not “advanced” or exotic in any new ways. Rather, the type system of Motoko integrates lessons from modern, but well-understood, practical type systems of today to provide an approachable, yet mathematically precise language for general-purpose, distributed programming.

Motoko engineering values

The design and initial implementation of Motoko each represent established, but ongoing language engineering efforts.

To guide these efforts, we establish the following sets of engineering values, which identify and distinguish our core values from our secondary values, and each of these sets of values from the non-values and non-goals of our efforts on Motoko.

Core values & goals (in order):

  1. Seamless integration with the platform (actors, messaging, persistence, IDL interoperability, …​)

  2. Ergonomics (familiarity, simplicity, clarity, explicitness, persistence, …​)

  3. Correctness (state isolation, sound type system, safety, bignums, pattern matching, "good" defaults/no footguns, …​)

Secondary values & goals (“nice to have”):

  1. Expressiveness, including first-class functions, polymorphism, and pattern matching. (We have each of these already, but more could follow.)

  2. Performance (probably not great, yet.)

  3. Batteries included (libraries, SDK, examples, etc.)

Non-Values & non-goals (“Things we are not focusing on”):

  1. Having a more advanced type system, with more complex types

  2. “Worse is Better”

  3. Interoperability with existing smart contract platforms

Reading this guide

Above, we summarize the core design considerations of Motoko.

Below, we connect these considerations to code examples, starting with the most fundamental concepts first, including the role of types and type annotations in very small programs.

Then, we ramp up quickly to programs that compute in more interesting ways, including function abstractions, user-defined type definitions, user-defined actors, the standard library of collections, and asynchronous communication.

This document is meant to guide readers from many backgrounds through the (evolving) design of Motoko. Yet this document, and the language implementation are each evolving quickly themselves.

Sign posts used in this text

We use “sign posts” to communicate to readers and editors.

This section gives a lists of these sign posts, including their intended audience and meaning.

We will identify sections and chapters where content is ready for review and copyediting as “IMPORTANT” sign post. For example:

Sections X, Y and Z below are ready.
All sections in this chapter are ready.

We will identify places where content is missing using the following sign “CAUTION” post:

Topic X is missing here

We will identify places where content is outdated or stale using the “WARNING” sign post:

Topic X needs to be revised to adhere to concepts A, B and C

We will identify places where content describes future features using the “NOTE” sign post:

Feature X is not yet supported by the platform, but is planned for the future.

Chapter: Basic concepts and terms

All sections in this chapter are ready.

Motoko is designed for distributed programming with actors.

Before considering that ultimate purpose, we first consider the basic building blocks of the language, in so doing, introduce concepts and terms that we use throughout the remainder of this book.

In particular, we introduce terms program, declaration, expression, value, variable, and type.

The use of these terms in Motoko should be unsurprising to anyone familiar with modern programming language theory. For other readers, we introduce these terms gradually, by initially using tiny example programs that eschew any use of actors or distributed programming. After establishing basic terminology, we introduce those more advanced aspects of the language, illustrated with larger examples.

While defining terms, we also review related concepts and keywords:

Motoko programs

Each Motoko program is a free mix of declarations and expressions, whose syntactic classes are distinct, but related (see the appendix for precise program syntax).

For programs that we deploy on the Internet Computer, a valid program consists of an actor expression, introduced with specific syntax (keyword actor) that we discuss in a later chapter.

In preparing for that discussion, we discuss programs in this chapter and the next that are not meant to be Internet Computer services. Rather, these tiny programs illustrate snippets of Motoko for writing those services, and each can (usually) be run on its own as a (non-service) Motoko program, possibly with some printed terminal output.

We begin with simple expressions, such as arithmetic. We encourage advanced readers to skip around, and to use this chart for a quick overview of the full (expression) syntax of Motoko, with additional links and detailed definitions.

For other readers, we start slowly and move gradually. The following snippet consists of two declarations (of variables x and y) followed by an expression, forming a single program:

let x = 1;
let y = x + 1;
x * y + x

We will use variations of this small program in our discussion below.

First, this program’s type is Nat (natural number), and when run, it evaluates to the (natural number) value of 3.

Introducing a block with enclosing braces ({ and }) and another variable (z), we can amend our original program as follows:

let z = {
  let x = 1;
  let y = x + 1;
  x * y + x

Before comparing declaration lists and expressions in more detail, we briefly digress to explain the printNat primitive, used in the final line above.

Printing via print and debug_show

Above, we print the final value using the built-in function printNat:

printNat: Nat -> ()

The function printNat accepts a natural number value (of type Nat) as input, and produces the unit value (of unit type, or ()) as its output.

In a sense, there is no output. The function printNat is impure, and rather than producing an output value, it produces the effect of emitting the natural number in a human-readable form to the output terminal. We discuss the return value (the unit value) in detail below, and relate it to the void type for readers more familiar with that concept.

Likewise, we can print text strings using print:

print: Text -> ()

So that the following program prints "hello world":

print("hello world")

Finally, we can transform most Motoko values into human-readable text strings for debugging purposes, without having to write those transformations by hand.

The debug_show primitive permits converting a large class of values into values of type Text.

For instance, we can convert a triple (of type (Text, Nat, Text)) into debugging text without writing a custom conversion function ourselves:

print(debug_show(("hello", 42, "world")))

Using these text transformations, we can print most Motoko data as we experiment with our programs.

Declarations and expressions

Declarations introduce immutable variables, mutable state, actors, objects, classes and other types. Expressions describe computations that involve these notions.

For now, we use example programs that declare immutable variables, and compute simple arithmetic.

Declarations versus expressions

Recall that each Motoko program is a free mix of declarations and expressions, whose syntactic classes are distinct, but related. In this section, we use examples to illustrate their distinctions and accommodate their intermixing.

Recall our example program, first introduced above:

let x = 1;
let y = x + 1;
x * y + x;

In reality, this program is a declaration list that consists of three declarations:

  1. immutable variable x, via declaration let x = 1;,

  2. immutable variable y, via declaration let y = x + 1;,

  3. and an unnamed, implicit variable holding the final expression’s value, x * y + x.

This expression x * y + x illustrates a more general principle: Each expression can be thought of as a declaration where necessary since the language implicitly declares an unnamed variable with that expression’s result value.

When the expression appears as the final declaration, this expression may have any type. Here, the expression x * y + x has type Nat.

Expressions that do not appear at the end, but rather within the list of declarations must have unit type, as with printing:

let x = 1;
let y = x + 1;
x * y + x;

Use ignore to place non-unit-typed expressions in declaration lists

We can always overcome this unit-type restriction by explicitly using ignore to ignore any unused result values:

let x = 1;
ignore(x + 42);
let y = x + 1;
ignore(y * 42);
x * y + x;

Declarations and variable substitution

Declarations may be mutually recursive, but in cases where they are not, they permit a substitution semantics.

Recall our original example:

let x = 1;
let y = x + 1;
x * y + x;

We may manually rewrite the program above by substituting the variables' declared values for each of their respective occurrences.

In so doing, we produce the following expression, which is also a program:

1 * (1 + 1) + 1

This is also a valid program, of the same type and with the same behavior (result value) as the original program, 3.

We can also form a single expression using a block.

From declarations to block expressions

Many of the programs above each consist of a list of declarations, as with this example, just above:

let x = 1;
let y = x + 1;
x * y + x

A declaration list is not itself (immediately) an expression, so we cannot (immediately) declare another variable with its final value (3).

Block expressions. We can form a block expression from this list of declarations by enclosing it with matching curly braces:

  let x = 1;
  let y = x + 1;
  x * y + x

This is also program, but one where the declared variables x and y are privately scoped to the block we introduced.

This block form preserves the autonomy of the declaration list and its choice of variable names.

Declarations follow lexical scoping

Above, we saw that nesting blocks preserves the autonomy of each separate declaration list and its choice of variable names. Language theorists call this idea lexical scoping. It means that variables' scopes may nest, but they may not interfere as they nest.

For instance, the following (larger, enclosing) program evaluates to 42, not 2, since the final occurrences of x and y, on the final line, refer to the very first definitions, not the later ones within the enclosed block:

let x = 40; let y = 2;
  let x = 1;
  let y = x + 1;
  x * y + x
x + y

Other languages that lack lexical scoping may give a different meaning to this program. However, modern languages universally favor lexical scoping, the meaning given here.

Aside from mathematical clarity, the chief practical benefit of lexical scoping is security, and its use in building compositionally-secure systems. Specifically, Motoko gives very strong composition properties: Nesting your program within one you do not trust cannot, for example, arbitrarily reassociate your variable occurrences with different meanings.

Values and evaluation

Once a Motoko expression receives the program’s (single) thread of control, it evaluates eagerly until it reduces to a (result) value.

In so doing, it will generally pass control to sub-expressions, and to sub-routines before it gives up control from the ambient control stack.

If this expression never reaches a value form, the expression evaluates indefinitely. Later we introduce recursive functions and imperative control flow, which each permit non-termination. For now, we only consider terminating programs that result in values.

In the material above, we focused on expressions that produced natural numbers. As a broader language overview, however, we briefly summarize the other value forms below:

Primitive values

Motoko permits the following primitive value forms:

  • Boolean values (true and false).

  • Integers (…​,-2, -1, 0, 1, 2, …​); Bounded and unbounded variants.

  • Natural numbers (0, 1, 2, …​); Bounded and unbounded variants.

  • Text values --- strings of unicode characters.

  • Words --- fixed-width numbers, without overflow checks, and with explicit wrap-around semantics.

Numbers. By default, integers and natural numbers are unbounded and do not overflow. Instead, they use representations that grow to accommodate any finite number.

For practical reasons, Motoko also includes bounded types for integers and natural numbers, distinct from the default versions. Each bounded variant has a fixed width (one of 8, 16, 32, 64) and each carries the potential for “overflow”. If and when this event occurs, it is an error and causes the program to trap. There are no unchecked, uncaught overflows in Motoko, except in well-defined situations, for specific (Word-based) types.

Word types permit bitwise operations that are unsupported by the other number types. The language provides primitive builtins to inter-convert between these various number representations.

The appendix contains a complete list of primitive types.

Non-primitive values

Building on the primitive values and types above, the language permits user-defined types, and each of the following non-primitive value forms and associated types:

We discuss the use of these forms in the succeeding chapters.

The links above give precise language definitions from the appendix.

The unit type versus the void type

Motoko has no type named void. In many cases where readers may think of return types being “void” from using languages like Java or C++, we encourage them to think instead of the unit type, written ().

In practical terms, like void, the unit value usually carries zero representation cost.

Unlike the void type, there is a unit value, but like the void return value, the unit value carries no values internally, and as such, it always carries zero information.

Another mathematical way to think of the unit value is as a tuple with no elements---the nullary (“zero-ary”) tuple. There is only one value with these properties, so it is mathematically unique, and thus need not be represented at runtime.

Natural numbers

The members of this type consist of the usual values ---0, 1, 2, …​----but, as in mathematics, the members of are not bound to a special maximum size. Rather, the (runtime) representation of these values accommodates arbitrary-sized numbers, making their "overflow" (nearly) impossible. (nearly because it is the same event as running out of program memory, which can always happen for some programs in extreme situations).

Motoko permits the usual arithmetic operations one would expect. As an illustrative example, consider the following program:

let x = 42 + (1 * 37) / 12: Nat

This program evaluates to the value 45, also of type Nat.

Type soundness

Each Motoko expression that type-checks we call well-typed. The type of a Motoko expression serves as a promise from the language to the developer about the future behavior of the program, if executed.

First, each well-typed program will evaluate without undefined behavior. That is, the phrase “well-typed programs don’t go wrong” applies here. For those unfamiliar with the deeper implications of that phrase, it means that there is a precise space of meaningful (unambiguous) programs, and the type system enforces that we stay within it, and that all well-typed programs have a precise (unambiguous) meaning.

Furthermore, the types make a precise prediction over the program’s result. If it yields control, the program will generate a (result) value that agrees with that of the original program.

In either case, the static and dynamic views of the program are linked by and agree with the static type system. This agreement is the central principle of a static type system, and is delivered by Motoko as a core aspect of its design.

The same type system also enforces that asynchrononous interactions agree between static and dynamic views of the program, and that the resulting messages generated "under the hood" never mismatch at run time. This agreement is similar in spirit to the caller/callee argument type and return type agreements that one ordinarily expects in a typed language.

Type annotations and variables

Variables relate (static) names and (static) types with (dynamic) values that are present only at runtime.

In this sense, Motoko types provide a form of trusted, compiler-verified documentation in the program source code.

Consider this very short program:

let x : Nat = 1

In this example, the compiler infers that the expression 1 has type Nat, and that x has the same type.

In this case, we can omit this annotation without changing the meaning of the program:

let x = 1

Except for some esoteric situations involving operator overloading, type annotations do not (typically) affect the meaning of the program as it runs.

If they are omitted and the compiler accepts the program, as is the case above, the program has the same meaning (same behavior) as it did originally.

However, sometimes type annotations are required by the compiler to infer other assumptions, and to check the program as a whole.

When they are added and the compiler still accepts the program, we know that the added annotations are consistent with the existing ones.

For instance, we can add additional (not required) annotations, and the compiler checks that all annotations and other inferred facts agree as a whole:

let x : Nat = 1 : Nat

If we were to try to do something inconsistent with our annotation type, however, the type checker will signal an error.

Consider this program, which is not well-typed:

let x : Text = 1 + 1

The type annotation Text does not agree with the rest of the program, since the type of 1 + 1 is Nat and not Text, and these types are unrelated by subtyping. Consequently, this program is not well-typed, and the compiler will signal an error (with a message and location) and will not compile or execute it.

Type errors and messages

Mathematically, the type system of Motoko is declarative, meaning that it exists independently of any implementation, as a concept entirely in formal logic. Likewise, the other key aspects of the language definition (e.g., its execution semantics) exist outside of an implementation.

However, to design this logical definition, to experiment with it, and to practice making mistakes, we want to interact with this type system, and to make lots of harmless mistakes along the way.

The error messages of the type checker attempt to help the developer when they misunderstand or otherwise misapply the logic of the type system, which is explained indirectly in this book.

These error messages will evolve over time, and for this reason, we will not include particular error messages in this text. Instead, we will attempt to explain each code example in its surrounding prose.

Using the Motoko standard library

For various practical language engineering reasons, the design of Motoko strives to minimize builtin types and operations.

Instead, whenever possible, the Motoko standard library provides the types and operations that make the language feel complete. However, this standard library is still under development, and is still incomplete.

An appendix chapter lists a selection of modules from the Motoko standard library, focusing on core features used in the examples that are unlikely to change radically. However, all of these standard library APIs will certainly change over time (to varying degrees), and in particular, they will grow in size and number.

To import from the standard library, use the import keyword. Give a local module name to introduce, in this example P for “Prelude”, and a URL where the import declaration may locate the imported module:

import P "mo:stdlib/";
P.printLn("hello world");

In this case, we import Motoko code (not some other module form) with the mo: prefix. We specify the stdlib/ path, followed by the module’s file name

Accommodating incomplete code

Sometimes, in the midst of writing a program, we want to run an incomplete version, or a version where one or more execution paths are either missing or simply invalid.

To accommodate these situations, we use the xxx, nyi and unreachable functions from the standard library, explained below. Each wraps a general trap mechanism, explained further below.

Use short-term holes

Short-term holes are never committed to a source repository, and only ever exist in a single development session, for a developer that is still writing the program.

Assuming that earlier, one has imported the prelude as follows:

import P "mo:stdlib/";

The developer can fill any missing expression with the following one:

The result will always type check at compile time, and will always trap at run time, if and when this expression ever executes.

Document longer-term holes

By convention, longer-term holes can be considered "yet not implemented" (nyi) features, and marked as such with a similar function from the prelude:

Document unreachable code paths

In contrast to the situations above, sometimes code will never be filled, since it will never be evaluated, assuming the coherence of the internal logic of the programs' invariants.

To document a code path as logically impossible, or unreachable, use the standard library function unreachable:


As in the situations above, this function type-checks in all contexts, and when evaluated, traps in all contexts.

Execution traps stop the program

Each form above is a simple wrapper around the always-fail use of the assert primitive:

assert false

Dynamically, we call this program-halting behavior a program(-generated) trap, and we say that the program traps when it executes this code. It will cease to progress further.

Overview of program syntax

The appendix has a complete definition of program syntax. In this section, we give a tabular overview of program syntax forms, with links into relevant sections of the book’s (non-appendix) chapters.

Some links are missing below; they should point into the succeeding chapters where each syntactic form is first introduced. Content is missing too (declarations).

Declaration syntax

Missing. See appendix.

Expression syntax





<unop> <exp>

unary operator

<exp> <binop> <exp>

binary operator

<exp> <relop> <exp>

binary relational operator

( <exp>,* )


<exp> . <nat>

tuple projection

? <exp>

option injection

{ <exp-field>;* }


<exp> . <id>

object projection

<exp> := <exp>


<unop>= <exp>

unary update

<exp> <binop>= <exp>

binary update

[ var? <exp>,* ]


<exp> [ <exp> ]

array indexing

<shared>? func <func_exp>

function expression

<exp> <typ-args>? <exp>

function call

{ <dec>;* }


not <exp>


<exp> and <exp>


<exp> or <exp>


if <exp> <exp> (else <exp>)?


switch <exp> { (case <pat> <exp>;)+ }


while <exp> <exp>

while loop

loop <exp> (while <exp>)?


for ( <pat> in <exp> ) <exp>


label <id> (: <typ>)? <exp>


break <id> <exp>?


continue <id>


return <exp>?


async <exp>

async expression

await <exp>

await future (only in async)

throw <exp>

raise an error (only in async)

try <exp> catch <pat> <exp>

catch an error (only in async)

assert <exp>


<exp> : <typ>

type annotation



( <exp> )


Chapter: Mutable state

Each actor in Motoko may use, but may never directly share, an internal mutable state.

Later, we discuss sharing among actors, where actors send and receive immutable data, and also handles to each others external entry points, which serve as shareable functions. Unlike those cases of shareable data, a key Motoko design invariant is that mutable data is kept internal (private) to the actor that allocates it, and is never shared remotely.

In this chapter, we continue using minimal examples to show how to introduce (private) actor state, and use mutation operations to change it over time.

In the next chapter, we introduce the syntax for local objects, and a minimal counter actor with a single mutable variable. In the following chapter, we show an actor with the same behavior, exposing the counter variable indirectly behind an associated service interface for using it remotely.

Immutable versus mutable variables

The var syntax declares mutable variables in a declaration block:

let txt  : Text = "abc"
let num  : Nat = 30

var pair : (Text, Nat) = (txt, num)
var txt2 : Text = txt

The declaration list above declares four variables. The first two variables (txt and num) are lexically-scoped, immutable variables. The final two variables (pair and txt2) are lexically-scoped, mutable variables.

Assignment to mutable memory

Mutable variables permit assignment, and immutable variables do not.

If we try to assign new values to either txt or num above, we will get static type errors; these variables are immutable.

However, we may freely update the value of mutable variables pair and txt2 using the syntax for assignment, written as :=, as follows:

text2 := text2 # "xyz"
pair := (text2, pair.1)

Above, we update each variable based on applying a simple “update rule” to their current values (for example, we update text2 by appending string constant "xyz" to its suffix). Likewise, an actor processes some calls by performing updates on its internal (private) mutable variables, using the same assignment syntax as above.

Special assignment operations

The assignment operation := is general, and works for all types.

Motoko also includes special assignment operations that combine assignment with a binary operation. The assigned value uses the binary operation on a given operand and the current contents of the assigned variable.

For example, numbers permit a combination of assignment and addition:

var num2 = 2;
num2 += 40;

After the second line, the variable num2 holds 42, as one would expect.

Motoko includes other combinations as well. For example, we can rewrite the line above that updates text2 more concisely as:

text2 #= "xyz"

As with +=, this combined form avoids repeating the assigned variable’s name on the right hand side of the (special) assignment operator #=.

The full list of assignment operations lists numerical, logical, and textual operations over appropriate types (number, boolean and text values, respectively).

Reading from mutable memory

When we updated each variable, we also first read from the mutable contents, with no special syntax.

This illustrates a subtle point: Each use of a mutable variable looks like the use of an immutable variable, but does not act like one. In fact, its meaning is more complex. As in many languages (JavaScript, Java, C#, etc.), but not all, the syntax of each use hides the memory effect that accesses the memory cell identified by that variable, and gets its current value. Other languages from functional traditions (SML, OCaml, Haskell, etc), generally expose these effects syntactically.

Below, we explore this point in detail.

Understanding var- versus let-bound variables

Consider the following two variable declarations, which look similar:

let x : Nat = 0


var x : Nat = 0

The only difference in their syntax is the use of keyword let versus var to define the variable x, which in each case the program initializes to 0.

However, these programs carry different meanings, and in the context of larger programs, the difference in meanings will impact the meaning of each occurrence of x.

For the first program, which uses let, each such occurrence means 0. Replacing each occurrence with 0 will not change the meaning of the program.

For the second program, which uses var, each occurrence means: “read and produce the current value of the mutable memory cell named x.” In this case, each occurrence’s value is determined by dynamic state: the contents of the mutable memory cell named x.

As one can see from the definitions above, there is a fundamental contrast between the meanings of let-bound and var-bound variables.

In large programs, both kinds of variables can be useful, and neither kind serves as a good replacement for the other.

However, let-bound variables are more fundamental.

To see why, consider encoding a var-bound variable using a one-element, mutable array, itself bound using a let-bound variable.

For instance, instead of declaring x as a mutable variable initially holding 0, we could instead use y, an immutable variable that denotes a mutable array with one entry, holding 0:

var x : Nat       = 0
let y : [var Nat] = [var 0]

We explain mutable arrays in more detail below.

Unfortunately, the read and write syntax required for this encoding reuses that of mutable arrays, which is not as readable as that of var-bound variables. As such, the reads and writes of variable x will be easier to read than those of variable y.

For this practical reason, and others, var-bound variables are a core aspect of the language design.

Immutable arrays

Before discussing mutable arrays, we introduce immutable arrays, which share the same projection syntax, but do not permit mutable updates (assignments) after allocation.

Allocate an immutable array of constants

let a : [Nat] = [1, 2, 3] ;

The array a above holds three natural numbers, and has type [Nat]. In general, the type of an immutable array is [_], using square brackets around the type of the array’s elements, which must share a single common type, in this case Nat.

Project from (read from) an array index

We can project from (read from) an array using the usual bracket syntax ([ and ]) around the index we want to access:

let x : Nat = a[2] + a[0] ;

Every array access in Motoko is safe. Accesses that are out of bounds will not access memory unsafely, but instead will cause the program to trap, as with an assertion failure.

Allocate an immutable array with varying content

Above, we showed a limited way of creating immutable arrays.

In general, each new array allocated by a program will contain a varying number of varying elements. Without mutation, we need a way to specify this family of elements "all at once", in the argument to allocation.

To accommodate this need, the Motoko language provides the higher-order array-allocation primitive Array_tabulate, which allocates a new array by consulting a user-provided "generation function" gen for each element.

Array_tabulate<T>(len : Nat,  gen : Nat -> T) : [T]

Function gen specifies the array as a function value of arrow type Nat → T, where T is the final array element type.

The function gen actually functions as the array during its initialization: It receives the index of the array element, and it produces the element (of type T) that should reside at that index in the array. The allocated output array populates itself based on this specification.

For instance, we can first allocate array1 consisting of some initial constants, and then functionally-update some of the indices by "changing" them (in a pure, functional way), to produce array2, a second array that does not destroy the first.

let array1 : [Nat] = [1, 2, 3, 4, 6, 7, 8]

let array2 : [Nat] = Array_tabulate<Nat>(42, func(i:Nat) : Nat {
               if ( i == 2 or i == 5 ) { array1[i] * i } // change 3rd and 6th entries
               else { array1[i] } // no change to other entries

Even though we "changed" array1 into array2 in a functional sense, notice that both arrays and both variables are immutable.

Next, we consider mutable arrays, which are fundamentally distinct.

Mutable arrays

Above, we introduced immutable arrays, which share the same projection syntax as mutable arrays, but do not permit mutable updates (assignments) after allocation. Unlike immutable arrays, each mutable array in Motoko introduces (private) mutable actor state.

Because Motoko’s type system enforces that remote actors do not share their mutable state, the Motoko type system introduces a firm distinction between mutable and immutable arrays that impacts typing, subtyping and the language abstractions for asynchronous communication.

Locally, the mutable arrays can not be used in places that expect immutable ones, since Motoko’s definition of subtyping for arrays (correctly) distinguishes those cases for the purposes of type soundness. Additionally, in terms of actor communication, immutable arrays are safe to send and share, while mutable arrays can not be shared or otherwise sent in messages. Unlike immutable arrays, mutable arrays have non-shareable types.

Allocate a mutable array of constants

To indicate allocation of mutable arrays (in contrast to the forms above, for immutable ones), the mutable array syntax [var _] uses the var keyword, in both the expression and type forms:

let a : [var Nat] = [var 1, 2, 3] ;

As above, the array a above holds three natural numbers, but has type [var Nat].

Allocate a mutable array with dynamic size

To allocate mutable arrays of non-constant size, use the Array_init primitive, and supply an initial value:

func Array_init<T>(len : Nat,  x : T) : [var T]

For example:

var size : Nat = 42 ;
let x : [var Nat] = Array_init<Nat>(size, 3);

The variable size need not be constant here; the array will have size number of entries, each holding the initial value 3.

Mutable updates

Mutable arrays, each with type form [var _], permit mutable updates via assignment to an individual element, in this case element index 2 gets updated from holding 3 to instead hold value 42:

let a : [var Nat] = [var 1, 2, 3] ;
a[2] := 42 ;

Subtyping does not permit mutable to be used as immutable

subtyping in Motoko does not permit us to use a mutable array of type [var Nat] in places that expect an immutable one of type [Nat].

There are two reasons for this. First, as with all mutable state, mutable arrays require different rules for sound subtyping. In particular, mutable arrays have a less flexible subtyping definition, necessarily. Second, Motoko forbids uses of mutable arrays across asynchronous communication, where mutable state is never shared.

The Array module

The Motoko standard library provides additional array operations.

Many common operations for arrays reside in the standard library, since the the Motoko language intentionally places features that can be written in Motoko into this library, and not the set of compiler and language builtin features.

Chapter: Local objects and classes

In addition to (remote) actor objects, Motoko provides local objects that are similar in their syntax, typing and evaluation to ordinary (local) objects from object-oriented programming.

The prior chapter introduced declarations of private mutable state, in the form of var-bound variables and (mutable) array allocation. In this chapter, we use mutable state to implement simple objects, a la object-oriented programming.

We illustrate this support via a running example, which continues in the following chapter. This example illustrates a general evolution path for Motoko programs: Each object, if important enough, has the potential to be refactored into an Internet service, by refactoring this (local) object into an actor object.

Example: The counter object

Consider the following object declaration of the object value counter:

object counter = {
  var count = 0;
  public func inc() { count += 1 };
  public func read() : Nat { count };
  public func bump() : Nat {

This declaration introduces a single object instance named counter, whose entire implementation is given above.

In this example, the developer exposes three public functions inc, read and bump using keyword public to declare each in the object body. The body of the object, like a block expression , consists of a list of declarations.

In addition to these three functions, the object has one (private) mutable variable count, which holds the current count, initially zero.

Object types

This object counter has the following object type type, written as a list of field-type pairs, enclosed in braces ({ and }):

  inc  : () -> () ;
  read : () -> Nat ;
  bump : () -> Nat ;

Each field type consists of an identifier, a colon :, and a type for the field content. Here, each field is a function, and thus has an arrow type form (_ → _).

In the declaration of object, the variable count was explicitly declared neither as public nor as private.

By default, all declarations in an object block are private, as is count here. Consequently, the type for count does not appear in the type of the object, and its name and presence are both inaccessible from the outside.

The inaccessibility of this field comes with a powerful benefit: By not exposing this implementation detail, the object has a more general type (fewer fields), and as a result, is interchangeable with objects that implement the same counter object type differently, without using such a field.

Example: The byte_counter object

To illustrate the point just above, consider this variation of the counter declaration above, of byte_counter:

object byte_counter = {
  var count : Nat8 = 0;
  public func inc() { count += 1 };
  public func read() : Nat { nat8ToNat(count) };
  public func bump() : Nat { inc(); read() };

This object has the same type as the previous one, and thus from the standpoint of type checking, this object is interchangeable with the prior one:

  inc  : () -> () ;
  read : () -> Nat ;
  bump : () -> Nat ;

Unlike the first version, however, this version does not use the same implementation of the counter field. Rather than use an ordinary natural Nat that never overflows, but may also grow without bound, this version uses a byte-sized natural number (type Nat8) whose size is always eight bits.

As such, the inc operation may fail with an overflow for this object, but never the prior one, which may instead (eventually) fill the program’s memory, a different kind of application failure.

Neither implementation of a counter comes without some complexity, but in this case, they share a common type.

In general, a common type shared among two implementations (of an object or service) affords the potential for the internal implementation complexity to be factored away from the rest of the application that uses it. Here, the common type abstracts over the simple choice of a number’s representation. In general, the implementation choices would each be more complex, and more interesting.

Object subtyping

To illustrate the role and use of object subtyping in Motoko, consider implementing a simpler counter with a more general type (fewer public operations):

object bump_counter = {
  var c = 0; public func bump() : Nat { c += 1; c };

The object bump_counter has the following object type, exposing exactly one operation, bump:

{ bump : () -> Nat }

This type exposes the most common operation, and one that only permits certain behavior. For instance, the counter can only ever increase, and can never decrease or be set to an arbitrary value.

In other parts of a system, we may in fact implement and use a less general version, with more operations:

full_counter : {
  inc   : () -> () ;
  read  : () -> Nat ;
  bump  : () -> Nat ;
  write : Nat -> () ;

Here, we consider a counter named full_counter with a less general type than any given above. In addition to inc, read and bump, it additionally includes write, which permits the caller to change the current count value to an arbitrary one, such as back to 0.

Object subtyping. In Motoko, objects have types that may relate by subtyping, as the various types of counters do above. As is standard, types with more fields are less general (are subtypes of) types with fewer fields. For instance, we can summarize the types given in the examples above as being related in the following subtyping order:

  • Most general:

{ bump : () -> Nat }
  • Middle generality:

  inc  : () -> () ;
  read : () -> Nat ;
  bump : () -> Nat ;
  • Least generality:

  inc  : () -> () ;
  read : () -> Nat ;
  bump : () -> Nat ;
  write : Nat -> () ;

If a function expects to receive an object of the first type ({ bump : () → Nat }), any of the types given above will suffice, since they are each equal to, or a subtype of, this (most general) type.

However, if a function expects to receive an object of the last, least general type, the other two will not suffice, since they each lack the needed write operation, to which this function rightfully expects to have access.

As aside for language theorists and advanced readers: Object subtyping in Motoko uses structural subtyping, not nominal subtyping. Recall that in nominal typing, the question of two types equality depends on choosing consistent, globally-unique type names (across projects and time). In Motoko, the question of two types' equality is based on their structure, not their names.

Subtyping in general. Formally, subtyping relationships in Motoko extend to all types, not just object types. Most cases are standard, and follow conventional programming language theory (for structural subtyping, specifically). Other notable cases in Motoko for new programmers include arrays, options, variants and number type inter-relationships.

Object classes

to do: examples and prose here

Chapter: Actors and async data

Each Motoko actor represents a service that one might want to deploy on the Internet Computer.

The interface of each actor introduces async data whenever it returns information to its caller. This programming abstraction serves a key role in Motoko, as it coordinates with the transformations of the Motoko compiler pipeline and eventual execution behavior of Motoko actors on the Internet Computer.

This abstraction represents a promise from the system to the caller, on behalf of the callee:

  • Either the async value, when awaited, will yield a value from the callee of the expected type,

  • or, an error --- system-level or callee-level --- will eventually arise.

In general, the caller may not immediately await each call. But even in cases when they do, they use the same async and await abstractions, for the same reason: To maintain the illusion of call-return, direct-style control flow, as supported by the Motoko compiler’s transformations.

Technical aside. In reality, the underlying message-passing of the system forces the program’s logic into another form. Specifically, control flow around each actor method call involves the program loosing control to a system-level message-processing loop, which forces the program’s logic into a so-called "continuation-passing-style" (CPS) to expose event-handling "callback functions". This program structure is complex for humans to read and maintain, and stands in stark contrast to the direct style most prefer for most program logic.

We note that Motoko programs may avoid callbacks for many cases, but not all cases where they are used in other asynchronous, message-passing settings. Notably, callbacks are still needed when they serve as a fundamental aspect of the service’s interface, as with a notification service, where users register with the service to get notified some times later, when some predetermined class of events, occur over time.

To start, we consider the simplest stateful service: A counter with a single "current count" value.

Example: a Counter service

Consider the following actor object (a value form):

actor Counter {
  var count : Nat = 0;

  public func increment() : async () {
    count += 1;

  public query func get_current() : async Nat {

  public func set_current(n: Nat) : async () {
    count := n;
todo: discuss counter example

Using async values by await-ing their answer values

To get the underlying content of an async value, such as a return value from get_current above, the caller uses await:

let a : async Nat = counter.get_current()
let c : Nat = await(counter.get_current())

The first line gets a promise of the current value (the variable a), but does not wait for it, and thus cannot use it as a natural number.

The second line immediately inspects this promise and gets the natural number, or waits until it is ready.

For now, the Motoko compiler gives an error for calls that do not follow this second form, which is currently required to ensure that certain program resources will always be reclaimed.

Actor classes generalize an actor’s initial state

An actor class defines a constructor function that produces objects of a predetermined type, with a predetermined interface and behavior.

For example, we can generalize Counter given above to CounterInit below, by introducing a constructor parameter, variable init of type Nat:

actor class CounterInit(init: Nat) {
  var count : Nat = init;

  public func increment() : async () {
    count += 1;

  public query func get_current() : async Nat {

  public func set_current(n: Nat) : async () {
    count := n;

To use this class, we can create several actors with different initial values:

let c1 = CounterInit(1);
let c2 = CounterInit(2);

The two lines above instantiate the actor class twice, once per line. The first invocation uses the initial value 1, where the second uses initial value 2. Their interface is common, and in terms of their types, they are compatible and can be used interchangeably.

For now, the Motoko compiler gives an error when compiling programs that do not consist of a single actor. The interpreter accommodates the examples above.

Chapter: Errors and optional results

Not complete

to do:

  • ground the concepts: Errors as return values versus errors via special, exceptional control flow

  • this chapter introduces special uses of switch and try constructs

  • switch supports general pattern-matching; point to broader discussion of switch and pattern matching (next chapter)

  • handle errors as values with switch (not with try)

  • design question in an API: When to use which?

  • handle errors as exceptions with try --- in a way, these are less general for API design; may only appear in certain (async) contexts. But they can recover from errors that would otherwise be fatal (such as system errors), so they are necessary.

  • discuss programming examples:

  • discuss use of Result module, with examples

  • discuss use of Option module, with examples

  • discuss use of Error type; exceptions versus traps (is there a difference?)

Chapter: Pattern matching

Not complete

to do:

  • errors and optional results are special cases of pattern matching; this chapter covers all types; interested readers can jump ahead and back as needed.

  • point: unhandled errors are a special case of non-exhaustive pattern match (for results and option types)

  • point: null-pointer errors are a special case of non-exhaustive pattern match

  • the Motoko type checker statically enforces exhaustive pattern matches for all optional types (and variants); hence, null-pointer errors are ruled out statically, and are impossible dynamically.

Chapter: Sharing among distinct actors

Not complete

Shared data

Shared functions

Example: Notification service

Not complete (todo: simple example of a callback-using service)

Chapter: Modules and imports

Not complete

to do:

  • discuss use of module keyword

  • discuss use of import keyword

Chapter: Imperative control flow

Not complete

to do:

  • discuss return

  • discuss labels and labeled gotos

  • discuss use of for loops

  • discuss iterators; discuss examples of iterating an array and iterating a text value (.keys, .vals, .chars, .len, etc.)

  • discuss use of while loops

  • discuss use of do loops

Using range with a for loop

The range function produces an iterator (of type Iter) with the given lower and upper bound, inclusive.

The following loop example prints the numbers 0 through 10 over its eleven iterations:

var i = 0;
for (j in range(0, 10)) {
 assert(j == i);
 i += 1;
assert(i == 11);

More generally, the function range is a class that constructs iterators over sequences of natural numbers. Each such iterator has type Iter<Nat>.

As a constructor function, range has a function type:

(lower:Nat, upper:Nat) -> Iter<Nat>

Where Iter<Nat> is an iterator object type with a next method that produces optional elements, each of type ?Nat:

type Iter<Nat> = {next : () -> ?Nat};

For each invocation, next returns an optional element (of type ?Nat).

The value null indicates that the iteration sequence has terminated.

Until reaching null, each non-null value, of the form ?n for some number n, contains the next successive element in the iteration sequence.

Using revrange

Like range, the function revrange is a class that constructs iterators (each of type Iter). As a constructor function, it has a function type:

(upper:Nat, lower:Nat) -> Iter

Unlike range, the revrange function descends in its iteration sequence, from an initial upper bound to a final lower bound.

Chapter: Advanced discussion topics

Not complete

To do:

  • discuss: no race conditions

  • discuss: no null-pointer exceptions

  • discuss: Subtypes and the Null type

  • discuss: Types are structural

Appendix Chapter: Standard library

Not complete:

See each chapter section below for:

Compiler prelude

The compiler itself contains a prelude in every program, effectively extending the language definition with a set of types and declarations that are always available.

In addition to these in-built compiler definitions, the prelude of the standard library contributes some additional functions in a supplemental Prelude module.

In contrast to those definitions, the compiler prelude definitions here are always present, and do not require any import declaration to bring them into the current scope.

type Iter

type Iter<T_> = {next : () -> ?T_};

function abs

func abs(x : Int) : Nat ;

function ignore

func ignore(_ : Any) {};

function range

class range(x : Nat, y : Nat) {
  var i = x;
  public func next() : ?Nat { if (i > y) null else {let j = i; i += 1; ?j} };

function revrange

class revrange(x : Nat, y : Nat) {
  var i = x + 1;
  public func next() : ?Nat { if (i <= y) null else {i -= 1; ?i} };


func printNat(x : Nat) ;
func printInt(x : Int) ;
func printChar(x : Char) ;
func print(x : Text) ;

RTS version

func rts_version() : Text ;


func hashInt(x : Int) : Word32 ;
func idlHash(x : Text) : Word32 ;

Number conversions

func int64ToInt(n : Int64) : Int ;
func intToInt64(n : Int) : Int64 ;
func int64ToWord64(n : Int64) : Word64 ;
func word64ToInt64(n : Word64) : Int64 ;
func int32ToInt(n : Int32) : Int ;
func intToInt32(n : Int) : Int32 ;
func int32ToWord32(n : Int32) : Word32 ;
func word32ToInt32(n : Word32) : Int32 ;
func int16ToInt(n : Int16) : Int ;
func intToInt16(n : Int) : Int16 ;
func int16ToWord16(n : Int16) : Word16 ;
func word16ToInt16(n : Word16) : Int16 ;
func int8ToInt(n : Int8) : Int ;
func intToInt8(n : Int) : Int8 ;
func int8ToWord8(n : Int8) : Word8 ;
func word8ToInt8(n : Word8) : Int8 ;

func nat64ToNat(n : Nat64) : Nat ;
func natToNat64(n : Nat) : Nat64 ;
func nat64ToWord64(n : Nat64) : Word64 ;
func word64ToNat64(n : Word64) : Nat64 ;
func nat32ToNat(n : Nat32) : Nat ;
func natToNat32(n : Nat) : Nat32 ;
func nat32ToWord32(n : Nat32) : Word32 ;
func word32ToNat32(n : Word32) : Nat32 ;
func nat16ToNat(n : Nat16) : Nat ;
func natToNat16(n : Nat) : Nat16 ;
func nat16ToWord16(n : Nat16) : Word16 ;
func word16ToNat16(n : Word16) : Nat16 ;
func nat8ToNat(n : Nat8) : Nat ;
func natToNat8(n : Nat) : Nat8 ;
func nat8ToWord8(n : Nat8) : Word8 ;
func word8ToNat8(n : Word8) : Nat8 ;

func natToWord8(n : Nat) : Word8 ;
func word8ToNat(n : Word8) : Nat ;
func intToWord8(n : Int) : Word8 ;
func word8ToInt(n : Word8) : Int ;

func natToWord16(n : Nat) : Word16 ;
func word16ToNat(n : Word16) : Nat ;
func intToWord16(n : Int) : Word16 ;
func word16ToInt(n : Word16) : Int ;

func natToWord32(n : Nat) : Word32 ;
func word32ToNat(n : Word32) : Nat ;
func intToWord32(n : Int) : Word32 ;
func word32ToInt(n : Word32) : Int ;

func natToWord64(n : Nat) : Word64 ;
func word64ToNat(n : Word64) : Nat ;
func intToWord64(n : Int) : Word64 ;
func word64ToInt(n : Word64) : Int ;

func charToWord32(c : Char) : Word32 ;
func word32ToChar(w : Word32) : Char ;

func charToText(c : Char) : Text ;

// Exotic bitwise operations
func popcntWord8(w : Word8) : Word8 ;
func clzWord8(w : Word8) : Word8 ;
func ctzWord8(w : Word8) : Word8 ;
func btstWord8(w : Word8, amount : Word8) : Bool ;

func popcntWord16(w : Word16) : Word16 ;
func clzWord16(w : Word16) : Word16 ;
func ctzWord16(w : Word16) : Word16 ;
func btstWord16(w : Word16, amount : Word16) : Bool ;

func popcntWord32(w : Word32) : Word32 ;
func clzWord32(w : Word32) : Word32 ;
func ctzWord32(w : Word32) : Word32 ;
func btstWord32(w : Word32, amount : Word32) : Bool ;

func popcntWord64(w : Word64) : Word64 ;
func clzWord64(w : Word64) : Word64 ;
func ctzWord64(w : Word64) : Word64 ;
func btstWord64(w : Word64, amount : Word64) : Bool ;

Array utilities

func Array_init<T>(len : Nat,  x : T) : [var T] ;

func Array_tabulate<T>(len : Nat,  gen : Nat -> T) : [T] ;

Error utilities

// these will change
type ErrorCode = {#error; #system}; /* TBC */

func error(message : Text) : Error ;

func errorCode(e : Error) : ErrorCode ;

func errorMessage(e : Error) : Text ;

type Result<T> = {#ok : T; #error : Error};

module Prelude

This standard library prelude module supplements the compiler prelude with additional features that do not require (additional) special compiler support.


Print text followed by a newline.

public func printLn(x : Text)

nyi (not yet implemented)

Mark incomplete code with the nyi and xxx functions.

Each have calls are well-typed in all typing contexts, which trap in all execution contexts.

public func nyi() : None

public func xxx() : None


Mark unreachable code with the unreachable function.

Calls are well-typed in all typing contexts, and they trap in all execution contexts.

public func unreachable() : None

module Result

The result of a computation that may contain errors, exceptions, etc.

Similar to the same concept of the same name in Rust. We use the Rust nomenclature for the datatype and its constructors.

public type Result<Ok, Err> = {
  #ok: Ok;
  #err: Err;


assert that we can unwrap the result; should only be used in tests, not in canister implementations. This will trap.

public func assertUnwrap<Ok, Error>(r: Result<Ok, Error>) : Ok


public func assertUnwrapAny<Ok>(r: Result<Ok, Any>) : Ok


public func assertOk(r: Result<Any, Any>)


public func assertErr(r: Result<Any, Any>)


public func assertErrIs<E>(r: Result<Any, E>, f: E->Bool) : Bool


public func assertErrAs<E, X>(r:Result<Any, E>, f: E->X) : X


bind operation in result monad.

public func bind<R1, R2, Error>(
  x:Result<R1, Error>,
  y:R1 -> Result<R2, Error>) : Result<R2, Error>


map the Ok type/value, leaving any Error type/value unchanged.

public func mapOk<Ok1, Ok2, Error>(
  x: Result<Ok1, Error>,
  y: Ok1 -> Ok2) : Result<Ok2, Error>


create a result from an option, including an error value to handle the null case.

public func fromOption<R, E>(x: ?R, err: E) : Result<R, E>


map the Ok type/value from the optional value, or else use the given error value.

public func fromSomeMap<R1, R2, E>(x: ?R1, f: R1->R2, err:E) : Result<R2, E>


asserts that the option is Some(_) form.

public func fromSome<Ok>(o: ?Ok) : Result<Ok, None>


a result that consists of an array of Ok results from an array of results, or the first error in the result array, if any.

public func joinArrayIfOk<R, E>(x: [Result<R, E>]) : Result<[R], E>

module Option

Type definition

import P "";

public type t<A> = ?A;


Returns true if the value is not null.

public func isSomeAny(x: ?Any): Bool

public func isSome<A>(x: t<A>): Bool


Returns true if the value is null.

public func isNullAny(x: ?Any): Bool = not isSome<Any>(x);

public func isNull<A>(x: t<A>): Bool = not isSome<A>(x);


Unwrap an optional value, and fail if it is null.

public func unwrap<T>(x: ?T): T


Unwrap an optional value or a default.

public func unwrapOr<T>(x: ?T, d: T): T


Unwrap an optional value. If null, return the default, else, apply the function to the unwrapped value.

public func option<A, B>(x: ?A, f: A->B, d: B): B


Apply a function to the wrapped value.

public func map<A, B>(f: A->B, x: ?A): ?B


Assert that the given value is not null; ignore this value and return unit.

public func assertSomeAny(x: ?Any) : ()
public func assertSome<A>(x: ?A)   : ()


Assert that the given value is null; ignore this value and return unit.

public func assertNullAny(x: ?Any) : ()
public func assertNull<A>(x: ?A)   : ()


Print an optional integer.

public func printOpInt(x : ?Int) : ()


public func apply<A, B>(f : ?(A -> B), x : ?A) : ?B


public func bind<A, B>(x : ?A, f : A -> ?B) : ?B


public func join<A>(x : ??A) : ?A


public func pure<A>(x: A) : ?A

module Hash

Hash values represent a string of hash bits, and support associated bit string operations.

Representations for Hash type

We consider two representations for a hash value:

  • as a linked list of booleans, as BitList below; or,

  • as a bit vector packed into a Word type (specifically, Word32).


Bit lists are closest to the mathematical definition of finite, but unbounded bit strings.

However, for practical applications, a bit vector provides (much) more efficient operations over a bit list, but limits the length of each bit string to that of a word.

For this reason, we recommend using bit vectors for hash values, and other practical situations. We define the type Hash below as such.

Canonical representations

We choose a canonical representation of hash values for the rest of the standard library to use, based on the (more efficient) bit vector representation:

public type Hash = BitVec;
public let Hash = BitVec;

A "bit string" as a linked list of bits:

public type BitList = ?(Bool, BitList);

A "bit vector" is a bounded-length bit string packed into a single word:

public type BitVec = Word32;
module BitVec

A "bit vector" is a bounded-length bit string packed into a single word.

 public type t = BitVec ;

 public func hashWord8s(key:[BitVec]) : BitVec ;

 public func length() : Nat ;

 public func hashOfInt(i:Int) : BitVec ;

 public func hashOfIntAcc(h1:BitVec, i:Int) : BitVec ;

 public func hashOfText(t:Text) : BitVec ;

Project a given bit from the bit vector:

 public func getHashBit(h:BitVec, pos:Nat) : Bool ;

Test if two lists of bits are equal:-

public func hashEq(ha:BitVec, hb:BitVec) : Bool ;


 public func bitsPrintRev(bits:BitVec) ;

 public func hashPrintRev(bits:BitVec) ;

 public func toList(v:BitVec) : BitList ;
module BitList

Encode hashes as lists of booleans.

public type t = BitList;

public func hashOfInt(i:Int) : BitList ;

Test if two lists of bits are equal.

public func getHashBit(h:BitList, pos:Nat) : Bool ;

Test if two lists of bits are equal.

public func hashEq(ha:BitList, hb:BitList) : Bool ;


public func bitsPrintRev(bits:BitList) ;

public func hashPrintRev(bits:BitList) ;

module Array

The design of Motoko strives to minimize builtin operations, and whenever possible, to instead implement array operations as Motoko functions in a standard library module dedicated to extending that type’s suite of supported operations.

Append two arrays:

public func append<A>(xs : [A], ys : [A]) : [A]

Apply an array of functions to an array of arguments (of matching lengths):

public func apply<A, B>(fs : [A -> B], xs : [A]) : [B]

Apply a function to each array element, produce an array of (all) results:

public func bind<A, B>(xs : [A], f : A -> [B]) : [B]

Fold over the array:

public func foldl<A, B>(f : (B, A) -> B, initial : B, xs : [A]) : B

Fold over the array:

public func foldr<A, B>(f : (A, B) -> B, initial : B, xs : [A]) : B

Find an element in the array:

public func find<A>(f : A -> Bool, xs : [A]) : ?A

Convert a mutable array into an immutable one:

public func freeze<A>(xs : [var A]) : [A]

Convert an array of arrays into a single (flattened) array:

public func join<A>(xs : [[A]]) : [A]

Map each array element by the given mapping function:

public func map<A, B>(f : A -> B, xs : [A]) : [B]
public func pure<A>(x: A) : [A] ;

Convert an immutable array into a mutable one:

public func thaw<A>(xs : [A]) : [var A]

module List

Purely-functional, singly-linked lists.

A singly-linked list consists of zero or more cons cells, wherein each cell contains a single list element (the cell’s head), and a pointer to the remainder of the list (the cell’s tail).

public type List<T> = ?(T, List<T>);


empty list

public func nil<T>() : List<T>


test for empty list

public func isNil<T>(l : List<T>) : Bool


aka “list cons”

public func push<T>(x : T, l : List<T>) : List<T>


last element, optionally; tail recursive

public func last<T>(l : List<T>) : ?T


treat the list as a stack; combines the usual operations head and non-failing) tail into one operation

public func pop<T>(l : List<T>) : (?T, List<T>)


length; tail recursive

public func len<T>(l : List<T>) : Nat


test length against a maximum value; tail recursive

public func lenIsEqLessThan<T>(l : List<T>, i : Nat) : Bool


get the length, unless greater than a maximum value, in which return null; tail recursive

public func lenClamp<T>(l : List<T>, i0 : Nat) : ?Nat


array-like list access, but in linear time; tail recursive

public func nth<T>(l : List<T>, n : Nat) : ?T


reverse the list; tail recursive

public func rev<T>(l : List<T>) : List<T>


Called app in SML Basis, and iter in OCaml; tail recursive

public func iter<T>(l : List<T>, f:T -> ()) : ()


map the list elements; non-tail recursive.

public func map<T,S>(l : List<T>, f:T -> S) : List<S>


filter the list elements; non-tail recursive

public func filter<T>(l : List<T>, f:T -> Bool) : List<T>


split the list elements; non-tail recursive

public func split<T>(l : List<T>, f:T -> Bool) : (List<T>, List<T>)


map and filter the list elements; non-tail recursive

public func mapFilter<T,S>(l : List<T>, f:T -> ?S) : List<S>


append two lists; non-tail recursive

public func append<T>(l : List<T>, m : List<T>) : List<T>


concat (aka “list join”); tail recursive, but requires “two passes”

public func concat<T>(l : List<List<T>>) : List<T>


See SML Basis library; tail recursive

public func revAppend<T>(l1 : List<T>, l2 : List<T>) : List<T>


“take” n elements from the prefix of the given list.

If the given list has fewer than n elements, we return the full input list.

public func take<T>(l : List<T>, n:Nat) : List<T>


public func drop<T>(l : List<T>, n:Nat) : List<T>


fold list left-to-right using function f; tail recursive

public func foldLeft<T,S>(l : List<T>, a:S, f:(T,S) -> S) : S


fold the list right-to-left using function f; non-tail recursive

public func foldRight<T,S>(l : List<T>, a:S, f:(T,S) -> S) : S


test if there exists list element for which given predicate is true

public func find<T>(l: List<T>, f:T -> Bool) : ?T


test if there exists list element for which given predicate is true

public func exists<T>(l: List<T>, f:T -> Bool) : Bool


test if given predicate is true for all list elements

public func all<T>(l: List<T>, f:T -> Bool) : Bool


Given two ordered lists, merge them into a single ordered list

public func merge<T>(l1: List<T>, l2: List<T>, lte:(T,T) -> Bool) : List<T>


Compare two lists lexicographic` ordering. tail recursive.

To do: Eventually, follow collate design from SML Basis, with real sum types, use 3-valued order type here.

public func lessThanEq<T>(l1: List<T>, l2: List<T>, lte:(T,T) -> Bool) : Bool


Compare two lists for equality. tail recursive.

isEq(l1, l2) is equivalent to lessThanEq(l1,l2) && lessThanEq(l2,l1), but the former is more efficient.

public func isEq<T>(l1: List<T>, l2: List<T>, eq:(T,T) -> Bool) : Bool


using a predicate, create two lists from one: the “true” list, and the “false” list.

(See SML basis library); non-tail recursive.

public func partition<T>(l: List<T>, f:T -> Bool) : (List<T>, List<T>)


generate a list based on a length, and a function from list index to list element.

(See SML basis library); non-tail recursive.

public func tabulate<T>(n:Nat, f:Nat -> T) : List<T>

module AssocList

Association Lists, a la functional programming, in Motoko.

import List "";

public type AssocList<K,V> = List.List<(K,V)>;


find the value associated with a given key, or null if absent.

public func find<K,V>(al : AssocList<K,V>,
            : ?V


replace the value associated with a given key, or add it, if missing. returns old value, or null, if no prior value existed.

public func replace<K,V>(al : AssocList<K,V>,
                         ov: ?V)
            : (AssocList<K,V>, ?V)


The key-value pairs of the final list consist of those pairs of the left list whose keys are not present in the right list; the values of the right list are irrelevant.

public func diff<K,V,W>(al1: AssocList<K,V>,
                        al2: AssocList<K,W>,
                        keq: (K,K)->Bool)
            : AssocList<K,V>


public func mapAppend<K,V,W,X>(al1:AssocList<K,V>,
            : AssocList<K,X>


This operation generalizes the notion of “set union” to finite maps. Produces a “disjunctive image” of the two lists, where the values of matching keys are combined with the given binary operator.

For unmatched key-value pairs, the operator is still applied to create the value in the image. To accomodate these various situations, the operator accepts optional values, but is never applied to (null, null).

public func disj<K,V,W,X>(al1:AssocList<K,V>,
            : AssocList<K,X>


This operation generalizes the notion of “set intersection” to finite maps. Produces a “conjuctive image” of the two lists, where the values of matching keys are combined with the given binary operator, and unmatched key-value pairs are not present in the output.

public func join<K,V,W,X>(al1 : AssocList<K,V>,
            : AssocList<K,X>


This fold produces the list content, but where the list’s nil and cons constructors are replaced with the given value and function, respectively (nil and cons arguments).

public func fold<K,V,X>(al:AssocList<K,V>,
            : X

Appendix Chapter: Further reading

This appendix section gives additional background information. In some cases, we give links for further reading on various topics relevant to the design, use or deployment of Motoko services, or the language’s design itself.

Wasm as a formal, practical standard for portable assembly

Not complete

We refer readers to:

The Internet Computer as a platform for Motoko services

To software services authored in Motoko, the Internet Computer provides the abstraction of a single, shared operating system that hosts these services. Each service is a "canister" that consists of meta data, static content, and a Wasm module of compiled Motoko software (or Wasm from another language, which is also possible).

Each canister on the Internet Computer implements a micro service that interacts with other micro services via tamper-proof, asynchronous message-passing with strong communication (response-or-failure message delivery) guarantees.

Under the hood, the Internet Computer is a network of connected computers that communicate securely. Collectively, they provide processing services to registered users, developers, and other computers.

Unlike a traditional public or private cloud, such like Amazon Web Services (AWS), Google Cloud Platform (GCP), or Microsoft Azure, the Internet Computer platform hosts programs that are each distributed, and the platform itself is not owned and operated by a single private company.

Instead, its distributed architecture enables multiple computers to operate as a powerful virtual machine. This virtual machine has no single point of failure, and it runs independently of legacy IT technologies that are vulnerable to attack. As such, the Internet Computer provides a unique, open, unstoppable platform for hosting Motoko micro services.

Background on modern type systems

As with the design of Wasm, on which we build, the design and implementation of Motoko have benefited from decades of research on programming language theory, design and implementation. We humbly acknowledge our current nascent position within this long history.

For readers that want initiation into the world of programming languages, types and their theory, we recommend the following textbooks:

These books provide references for further background reading.

Not complete. To do: Add longer list of influential references, including academic papers and theses.

Discussion topics

Highlights and important features

Although Motoko is, strictly-speaking, a new language, you might find it is similar to a language you already know. For example, the Motoko typing system is similar to a functional programming language such as OCaml (Objective Caml), but the syntax you use in defining functions is more like coding in JavaScript. It also draws on elements that are common in other, more familiar, languages, including JavaScript, TypeScript, C#, Swift, Pony, ML, and Haskell. Unlike other programming languages, however, Motoko extends and optimizes features that are uniquely suited to the internet computer platform.

Actors and objects

One of the most important principles to keep in mind when preparing to use Motoko is that it is an actor-based programming model. An actor is a special kind of object with an isolated state that can interacted with remotely and asynchronously. All communication with and between actors involves passing messages asynchronously over the network using the internet computer’s messaging protocol. An actor’s messages are processed in sequence, so state modifications never cause race conditions.

Classes can be used to produce objects of a predetermined type, with a predetermined interface and behavior. Because actors are essentially objects, you can also define actor classes. In general, each actor object is used to create one application which is then deployed as a canister containing compiled WebAssembly, some environment configuration information, and interface bindings. For more information about the developing applications and deploying applications, see the Developer’s Guide.

Key language features

Some of the other important language features of Motoko include the following:

  • JavaScript/TypeScript-style syntax.

  • Bounded polymorphic type system that can assign types without explicit type annotations. Types can be inferred in many common situations. Strong, static typing ensures type safety and includes subtype polymorphism, and structural typing. Unbounded and bounded numeric types with explicit conversions between them. Bounded numeric types are checked for overflow.

  • Support for imperative programming features, including mutable variables and arrays, and local control flow constructs, such as loops, return, break and continue.

  • Functions and messages are first-class values. Pattern-matching is supported for scalar and compound values.

  • A simple, class-based object system without inheritance.

  • The value of a reference can never implicitly be null to prevent many common null-reference failures. Instead, the language enables you to explicitly handle null values using null, option type ?<type>.

  • Asynchronous message handling enables sequential programming with familiar async and await constructs and promise replies.

Appendix Chapter: Language manual

This chapter serves as a technical appendix for the previous chapters.

It serves as a kind of manual for a special audience of readers:

  • First, it gives technical details for authors of the higher-level documentation above.

  • Second, it gives the same details for compiler experts interested in the details of Motoko.

  • Finally, this chapter provides a place where the documentation above can direct curious or advanced readers.

This part strives to be complete as a reference manual, but not instructive or overly accessible for newcomers.

Program syntax


Space, newline, horizontal tab, carriage return, line feed and form feed are considered as whitespace. Whitespace is ignored but used to separate adjacent keywords, identifiers and operators.

In the definition of some lexemes, we use the symbol to denote a single whitespace character.


Single line comments are all characters following // until the end of the same line.

// single line comment
x = 1

Single or multi-line comments are any sequence of characters delimited by /* and */:

/* multi-line comments
   look like this, as in C and friends */

Comments delimited by /* and */ may be nested, provided the nesting is well-bracketed.

All comments are treated as whitespace.


The following keywords are reserved and may not be used as identifiers:

actor and assert assert await break case catch class continue debug
debug_show else false for func if in import not null object or
label let loop private public query return shared switch true try
type var while


<prog> ::=

Declaration syntax

The syntax of a declaration is as follows:

<dec> ::=                                                                declaration
  <exp>                                                                    expression
  let <pat> = <exp>                                                        immutable
  var <id> (: <typ>)? = <exp>                                              mutable
  <sort> <id>? =? { <dec-field>;* }                                        object
  <shared>? func <id>? <typ-params>? <pat> (: <typ>)? =? <exp>             function
  type <id> <typ-params>? = <typ>                                          type
  <sort>? class <id> <typ-params>? <pat> (: <typ>)? =? { <exp-field>;* }   class

<shared> ::=
  shared query?
<dec-field> ::=                                object declaration fields
  (public|private)? <dec>                        field


Identifiers are alpha-numeric, start with a letter and may contain underscores:

<id>   ::= Letter (Letter | Digit | _)*
Letter ::= A..Z | a..z
Digit  ::= 0..9

Expression syntax

The syntax of an expression is as follows:

<exp> ::=                                      expressions
  <id>                                           variable
  <lit>                                          literal
  <unop> <exp>                                   unary operator
  <exp> <binop> <exp>                            binary operator
  <exp> <relop> <exp>                            binary relational operator
  ( <exp>,* )                                    tuple
  <exp> . <nat>                                  tuple projection
  ? <exp>                                        option injection
  { <exp-field>;* }                              object
  # id <exp>?                                    variant injection
  <exp> . <id>                                   object projection
  <exp> := <exp>                                 assignment
  <unop>= <exp>                                  unary update
  <exp> <binop>= <exp>                           binary update
  [ var? <exp>,* ]                               array
  <exp> [ <exp> ]                                array indexing
  <shared>? func <func_exp>                      function expression
  <exp> <typ-args>? <exp>                        function call
  { <dec>;* }                                    block
  not <exp>                                      negation
  <exp> and <exp>                                conjunction
  <exp> or <exp>                                 disjunction
  if <exp> <exp> (else <exp>)?                   conditional
  switch <exp> { (case <pat> <exp>;)+ }          switch
  while <exp> <exp>                              while loop
  loop <exp> (while <exp>)?                      loop
  for ( <pat> in <exp> ) <exp>                   iteration
  label <id> (: <typ>)? <exp>                    label
  break <id> <exp>?                              break
  continue <id>                                  continue
  return <exp>?                                  return
  async <exp>                                    async expression
  await <exp>                                    await future (only in async)
  throw <exp>                                    raise an error (only in async)
  try <exp> catch <pat> <exp>                    catch an error (only in async)
  assert <exp>                                   assertion
  <exp> : <typ>                                  type annotation
  dec                                            declaration
  debug <exp>                                    debug expression
  ( <exp> )                                      parentheses


The syntax of a pattern is as follows:

<pat> ::=                                      patterns
  _                                              wildcard
  <id>                                           variable
  <unop>? <lit>                                  literal
  ( <pat>,* )                                    tuple or brackets
  { <pat-field>;* }                              object pattern
  # <id> <pat>?                                  variant pattern
  ? <pat>                                        option
  <pat> : <typ>                                  type annotation
  <pat> or <pat>                                 disjunctive pattern

<pat-field> ::=                                object pattern fields
  <id> = <pat>                                   field


Integers are written as decimal or hexadecimal, Ox-prefixed natural numbers. Subsequent digits may be prefixed a single, semantically irrelevant, underscore.

digit ::= ['0'-'9']
hexdigit ::= ['0'-'9''a'-'f''A'-'F']
num ::= digit ('_'? digit)*
hexnum ::= hexdigit ('_'? hexdigit)*
nat ::= num | "0x" hexnum

Negative integers may be constructed by applying a prefix negation - operation.


A character is a single quote (') delimited: * Unicode character in UTF-8, * \-escaped newline, carriage return, tab, single or double quotation mark * \-prefixed ASCII character (TBR), * or \u{ hexnum } enclosed valid, escaped Unicode character in hexadecimal (TBR).

ascii ::= ['\x00'-'\x7f']
ascii_no_nl ::= ['\x00'-'\x09''\x0b'-'\x7f']
utf8cont ::= ['\x80'-'\xbf']
utf8enc ::=
    ['\xc2'-'\xdf'] utf8cont
  | ['\xe0'] ['\xa0'-'\xbf'] utf8cont
  | ['\xed'] ['\x80'-'\x9f'] utf8cont
  | ['\xe1'-'\xec''\xee'-'\xef'] utf8cont utf8cont
  | ['\xf0'] ['\x90'-'\xbf'] utf8cont utf8cont
  | ['\xf4'] ['\x80'-'\x8f'] utf8cont utf8cont
  | ['\xf1'-'\xf3'] utf8cont utf8cont utf8cont
utf8 ::= ascii | utf8enc
utf8_no_nl ::= ascii_no_nl | utf8enc

escape ::= ['n''r''t''\\''\'''\"']

character ::=
  | [^'"''\\''\x00'-'\x1f''\x7f'-'\xff']
  | utf8enc
  | '\\'escape
  | '\\'hexdigit hexdigit
  | "\\u{" hexnum '}'

char := '\'' character '\''


A text literal is "-delimited sequence of characters:

text ::= '"' character* '"'


<lit> ::=                                     literals
  <nat>                                         natural
  <float>                                       float
  <char>                                        character
  <text>                                        Unicode text

Literals are constant values. The syntactic validity of a literal depends on the precision of the type at which it is used.

Operators and types


To simplify the presentation of available operators, operators and primitive types are classified into basic categories:

Abbreviation Category



arithmetic operations



logical/Boolean operations



bitwise operations



equality and comparison




Some types have several categories, e.g. type Int is both arithmetic (A) and relational ® and supports both arithmentic addition (+) and relational less than () (amongst other operations).

Unary Operators

<unop> Category



numeric negation



numeric identity



bitwise negation

Relational Operators

<relop> Category



less than (must be enclosed in whitespace)



greater than (must be enclosed in whitespace)






not equals


less than or equal



greater than or equal

Equality is structural.

Numeric Binary Operators

<binop> Category



















Bitwise Binary Operators

<binop> Category



bitwise and



bitwise or



exclusive or



shift left



shift right (must be preceded by whitespace)



signed shift right



rotate left



rotate right

String Operators

<binop> Category




Assignment Operators

:=, <unop>=, <binop>= Category



assignment (in place update)



in place add



in place subtract



in place multiply



in place divide



in place modulo



in place exponentiation



in place logical and



in place logical or



in place exclusive or



in place shift left



in place shift right



in place signed shift right



in place rotate left



in place rotate right



in place concatenation

The category of a compound assigment <unop>=/<binop>= is given by the category of the operator <unop>/<binop>.

Operator and Keyword Precedence

The following table defines the relative precedence and associativity of operators and tokens, ordered from lowest to highest precedence. Tokens on the same line have equal precedence with the indicated associativity.

Precedence Associativity Token



if _ _ (no else), loop _ (no while)



else, while



:= `, `+=, -=, =, /=, %=, *=, #=, &=, |=, ^=, <⇐, >>-, <<>=, <>>=












==, !=, <, >, , >, >=



+, -, #



*, /, %












<<, >>, <<>, <>>




Type syntax

Type expressions are used to specify the types of arguments, constraints (a.k.a bounds) on type parameters, definitions of type constructors, and the types of sub-expressions in type annotations.

<typ> ::=                                     type expressions
  <path> <typ-args>?                            constructor
  <sort>? { <typ-field>;* }                     object
  { <typ-tag>;* }                               variant
  { # }                                         empty variant
  [ var? <typ> ]                                array
  Null                                          null type
  ? <typ>                                       option
  <shared>? <typ-params>? <typ> -> <typ>        function
  async <typ>                                   future
  ( ((<id> :)? <typ>),* )                       tuple
  Any                                           top
  None                                          bottom
  Error                                         errors/exceptions
  ( type )                                      parenthesized type

<sort> ::= (actor | module | object)

<path> ::=                                   paths
  <id>                                         type identifier
  <path> . <id>                                projection

An absent <sort>? abbreviates object.

Primitive types

Motoko provides the following primitive type identifiers, including support for Booleans, signed and unsigned integers and machine words of various sizes, characters and text.

The category of a type determines the operators (unary, binary, relational and in-place update via assigment) applicable to values of that type.

Identifier Category Description


L, R

boolean values true and false and logical operators


A, R

signed integer values with arithmetic (unbounded)


A, R

signed 8-bit integer values with checked arithmetic


A, R

signed 16-bit integer values with checked arithmetic


A, R

signed 32-bit integer values with checked arithmetic


A, R

signed 64-bit integer values with checked arithmetic


A, R

non-negative integer values with arithmetic (unbounded)


A, R

non-negative 8-bit integer values with checked arithmetic


A, R

non-negative 16-bit integer values with checked arithmetic


A, R

non-negative 32-bit integer values with checked arithmetic


A, R

non-negative 64-bit integer values with checked arithmetic


A, B, R

unsigned 8-bit integers with bitwise operations


A, B, R

unsigned 16-bit integers with bitwise operations


A, B, R

unsigned 32-bit integers with bitwise operations


A, B, R

unsigned 64-bit integers with bitwise operations



Unicode characters


T, R

Unicode strings of characters with concatenation _ # _


(opaque) error values

Type Bool

The type Bool of categories L, R (Logical, Relational) has values true and false and is supported by one and two branch if _ <exp> (else <exp>)?, not <exp>, _ and and or _ expressions. Expressions if, and and or are short-circuiting.

Type Char

A Char of category R (Relational) represents characters as a code point in the Unicode character set. Characters can be converted to Word32, and Word32`s in the range 0 .. 0x1FFFFF can be converted to `Char (the conversion traps if outside of this range). With charToText a character can be converted into a text of length 1.

Type Text

The type Text of categories T and R (Text, Relational) represents sequences of Unicode characters (i.e. strings). Operations on text values include concatenation (_ # _) and sequential iteration over characters via for (c in _) …​ c …​. The textLength function returns the number of characters in a Text value.

Type Int and Nat

The types Int and Nat are signed integral and natural numbers of categories A (Arithmetic) and R (Relational).

Both Int and Nat are arbitrary precision, with only subtraction - on Nat trapping on underflow.

The subtype relation Nat <: Int holds, so every expression of type Nat is also an expression of type Int (but not vice versa). In particular, every value of type Nat is also a value of type Int, without change of representation.

Bounded Integers Int8, Int16, Int32 and Int64

The types Int8, Int16, Int32 and Int64 represent signed integers with respectively 8, 16, 32 and 64 bit precision. All have categories A (Arithmetic) and R (Relational).

Operations that may under- or overflow the representation are checked and trap on error.

Bounded Naturals Nat8, Nat16, Nat32 and Nat64

The types Nat8, Nat16, Nat32 and Nat64 represent unsigned integers with respectively 8, 16, 32 and 64 bit precision. All have categories A (Arithmetic) and R (Relational).

Operations that may under- or overflow the representation are checked and trap on error.

Word types

The types Word8, Word16, Word32 and Word64 represent fixed-width bit patterns of width n (8, 16, 32 and 64). All word types have categories A (Arithmetic), B (Bitwise) and R (Relational). As arithmetic types, word types implementing numeric wrap-around (modulo 2^n). As bitwise types, word types support bitwise operations and (&), or (|) and exclusive-or (^). Further, words can be rotated left (<<>), right (<>>), and shifted left (<<), right (>>), as well as right with two’s-complement sign preserved (+>>). All shift and rotate amounts are considered modulo the word’s width n.

Conversions to Int and Nat, named wordnToInt and wordnToNat, are exact and expose the word’s bit-pattern as two’s complement values, resp. natural numbers. Reverse conversions, named intToWordn and natToWordn are potentially lossy, but the round-trip property holds modulo 2^n. The former choose the two’s-complement representation for negative integers.

Word types are not in subtype relationship with each other or with other arithmetic types, and their literals need type annotation, e.g. (-42 : Word16). For negative literals the two’s-complement representation is applied.

Error type

Errors are opaque values constructed using operation * error: Text → Error and examined using operations: * errorCode: Error → ErrorCode * errorMessage: Error → Text

(where ErrorCode is the prelude defined variant type:

type ErrorCode = {#error; #system ; /*...*/ };


Error values can be thrown and caught within an async expression or shared function (only).

A constructed error e = error(m) has errorCode(e) = #error and errorMessage(e)=m. Errors with non-#error (system) error codes may be caught and thrown, but not constructed.

Note: Exiting an async block or shared function with a system error exits with a copy of the error with revised code #error and the original error message. This prevents programmatic forgery of system errors.

Constructed types

<path> <typ-args>? is the application of a type identifier or path, either built-in (i.e. Int) or user defined, to zero or more type arguments. The type arguments must satisfy the bounds, if any, expected by the type constructor’s type parameters (see below).

Though typically a type identifier, more generally, <path> may be a .-separated sequence of actor, object or module identifiers ending in an identifier accessing a type component of a value (for example, Acme.Collections.List).

Object types

<sort>? { <typ-field>;* } specifies an object type by listing its zero or more named type fields.

Within an object type, the names of fields must be distinct (both by name and hash value).

Object types that differ only in the ordering of the fields are equivalent.

When <sort>? is actor, all fields have shared function type (specifying messages).

Variant types

{ <typ-tag>;* } specifies a variant type by listing its variant type fields as a sequence of `<typ-tag>`s.

Within a variant type, the tags of its variants must be distinct (both by name and hash value).

Variant types that differ only in the ordering of their variant type fields are equivalent.

{ # } specifies the empty variant type.

Array types

[ var? <typ> ] specifies the type of arrays with elements of type <typ>.

Arrays are immutable unless specified with qualifier var.

Null type

The Null type has a single value, the literal null. Null is a subtype of the option ? T, for any type T.

Option types

? <typ> specifies the type of values that are either null or a proper value of the form ? <v> where <v> has type typ.

Function types

Type <shared>? <typ-params>? <typ1> → <typ2> specifies the type of functions that consume (optional) type parameters <typ-params>, consume a value parameter of type <typ1> and produce a result of type <typ2>.

Both <typ1> and <typ2> may reference type parameters declared in <typ-params>.

If <typ1> or <typ2> (or both) is a tuple type, then the length of that tuple type determines the argument or result arity of the function type.

The optional <shared> qualifier specifies whether the function value is shared, which further constrains the form of <typ-params>, <typ1> and <typ2> (see Sharability below).

(Note that a <shared> function may be itself be shared or shared query, determining the persistence of its state changes.)

Async types

async <typ> specifies a promise producing a value of a type <typ>.

Promise types typically appear as the result type of a shared function that produces an await-able value.

Tuple types

( ((<id> :)? <typ>),* ) specifies the type of a tuple with zero or more ordered components.

The optional identifier <id>, naming its components, is for documentation purposes only and cannot be used for component access. In particular, tuple types that differ only in the names of components are equivalent.

Any type

Type Any is the top type, i.e. the super-type of all types. All values have type Any.

None type

Type None is the bottom type, a subtype of all other types. No value has type None.

As an empty type, None can be used to specify the impossible return value of an infinite loop or unconditional trap.

Parenthesised type

A function that takes an immediate, syntactic tuple of length n >= 0 as its domain or range is a function that takes (respectively returns) n values.

When enclosing the argument or result type of a function, which is itself a tuple type, ( <tuple-typ> ) declares that the function takes or returns a single (boxed) value of type <tuple-type>.

In all other positions, ( <typ> ) has the same meaning as <typ>.

Type fields

<typ-field> ::=                               object type fields
  <id> : <typ>                                  immutable
  var <id> : <typ>                              mutable
  <id> <typ-params>? <typ1> : <typ2>            function (short-hand)

A type field specifies the name and type of a field of an object. The field names within a single object type must be distinct and have non-colliding hashes.

<id> : <typ> specifies an immutable field, named <id> of type <typ>.

var <id> : <typ> specifies a mutable field, named <id> of type <typ>.

Variant type fields

<typ-tag> ::=                                 variant type fields
  # <id> : <typ>                                tag
  # <id>                                        unit tag (short-hand)

A variant type field specifies the tag and type of a single variant of an enclosing variant type. The tags within a single variant type must be distinct and have non-colliding hashes.

# <id> : <typ> specifies an (immutable) field, named <id> of type <typ>. # <id> is sugar for an (immutable) field, named <id> of type ().


When enclosed by an actor object type, <id> <typ-params>? <typ1> : <typ2> is syntactic sugar for an immutable field named <id> of shared function type shared <typ-params>? <typ1> → <typ2>.

When enclosed by a non-actor object type, <id> <typ-params>? <typ1> : <typ2> is syntactic sugar for an immutable field named <id> of ordinary function type <typ-params>? <typ1> → <typ2>.

Type parameters

<typ-params> ::=                              type parameters
  < typ-param,* >
  <id> <: <typ>                               constrained type parameter
  <id>                                        unconstrained type parameter

A type constructors, function value or function type may be parameterised by a vector of comma-separated, optionally constrained, type parameters.

<id> <: <typ> declares a type parameter with constraint <typ>. Any instantiation of <id> must subtype <typ> (at that same instantiation).

Syntactic sugar <id> declares a type parameter with implicit, trivial constraint Any.

The names of type parameters in a vector must be distinct.

All type parameters declared in a vector are in scope within its bounds.

Type arguments

<typ-args> ::=                                type arguments
  < <typ>,* >

Type constructors and functions may take type arguments.

The number of type arguments must agree with the number of declared type parameters of the function.

Given a vector of type arguments instantiating a vector of type parameters, each type argument must satisfy the instantiated bounds of the corresponding type parameter.

Well-formed types

A type T is well-formed only if (recursively) its constituent types are well-formed, and:

  • if T is async U then U is shared, and

  • if T is shared query? U → V, U is shared and V == () or V == async W' with W shared, and

  • if T is C<T0, …​, TN> where:

    • a declaration type C<X0 <: U0, Xn <: Un> = …​ is in scope, and

    • Ti <: Ui[ T0/X0, …​, Tn/Xn ], for each 0 ⇐ i ⇐ n.

  • if T is actor { …​ } then all fields in …​ are immutable and have shared function type.


Two types T, U are related by subtyping, written T <: U, whenever, one of the following conditions is true:

  • T equals U (reflexivity).

  • U equals Any.

  • T equals None.

  • T is a type parameter X declared with constraint U.

  • T is Nat and U is Int.

  • T is a tuple (T0, …​, Tn), U is a tuple (U0, …​, Un), and for each 0 ⇐ i ⇐ n, Ti <: Ui.

  • T is an immutable array type [ V ], U is an immutable array type [ W ] and V <: W.

  • T is a mutable array type [ var V ], U is a mutable array type [ var W ] and V == W.

  • T is Null and U is an option type ? W for some W.

  • T is ? V, U is ? W and V <: W.

  • T is a promise async V, U is a promise async W, and V <: W.

  • T is an object type sort0 { fts0 }, U is an object type sort1 { fts1 } and

    • sort0 == sort1, and, for all fields,

    • if field id : V is in fts0 then id : W is in fts1 and V <: W, and

    • if mutable field var id : V is in fts0 then var id : W is in fts1 and V == W.

      (That is, object type T is a subtype of object type U if they have same sort, every mutable field in U super-types the same field in T and every mutable field in U is mutable in T with an equivalent type. In particular, T may specify more fields than U.)

  • T is a variant type { fts0 }, U is a variant type { fts1 } and

    • if field # id : V is in fts0 then # id : W is in fts1 and V <: W.

      (That is, variant type T is a subtype of variant type U if every field of T subtypes the same field of U. In particular, T may specify fewer variants than U.)

  • T is a function type <shared>? <X0 <: V0, …​, Xn <: Vn> T1 → T2, U is a function type <shared>? <X0 <: W0, …​, Xn <: Wn> U1 → U2 and

    • T and U are either both equivalently <shared>?, and

    • assuming constraints X0 <: W0, …​, Xn <: Wn then

      • for all i, Wi <: Vi, and

      • U1 <: T1, and

      • T2 <: U2.

        (That is, function type T is a subtype of function type U if they have same <shared>? qualification, they have the same type parameters (modulo renaming) and assuming the bounds in U, every bound in T supertypes the corresponding parameter bound in U (contra-variance), the domain of T supertypes the domain of U (contra-variance) and the range of T subtypes the range of U (co-variance).)

  • T (respectively U) is a constructed type C<V0,…​VN> that is equal, by definition of type constructor C, to W, and W <: U (respectively U <: W).

  • For some type V, T <: V and V <: U (transitivity).


A type T is shared if it is

  • Any or None, or

  • a primitive type other than Error, or

  • an option type ? V where V is shared, or

  • a tuple type (T0, …​, Tn) where all Ti are shared, or

  • an immutable array type [V] where V is shared, or

  • an object type where all fields are immutable and have shared type, or

  • a variant type where all tags have shared type, or

  • a shared function type, or

  • an actor type.

For now, the Motoko compiler does not permit function types or actors as shared types and reports an error when compiling programs that require this.

Static and dynamic semantics

Below, we give a detailed account of the semantics of Motoko programs.

For each expression form and each declaration form, we summaize its semantics, both in static terms (based on typing) and dynamic terms (based on program evaluation).


A program <prog> is a sequence of declarations <dec>;* that ends with an optional actor declaration. The actor declaration determines the main actor, if any, of the program.

All type and value declarations within <prog> are mutually-recursive.

Declaration Fields

Declaration fields declare the fields of actors and objects. They are just declarations, prefixed by an optional visibility qualifier public or private; if omitted, visibility defaults to private.

Any identifier bound by a public declaration appears in the type of enclosing object and is accessible via the dot notation.

An identifier bound by a private declaration is excluded form the type of the enclosing object and inaccessible via the dot notation.

Sequence of Declarations

A sequence of declarations <dec>;* occurring in a block, a program or the exp-field;* sequence of an object declaration has type T provided

  • <dec>;* is empty and T == (); or

  • <dec>;* is non-empty and:

  • all value identifiers bound by <dec>;* are distinct, and

  • all type identifiers bound by <dec>;* are distinct, and

  • under the assumption that each value identifier <id> in decs;* has type var_id? Tid, and assuming the type definitions in decs;*:

  • each declaration in <dec>;* is well-typed, and

  • each value identifier <id> in bindings produced by <dec>;* has type var_id? Tid, and

  • the last declaration in <dec>;* has type T.

Declarations in <dec>;* are evaluated sequentially. The first declaration that traps causes the entire sequence to trap. Otherwise, the result of the declaration is the value of the last declaration in <dec>;*. In addition, the set of value bindings defined by <dec>;* is the union of the bindings introduced by each declaration in <dec>;*.

It is a compile-time error if any declaration in <dec>;* might require the value of an identifier declared in <dec>;* before that identifier’s declaration has been evaluated. Such use-before-define errors are detected by a simple, conservative static analysis not described here.


Patterns bind function parameters, declare identifiers and decompose values into their constituent parts in the cases of a switch expression.

Matching a pattern against a value may succeed, binding the corresponding identifiers in the pattern to their matching values, or fail. Thus the result of a match is either a successful binding, mapping identifiers of the pattern to values, or failure.

The consequences of pattern match failure depends on the context of the pattern.

  • In a function application or let-binding, failure to match the formal argument pattern or let-pattern causes a trap.

  • In a case branch of a switch expression, failure to match that case’s pattern continues with an attempt to match the next case of the switch, trapping only when no such case remains.

Wildcard pattern

The wildcard pattern _ matches a single value without binding its contents to an identifier.

Identifier pattern

The identifier pattern <id> matches a single value and binds it to the identifier <id>.

Literal pattern

The literal pattern <unop>? <lit> matches a single value against the constant value of literal <lit> and fails if they are not (structurally) equal values.

For integer literals only, the optional <unop> determines the sign of the value to match.

Tuple pattern

The tuple pattern ( <pat>,* ) matches a n-tuple value against an n-tuple of patterns (both the tuple and pattern must have the same number of items). The set of identifiers bound by each component of the tuple pattern must be distinct.

Pattern matching fails if one of the patterns fails to match the corresponding item of the tuple value. Pattern matching succeeds if every pattern matches the corresponding component of the tuple value. The binding returned by a successful match is the disjoint union of the bindings returned by the component matches.

Object pattern

The object pattern { <pat-field>;* } matches an object value, a collection of named field values, against a sequence of named pattern fields. The set of identifiers bound by each field of the object pattern must be distinct. The names of the pattern fields in the object pattern must be distinct.

Pattern matching fails if one of the pattern fields fails to match the corresponding field value of the object value. Pattern matching succeeds if every pattern field matches the corresponding named field of the object value. The binding returned by a successful match is the union of the bindings returned by the field matches.

The <sort> of the matched object type must be determined by an enclosing type annotation or other contextual type information.

Variant pattern

The variant pattern # <id> <pat>? matches a variant value (of the form # <id'> v) against a variant pattern. An absent <pat>? is shorthand for the unit pattern (). Pattern matching fails if the tag <id'> of the value is distinct from the <id> of the pattern (i.e. <id> <> <id'>); or the tags are equal but the value v does not match the pattern <pat>?. Pattern matching succeeds if the tag of the value is <id> (i.e. <id'> = <id>) and the value v matches the pattern <pat>?. The binding returned by a successful match is just the binding returned by the match of v against <pat>?.

Annotated pattern

The annotated pattern <pat> : <typ> matches value of v type <typ> against the pattern <pat>.

<pat> : <typ> is not a dynamic type test, but is used to constrain the types of identifiers bound in <pat>, e.g. in the argument pattern to a function.

Option pattern

The option ? <pat> matches a value of option type ? <typ>.

The match fails if the value is null. If the value is ? v, for some value v, then the result of matching ? <pat> is the result of matching v against <pat>.

Conversely, the null literal pattern may be used to test whether a value of option type is the value null and not ? v for some v.

Or pattern

The or pattern <pat1> or <pat2> is a disjunctive pattern.

The result of matching <pat1> or <pat2> against a value is the result of matching <pat1>, if it succeeds, or the result of matching <pat2>, if the first match fails.

(Note, statically, neither <pat1> nor <pat2> may contain identifier (<id>) patterns so a successful match always binds zero identifiers.)

Expression Declaration

The declaration <exp> has type T provided the expression <exp> has type T . It declares no bindings.

The declaration <exp> evaluates to the result of evaluating <exp> (typically for `<exp>’s side-effect).

Let Declaration

The let declaration <pat> = <exp> has type T and declares the bindings in <pat> provided:

  • <exp> has type T.

  • <pat> has type T.

The <pat> = <exp> evaluates <exp> to a result r. If r is trap, the declaration evaluates to trap. If r is a value v then evaluation proceeds by matching the value v against <pat>. If matching fails, then the result is trap. Otherwise, the result is v and the binding of all identifiers in <pat> to their matching values in v.

All bindings declared by a let (if any) are immutable.

Var Declaration

The variable declaration var <id> (: <typ>)? = <exp> declares a mutable variable <id> with initial value <exp>. The variable’s value can be updated by assignment.

The declaration var <id> has type () provided:

  • <exp> has type T; and

  • If the annotation (:<typ>)? is present, then T == <typ>.

Within the scope of the declaration, <id> has type var T (see Assignment).

Evaluation of var <id> (: <typ>)? = <exp> proceeds by evaluating <exp> to a result r. If r is trap, the declaration evaluates to trap. Otherwise, the r is some value v that determines the initial value of mutable variable <id>. The result of the declaration is () and <id> is bound to a fresh location that contains v.

Type Declaration

The declaration type <id> <typ-params>? = <typ> declares a new type constructor <id>, with optional type parameters <typ-params> and definition <typ>.

The declaration type C < X0<:T0>, …​, Xn <: Tn > = U is well-formed provided:

  • type parameters X0, …​, Xn are distinct, and

  • assuming the constraints X0 <: T0, …​, Xn <: Tn:

  • constraints T0, …​, Tn are well-formed.

  • definition U is well-formed.

In scope of the declaration type C < X0<:T0>, …​, Xn <: Tn > = U, any well-formed type C < U0, …​, Un> is equivalent to its expansion U [ U0/X0, …​, Un/Xn ]. Distinct type expressions that expand to identical types are inter-changeable, regardless of any distinction between type constructor names. In short, the equivalence between types is structural, not nominal.

Object Declaration

Declaration <sort> <id>? =? { <exp-field>;* } declares an object with optional identifier <id> and zero or more fields <exp_field>;*. Fields can be declared with public or private visibility; if the visibility is omitted, it defaults to private.

The qualifier <sort> (one of actor, module or object) specifies the sort of the object’s type. The sort imposes restrictions on the types of the public object fields.

Let T = sort { [var0] id0 : T0, …​ , [varn] idn : T0 } denote the type of the object. Let <dec>;* be the sequence of declarations in <exp_field>;*. The object declaration has type T provided that:

  1. type T is well-formed for sort sort, and

  2. under the assumption that <id> : T,

    • the sequence of declarations <dec>;* has type Any and declares the disjoint sets of private and public identifiers, Id_private and Id_public respectively, with types T(id) for id in Id == Id_private union Id_public, and

    • { id0, …​, idn } == Id_public, and

    • for all i in 0 ⇐ i ⇐ n, [vari] Ti == T(idi).

Note that requirement 1. imposes further constraints on the field types of T. In particular:

  • if the sort is actor then all public fields must be non-var (immutable) shared functions (the public interface of an actor can only provide asynchronous messaging via shared functions).

Evaluation of (object|actor)? <id>? =? { <exp-field>;* } proceeds by evaluating the declarations in <dec>;*. If the evaluation of <dec>;* traps, so does the object declaration. Otherwise, <dec>;* produces a set of bindings for identifiers in Id. let v0, …​, vn be the values or locations bound to identifiers <id0>, …​, <idn>. The result of the object declaration is the object v == sort { <id0> = v1, …​, <idn> = vn}.

If <id>? is present, the declaration binds <id> to v. Otherwise, it produces the empty set of bindings.

Function Declaration

The function declaration <shared>? func <id>? <typ-params>? <pat> (: <typ>)? =? <exp> is syntactic sugar for a let declaration of a function expression. That is:

<shared>? func <id> <typ-params>? <pat> (: <typ>)? =? <exp> :=
  let <id> = <shared>? func <id> <typ-params>? <pat> (: <typ>)? =? <exp>

where <pat> is <id> when <id>? is present and <pat> is _ otherwise.

Named function definitions are recursive.

Class declarations

The declaration <sort>? class <id> <typ-params>? <pat> (: <typ>)? =? <id_this>? { <exp-field>;* } is sugar for pair of a type and function declaration:

<sort>? class <id> <typ-params>? <pat> (: <typ>)? =? <id_this>? { <dec-field>;* } :=
  type <id> <typ-params> = <sort> { <typ-field>;* };
  func <id> <typ-params>? <pat> : <id> <typ-args>  = <sort> <id_this>? { <dec-field>;* }


  • <typ-args>? is the sequence of type identifiers bound by <typ-params>? (if any), and

  • <typ-field>;* is the set of public field types inferred from <dec-field;*>.

  • <id_this>? is the optional this parameter of the object instance.


The expression <id> evaluates to the value bound to <id> in the current evaluation environment.

Literals' evaluation

A literal has type T only when its value is within the prescribed range of values of type T.

The literal (or constant) expression <lit> evaluates to itself.

Unary operators

The unary operator <unop> <exp> has type T provided:

  • <exp> has type T, and

  • <unop>’s category is a category of `T.

The unary operator expression <unop> <exp> evaluates exp to a result. If the result is a value v, it returns the result of <unop> v. If the result is a trap, it, too, traps.

Binary operators

The binary compound assigment <exp1> <binop> <exp2> has type T provided:

  • <exp1> has type T, and

  • <exp2> has type T, and

  • <binop>’s category is a category of `T.

The binary operator expression <exp1> <binop> <exp2> evaluates exp1 to a result r1. If r1 is trap, the expression results in trap.

Otherwise, exp2 is evaluated to a result r2. If r2 is trap, the expression results in trap.

Otherwise, r1 and r2 are values v1 and v2 and the expression returns the result of v1 <binop> v2.

Relational operators

The relational expression <exp1> <relop> <exp2> has type Bool provided:

  • <exp1> has type T, and

  • <exp2> has type T, and

  • <relop>’s category R is a category of `T.

The binary operator expression <exp1> <relop> <exp2> evaluates exp1 to a result r1. If r1 is trap, the expression results in trap.

Otherwise, exp2 is evaluated to a result r2. If r2 is trap, the expression results in trap.

Otherwise, r1 and r2 are values v1 and v2 and the expression returns the result of v1 <relop> v2.


Tuple expression (<exp1>, …​, <expn>) has tuple type (T1, …​, Tn), provided <exp1>, …​, <expN> have types T1, …​, Tn.

The tuple expression (<exp1>, …​, <expn>) evaluates the expressions exp1 …​ expn in order, trapping as soon as some expression <expi> traps. If no evaluation traps and exp1, …​, <expn> evaluate to values v1,…​,vn then the tuple expression returns the tuple value (v1, …​ , vn).

The tuple projection <exp> . <nat> has type Ti provided <exp> has tuple type (T1, …​, Ti, …​, Tn), <nat> == i and 1 ⇐ i ⇐ n.

The projection <exp> . <nat> evaluates exp to a result r. If r is trap, then the result is trap. Otherwise, r must be a tuple (v1,…​,vi,…​,vn) and the result of the projection is the value vi.

Option expressions

The option expression ? <exp> has type ? T provided <exp> has type T.

The literal null has type Null. Since Null <: ? T for any T, literal null also has type ? T and signifies the "missing" value at type ? T.

Variant injection

The variant injection # <id> <exp> has variant type {# id T} provided: * <exp> has type T.

The variant injection # <id> is just syntactic sugar for # <id> ().

The variant injection`# <id> <exp>` evaluates exp to a result r. If r is trap, then the result is trap. Otherwise, r must be a value v and the result of the injection is the tagged value # <id> v.

The tag and contents of a variant value can be tested and accessed using a variant pattern.


Objects can be written in literal form { <exp-field>;* }, consisting of a list of expression fields:

<exp-field> ::= var? <id> = <exp>

Such an object literal is equivalent to the object declaration object { <dec-field>;* } where the declaration fields are obtained from the expression fields by prefixing each of them with public let, or just public in case of var fields.

Object projection (Member access)

The object projection <exp> . <id> has type var? T provided <exp> has object type sort { var1? <id1> : T1, …​, var? <id> : T, …​, var? <idn> : Tn } for some sort sort.

The object projection <exp> . <id> evaluates exp to a result r. If r is trap,then the result is trap. Otherwise, r must be an o bject value { <id1> = v1,…​, id = v, …​, <idn> = vn } and the result of the projection is the value v of field id.

If var is absent from var? T then the value v is the constant value of immutable field <id>, otherwise:

  • if the projection occurs as the target an assignment statement; v is the mutable location of the field <id>.

  • otherwise, v (of type T) is the value currently stored in mutable field <id>.


The assignment <exp1> := <exp2> has type () provided:

  • <exp1> has type var T, and

  • <exp2> has type T.

The assignment expression <exp1> := <exp2> evaluates <exp1> to a result r1. If r1 is trap, the expression results in trap.

Otherwise, exp2 is evaluated to a result r2. If r2 is trap, the expression results in trap.

Otherwise r1 and r2 are (respectively) a location v1 (a mutable identifier, an item of a mutable array or a mutable field of object) and a value v2. The expression updates the current value stored in v1 with the new value v2 and returns the empty tuple ().

Unary Compound Assignment

The unary compound assignment <unop>= <exp> has type () provided:

  • <exp> has type var T, and

  • <unop>’s category is a category of `T.

The unary compound assignment <unop>= <exp> evaluates <exp> to a result r. If r is trap the evaluation traps, otherwise r is a location storing value v and r is updated to contain the value <unop> v.

Binary Compound Assignment

The binary compound assigment <exp1> <binop>= <exp2> has type () provided:

  • <exp1> has type var T, and

  • <exp2> has type T, and

  • <binop>’s category is a category of `T.

For binary operator <binop>, <exp1> <binop>= <exp1>, the compound assignment expression <exp1> <binop>= <exp2> evaluates <exp1> to a result r1. If r1 is trap, the expression results in trap. Otherwise, exp2 is evaluated to a result r2. If r2 is trap, the expression results in trap.

Otherwise r1 and r2 are (respectively) a location v1 (a mutable identifier, an item of a mutable array or a mutable field of object) and a value v2. The expression updates the current value, w stored in v1 with the new value w <binop> v2 and returns the empty tuple ().


The expression [ var? <exp>,* ] has type [var? T] provided each expression <exp> in the sequence <exp,>* has type T.

The array expression [ var <exp0>, …​, <expn> ] evaluates the expressions exp0 …​ expn in order, trapping as soon as some expression <expi> traps. If no evaluation traps and exp0, …​, <expn> evaluate to values v0,…​,vn then the array expression returns the array value [var? v0, …​ , vn] (of size n+1).

The array indexing expression <exp1> [ <exp2> ] has type var? T provided <exp> has (mutable or immutable) array type [var? T1].

The projection <exp1> . <exp2> evaluates exp1 to a result r1. If r1 is trap, then the result is trap.

Otherwise, exp2 is evaluated to a result r2. If r2 is trap, the expression results in trap.

Otherwise, r1 is an array value, var? [v0, …​, vn], and r2 is a natural integer i. If i > n the index expression returns trap.

Otherwise, the index expression returns the value v, obtained as follows:

If var is absent from var? T then the value v is the constant value vi.


  • if the projection occurs as the target an assignment statement then v is the `i`th location in the array;

  • otherwise, v is vi, the value currently stored in the `i`th location of the array.

Function Calls

The function call expression <exp1> <T0,…​,Tn>? <exp2> has type T provided

  • the function <exp1> has function type <shared>? < X0 <: V0, …​, Xn <: Vn > U1→ U2; and

  • each type argument satisfies the corresponding type parameter’s bounds: for each 1⇐ i ⇐ n, Ti <: [T0/X0, …​, Tn/Xn]Vi; and

  • the argument <exp2> has type [T0/X0, …​, Tn/Xn]U1, and

  • T == [T0/X0, …​, Tn/Xn]U2.

The call expression <exp1> <T0,…​,Tn>? <exp2> evaluates exp1 to a result r1. If r1 is trap, then the result is trap.

Otherwise, exp2 is evaluated to a result r2. If r2 is trap, the expression results in trap.

Otherwise, r1 is a function value, <shared>? func <X0 <: V0, …​, n <: Vn> pat { exp } (for some implicit environment), and r2 is a value v2. Evaluation continues by matching v1 against pat. If matching succeeds with some bindings, evaluation proceeds with exp using the environment of the function value (not shown) extended with those bindings. Otherwise, the pattern match has failed and the call results in trap.


The function expression <shared>? func < X0 <: T1, …​, Xn <: Tn > <pat> (: T2)? =? <exp> has type <shared>? < X0 <: T0, …​, Xn <: Tn > T1→ T2 if, under the assumption that X0 <: T1, …​, Xn <: Tn:

  • all the types in T1, …​, Tn and T are well-formed and well-constrained.

  • pattern pat has type T1;

  • expression <exp> has type return type T2 under the assumption that pat has type T1.

<shared>? func <typ-params>? <pat> (: <typ>)? =? <exp> evaluates to a function value (a.k.a. closure), denoted <shared>? func <typ-params>? <pat> = <exp>, that stores the code of the function together with the bindings from the current evaluation environment (not shown) needed to evaluate calls to the function value.

Note that a <shared> function may be itself be shared or shared query: * A shared function may be invoked from a remote caller. Unless causing a trap, the effects on the callee persist beyond completion of the call. * A shared query function may be also be invoked from a remote caller, but the effects on the callee are transient and discarded once the call has completed with a result (whether a value or error).


The block expression { <dec>;* } has type T provided the last declaration in the sequence <dec>;* has type T. All identifiers declared in block must be distinct type identifiers or distinct value identifiers and are in scope in the definition of all other declarations in the block.

The bindings of identifiers declared in { dec;* } are local to the block. The type T must be well-formed in the enclosing environment of the block. In particular, any local, recursive types that cannot be expanded to types well-formed the enclosing environment must not appear in T.

The type system ensures that a value identifier cannot be evaluated before its declaration has been evaluated, precluding run-time errors at the cost of rejection some well-behaved programs.

Identifiers whose types cannot be inferred from their declaration, but are used in a forward reference, may require an additional type annotation (see Annotated patterns) to satisfy the type checker.

The block expression { <dec>;* } evaluates each declaration in <dec>;* in sequence (program order). The first declaration in <dec>;* that results in a trap cause the block to result in trap, without evaluating subsequent declarations.


The not expression not <exp> has type Bool provided <exp> has type Bool.

If <exp> evaluates to trap, the expression returns trap. Otherwise, <exp> evaluates to a Boolean value v and the expression returns not v, (the Boolean negation of v).


The and expression <exp1> and <exp2> has type Bool provided <exp1> and <exp2> have type Bool.

The expression <exp1> and <exp2> evaluates exp1 to a result r1. If r1 is trap, the expression results in trap. Otherwise r1 is a Boolean value v. If v == false the expression returns the value false (without evaluating <exp2>). Otherwise, the expression returns the result of evaluating <exp2>.


The or expression <exp1> or <exp2> has type Bool provided <exp1> and <exp2> have type Bool.

The expression <exp1> and <exp2> evaluates exp1 to a result r1. If r1 is trap, the expression results in trap. Otherwise r1 is a Boolean value v. If v == true the expression returns the value true (without evaluating <exp2>). Otherwise, the expression returns the result of evaluating <exp2>.


The expression if <exp1> <exp2> (else <exp3>)? has type T provided:

  • <exp1> has type Bool

  • <exp2> has type T

  • <exp3> is absent and () <: T, or

  • <exp3> is present and has type T.

The expression evaluates <exp1> to a result r1. If r1 is trap, the result is trap. Otherwise, r1 is the value true or false. If r1 is true, the result is the result of evaluating <exp2>. Otherwise, r1 is false and the result is () (if <exp3> is absent) or the result of <exp3> (if <exp3> is present).


The switch expression switch <exp0> { (case <pat> <exp>;)+ } has type T provided:

  • exp0 has type U; and

  • for each case case <pat> <exp> in the sequence (case <pat> <exp>;)+ :

  • pattern <pat> has type U; and,

  • expression <exp> has type T (in an environment extended with `<pat>’s bindings).

The expression evaluates <exp0> to a result r1. If r1 is trap, the result is trap. Otherwise, r1 is some value v. Let case <pat> <exp>; be the first case in (case <pat> <exp>;)+ such that <pat> matches v with for some bindings of identifiers to values. Then result of the switch is the result of evaluating <exp> under those bindings. If no case has a pattern that matches v, the result of the switch is trap.


The expression while <exp1> <exp2> has type () provided:

  • <exp1> has type Bool, and

  • <exp2> has type ().

The expression evaluates <exp1> to a result r1. If r1 is trap, the result is trap. Otherwise, r1 is the value true or false. If r1 is true, the result is the result of re-evaluating while <exp1> <exp2>. Otherwise, the result is ().


The expression loop <exp> has type None provided <exp> has type ().

The expression evaluates <exp> to a result r1. If r1 is trap, the result is trap. Otherwise, the result is the result of (re-)evaluating loop <exp1>.

Loop While

The expression loop <exp1> while <exp2> has type () provided:

  • <exp1> has type (), and

  • <exp2> has type Bool.

The expression evaluates <exp1> to a result r1. If r1 is trap, the result is trap. Otherwise, evaluation continues with <exp2>, producing result r2. If r2 is trap the result is trap. Otherwise, if r2 is true, the result is the result of re-evaluating loop <exp1> while <exp2>. Otherwise, r2 is false and the result is ().


The for expression for ( <pat> in <exp1> ) <exp2> has type () provided:

  • <exp1> has type { next : () → ?T; };

  • pattern <pat> has type T; and,

  • expression <exp2> has type () (in the environment extended with `<pat>’s bindings).

The for-expression is syntactic sugar for

for ( <pat> in <exp1> ) <exp2> :=
    let x = <exp1>;
    label l loop {
      switch ( {
        case (? <pat>) <exp2>;
        case (null) break l;

where x is a fresh identifier.

In particular, the for loops will trap if evaluation of <exp1> traps; as soon as some value of traps or the value of does not match pattern <pat>.

TBR: do we want this semantics? We could, instead, skip values that don’t match <pat>?


The label-expression label <id> (: <typ>)? <exp> has type T provided:

  • (: <typ>)? is absent and T is unit; or (: <typ>)? is present and T == <typ>;

  • <exp> has type T in the static environment extended with label l : T.

The result of evaluating label <id> (: <typ>)? <exp> is the result of evaluating <exp>.

Labeled loops

If <exp> in label <id> (: <typ>)? <exp> is a looping construct:

  • while (exp2) <exp1>,

  • loop <exp1> (while (<exp2>))?, or

  • for (<pat> in <exp2> <exp1>

the body, <exp1>, of the loop is implicitly enclosed in label <id_continue> (…​) allowing early continuation of the loop by the evaluation of expression continue <id>.

<id_continue> is fresh identifier that can only be referenced by continue <id> (through its implicit expansion to break <id_continue>).


The expression break <id> is equivalent to break <id> ().

The expression break <id> <exp> has type Any provided:

  • The label <id> is declared with type label <id> : T.

  • <exp> has type T.

The evaluation of break <id> <exp> evaluates exp to some result r. If r is trap, the result is trap. If r is a value v, the evaluation abandons the current computation up to dynamically enclosing declaration label <id> …​ using the value v as the result of that labelled expression.


The expression continue <id> is equivalent to break <id_continue>, where <id_continue> is implicitly declared around the bodies of <id>-labelled looping constructs (See Section Labeled Loops).


The expression return is equivalent to return ().

The expression return <exp> has type None provided:

  • <exp> has type T and

  • T is the return type of the nearest enclosing function (with no intervening async expression), or

  • async T is the type of the nearest enclosing (perhaps implicit) async expression (with no intervening function declaration)

The return expression exits the corresponding dynamic function invocation or completes the corresponding dynamic async expression with the result of exp.


The async expression async <exp> has type async T provided:

  • <exp> has type T;

  • T is shared.

Any control-flow label in scope for async <exp> is not in scope for <exp>. However, <exp> may declare and use its own, local, labels.

The implicit return type in <exp> is T. That is, the return expression, <exp0>, (implicit or explicit) to any enclosed return <exp0>? expression, must have type T.

Evaluation of async <exp> queues a message to evaluate <exp> in the nearest enclosing or top-level actor. It immediately returns a promise of type async T that can be used to await the result of the pending evaluation of <exp>.


The await expression await <exp> has type T provided:

  • <exp> has type async T,

  • T is shared,

  • the await is explicitly enclosed by an async-expression or appears in the body of a shared function.

Expression await <exp> evaluates <exp> to a result r. If r is trap, evaluation returns trap. Otherwise r is a promise. If the promise is complete with value v, then await <exp> evaluates to value v. If the promise is complete with (thrown) error value e, then await <exp> re-throws the error e. If the promise is incomplete, that is, its evaluation is still pending, await <exp> suspends evaluation of the neared enclosing async or shared-function, adding the suspension to the wait-queue of the promise. Execution of the suspension is resumed once the promise is completed (if ever).

WARNING: between suspension and resumption of a computation, the state of the enclosing actor may change due to concurrent processing of other incoming actor messages. It is the programmer’s responsibility to guard against non-synchronized state changes.


The throw expression throw <exp> has type None provided:

  • <exp> has type Error,

  • the throw is explicitly enclosed by an async-expression or appears in the body of a shared function.

Expression throw <exp> evaluates <exp> to a result r. If r is trap, evaluation returns trap. Otherwise r is an error value e. Execution proceeds from the catch clause of the nearest enclosing try <exp> catch <pat> <ex> whose pattern <pat> matches value e. If there is no such try expression, e is stored as the erroneous result of the async value of the nearest enclosing async expression or shared function invocation.


The try expression try <exp1> catch <pat> <exp2> has type T provided:

  • <exp1> has type T.

  • <pat> has type Error and <exp2> has type T in the context extended with <pat>

  • the try is explicitly enclosed by an async-expression or appears in the body of a shared function.

Expression try <exp1> catch <pat> <exp2> evaluates <exp1> to a result r. If evaluation of <exp1> throws an uncaught error value e, the result of the try is the result of evaluating <exp2> under the bindings determined by the match of e against pat.

Note: because the Error type is opaque, the pattern match cannot fail (typing ensures that <pat> is an irrefutable wildcard or identifier pattern).


The assert expression assert <exp> has type () provided exp has type Bool.

Expression assert <exp> evaluates <exp> to a result r. If r is trap evaluation returns trap. Otherwise r is a boolean value v. The result of assert <exp> is:

  • the value (), when v is true; or

  • trap, when v is false.

Type Annotation

The type annotation expression <exp> : <typ> has type T provided:

  • <typ> is T, and

  • <exp> has type U where U <: T.

Type annotation may be used to aid the type-checker when it cannot otherwise determine the type of <exp> or when one wants to constrain the inferred type, U of <exp> to a less-informative super-type T provided U <: T.

The result of evaluating <exp> : <typ> is the result of evaluating <exp>.

Note: type annotations have no-runtime cost and cannot be used to perform the (checked or unchecked) down-casts available in other object-oriented languages.


The declaration expression <dec> has type T provided the declaration <dec> has type T.

Evaluating the expression <dec> proceed by evaluating <dec>, returning the result of <dec> but discarding the bindings introduced by <dec> (if any).


The debug expression debug <exp> has type () provided the expression <exp> has type ().

When the program is compiled or interpreted with (default) flag --debug, evaluating the expression debug <exp> proceeds by evaluating <exp>, returning the result of <exp>.

When the program is compiled or interpreted with flag --release, evaluating the expression debug <exp> immediately returns the unit value '()'. The code for <exp> is never executed, nor is its code included in the compiled binary.


The parenthesized expression ( <exp> ) has type T provided <exp> has type T.

The result of evaluating ( <exp> ) is the result of evaluating <exp>.


Whenever <exp> has type T and T <: U (T subtypes U) then by virture of implicit subsumption, <exp> also has type U (without extra syntax).

In general, this means that an expression of a more specific type may appear wherever an expression of a more general type is expected, provided the specific and general types are related by subtyping.