Basic concepts and terms

Motoko is designed for distributed programming with actors.

When programming on the Internet Computer in Motoko, each actor represents an Internet Computer canister smart contract with a Candid interface, whether written in Motoko, Rust, Wasm or some other language that compiles to Wasm. Within Motoko, we use the term actor to refer to any canister, authored in any language that deploys to the Internet Computer. The role of Motoko is to make these actors easy to author, and easy to use programmatically, once deployed.

Before you begin writing distributed applications using actors, you should be familiar with a few of the basic building blocks of any programming language and with Motoko in particular. To get you started, this section introduces the following key concepts and terms that are used throughout the remainder of the documentation and that are essential to learning to program in Motoko:

  • program

  • declaration

  • expression

  • value

  • variable

  • type

If you have experience programming in other languages or are familiar with modern programming language theory, you are probably already comfortable with these terms and how they are used. There’s nothing unique in how these terms are used in Motoko. If you are new to programming, however, this guide introduces each of these terms gradually and by using simplified example programs that eschew any use of actors or distributed programming. After you have the basic terminology as a foundation to build on, you can explore more advanced aspects of the language. More advanced features are illustrated with correspondingly more complex examples.

The following topics are covered in the section:

Motoko program syntax

Each Motoko program is a free mix of declarations and expressions, whose syntactic classes are distinct, but related (see the language quick reference guide 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 Actors and async data.

In preparing for that discussion, we discuss programs in this chapter and in Mutable state 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.

The examples in this section illustrate basic principles using simple expressions, such as arithmetic. For an overview of the full expression syntax of Motoko, see the Language quick reference.

As a starting point, the following code snippet consists of two declarations — for the variables x and y — followed by an expression to form 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 (do { and }) and another variable (z), we can amend our original program as follows:

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

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 ().

Ignoring 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. For example:

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

Declarations and variable substitution

Declarations can be mutually recursive, but in cases where they are not, they permit substitution semantics. (that is, replacing equals for equals, as familiar from high-school algebraic simplification).

Recall our original example:

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

We can 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 3) — as the original program.

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. Blocks are only allowed as sub-expressions of control flow expressions like if, loop, case, etc. In all other places, we use do { …​ } to represent block expression, to distinguish blocks from object literals. For example, do {} is the empty block of type (), while {} is an empty record of record type {}.

do {
  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;
ignore do {
  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. For example, nesting your program within a program you do not trust cannot arbitrarily redefine your variables 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.

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 explicitly wrapping operations (indicated by a % character in the operator). The language provides primitive built-ins to convert between these various number representations.

The language quick reference 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. For precise language definitions of primitive and non-primitive values, see the language quick reference.

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 Nat 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 asynchronous interactions agree between static and dynamic views of the program, and that the resulting messages generated "under the hood" never mismatch at runtime. 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 (for example, 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 base library

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

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

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

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

import D "mo:base/Debug";
D.print("hello world");

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

Printing using Debug.print and debug_show

Above, we print the text string using the function print in library Debug.mo:

print: Text -> ()

The function print accepts a text string (of type Text) as input, and produces the unit value (of unit type, or ()) as its output.

Because unit values carry no information, all values of type unit are identical, so the print function doesn’t actually produce an interesting result. Instead of a result, it has a side effect. The function print has the effect of emitting the text string in a human-readable form to the output terminal. Functions that have side effects, such as emitting output, or modifying state, are often called impure. Functions that just return values, without further side-effects, are called pure. 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.

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:

import D "mo:base/Debug";
D.print(debug_show(("hello", 42, "world")))

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

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 base Prelude 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:base/Prelude";

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

P.xxx()

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 "not yet implemented" (nyi) features, and marked as such with a similar function from the Prelude module:

P.nyi()

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 base library function unreachable:

P.unreachable()

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

Traps due to execution failure

Some errors, such as division by zero, out-of-bounds array indexing, and pattern match failure are not prevented by the type system, but can cause dynamic failures called traps.

1/0; // traps due to division by 0
let a = ["hello", "world"];
a[2]; // traps due to out-of-bounds indexing
let true = false; // pattern match failure

We say that code traps when its exection causes a trap.

Execution of code is aborted at the first trap and makes no further progress.

Traps that occur within actor messages are more subtle: they don’t abort the entire actor, but prevent that particular message from proceeding, rolling back any yet uncommitted state changes. Other messages on the actor will continue execution.

Explicit traps

Occasionally it can be useful to force an unconditional trap, with a user-defined message.

The Debug library provides the function trap(t) for this purpose, which can be used in any context.

import Debug "mo:base/Debug";

Debug.trap("oops!");
import Debug "mo:base/Debug";

let swear : Text = Debug.trap("oh my!");

(The Prelude functions nyi(), unreachable() and xxx() discussed above are simple wrappers around Debug.trap.)

Assertions

Assertions allow you to conditionally trap when some Boolean test fails to hold, but continue execution otherwise. For example,

let n = 65535;
assert n % 2 == 0; // traps when n not even
assert false; // unconditionally traps
import Debug "mo:base/Debug";

assert 1 > 0; // never traps
Debug.print "bingo!";

Because an assertion may succeed, and thus proceed with execution, it may only be used in context where a value of type () is expected.