Basic concepts and terms

Motoko is designed for distributed programming with actors.

Before you begin writing programs for distributed processing using actors, you should be familiar with a few of the basic building blocks of amy 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 Lanaguage 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 ({ 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
};
printNat(z)

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

Printing using 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;
printNat(x);
let y = x + 1;
printNat(y);
x * y + x;

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 a substitution semantics.

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:

{
  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 re-associate 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 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 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 P for “Prelude”, and a URL where the import declaration may locate the imported module:

import P "mo:base/Prelude";
P.printLn("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 Prelude.mo minus its extension.

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: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.

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.