Basic concepts and terms
Overview
Motoko is designed for distributed programming with actors. When programming on ICP in Motoko, each actor represents an ICP canister smart contract with a Candid interface. Within Motoko, the term actor is used to refer to any canister authored in any language that deploys to ICP. The role of Motoko is to make these actors easy to author and use programmatically once deployed.
Before you begin writing canisters in Motoko, you should be familiar with a few of the basic concepts and terms specific to Motoko.
Values
Primitive values
Motoko supports the following primitive types and values:
Bool
: Boolean values (true
andfalse
).Int
: Integers (…,-2
,-1
,0
,1
,2
, …) - bounded and unbounded variants.Nat
: Natural numbers (0
,1
,2
, …) - bounded and unbounded variants.Char
: Unicode text characters ('a'
,'B'
,'☃'
).Text
: Text values of 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 bit-width (one of 8
, 16
, 32
, 64
) that determines the range of representable values, and each carries the potential for overflow. Exceeding a bound is a run-time fault that 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 conventional %
character in the operator. The language provides primitive built-ins to convert between these various number representations.
Non-primitive values
Motoko permits user-defined types and each of the following non-primitive value forms and associated types:
Tuples, including the unit value (the "empty tuple").
Arrays with both immutable and mutable variants.
Objects with named, unordered fields and methods.
Variants with named constructors and optional payload values.
Function values including shareable functions.
Async values, also known as promises or futures;
Error values carry the payload of exceptions and system failures.
For precise language definitions of primitive and non-primitive values, see the language reference.
Objects, records and their extension mechanisms
Objects are aggregate data made from labeled constituent data. In their most general form, objects can contain named values (let
and var
) as well as methods (func
) that act on them. Objects are written with the leading keyword object
followed by an optional name and the block comprising its constituents. Only public
constituents contribute to the object's type.
In many cases, objects are used as simple containers of data, which are referred to as records. When building records, Motoko has a simplified syntax to offer where semicolon-separated named fields are placed in braces. The labels are identifiers (with a leading var
when the field is mutable), followed by =
and the initial value. All fields are public and contribute to the record's type.
Furthermore, syntactic forms are provided for building new records from existing ones, adding new fields, or replacing existing ones. The base records and objects are separated by the and
keyword and can be followed by with
and semicolon-separated additional (or overwriting) fields. The bases and fields are wrapped in braces, indicating record formation. When the bases have overlapping fields (considering their types), then a disambiguating field overwrite must be provided. The original bases remain unmodified, and thus we refer to this as a functional record combination and extension.
Printing values
The function print
, from base library Debug
, 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, 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.
You 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
.
Motoko program syntax
Each Motoko program is comprised of declarations and expressions whose syntactic classes are distinct but related.
Declarations introduce immutable variables, mutable state, actors, objects, classes and other types. Declarations can be mutually recursive, but in cases where they are not, they permit substitution semantics such as replacing values with an equal value.
Expressions describe computations that involve these notions.
To deploy a valid program to ICP, the program must consist of an actor expression introduced with the keyword actor
.
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;
This program’s type is Nat
(natural number), and when run, it evaluates to the Nat
value of 3
.
This program is a declaration list that consists of three declarations:
Immutable variable
x
, via declarationlet x = 1;
.Immutable variable
y
, via declarationlet y = x + 1;
.An unnamed, implicit variable holding the final expression’s value,
x * y + x
.
The expression x * y + x
illustrates that 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 ()
.
Unit-type restrictions can be ignored by explicitly using the ignore
keyword to disregard any unused result values.
Lexical scoping
A declaration list is not itself an expression, so you cannot declare another variable with its final value.
Block expressions can be formed from a 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. A block expression produces a value and, when enclosed in parentheses, can occur within some larger, compound expression.
A particular form of blocks are provided for convenience when processing data that may be missing or incomplete. These are described under option blocks.
In all other places, do { … }
is used to represent block expressions and distinguish blocks from object literals. For example, do {}
is the empty block of type ()
, while {}
is an empty record of record type {}
. This block form preserves the autonomy of the declaration list and its choice of variable names. This means that variables' scopes may nest, but they may not interfere as they nest. Language theorists call this idea lexical scoping.
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.
Type soundness
Each Motoko expression that type checks is considered 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. There is a precise space of meaningful programs. The type system enforces that programs stay within it and that all well-typed programs have a precise 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 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 and 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, you can confirm that the added annotations are consistent with the existing ones.
Type errors and messages
Motoko is a statically typed programming language. That means that the compiler will reject any program that contains obviously non-sensical code.
For example, while adding two numbers is allowed, adding a number to a text value makes no sense to the Motoko compiler and is flagged as an error that must be fixed before the code can be run or deployed.
The rules that Motoko applies to verify the correctness of code before compiling and running it are called its type system. Motoko's type system will detect and reject static errors such as applying a function to the wrong number of arguments, or to arguments of the wrong type.
The type system is a safety feature that prevents a slew of errors that would otherwise have to be detected and reported at runtime, when they would be difficult or impossible to address.
Motoko base library
For various practical language engineering reasons, the design of Motoko strives to minimize built-in 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, focusing on core features used in the examples that are unlikely to change radically. The base library APIs will likely evolve over time and in particular, grow in size and number as Motoko matures.
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 with the mo:
prefix, specify the base/
path, followed by the module’s file name Debug.mo
minus its extension.
Traps
Some errors, such as division by zero, out-of-bounds array indexing, and pattern match failure are by design not prevented by the type system, but instead cause dynamic faults called traps.
Because the meaning of execution is ill-defined after a faulting trap, execution of the code ends by aborting at the trap.
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. This has subtle security implications, so be sure to consult the relevant security recommendations.
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!");
Assertions allow you to conditionally trap when some Boolean test fails to hold, but continue execution otherwise:
let n = 65535;
assert n % 2 == 0; // traps when n not even
Because an assertion may succeed, and thus proceed with execution, it may only be used in context where a value of type ()
is expected.
The system
capability
Smart contracts (i.e., Motoko actor
s) may generally contain assets that correspond to real-world value, the loss of which can be detrimental. Many such assets are mobile and can be transferred through message sending. In order for a library to be able to send a message, the corresponding function must be imported and possess an async
(or async*
) type. Calling such functions is only possible when the send capability is given by the callee, also having such a type.
Naturally, the programmer must be careful when granting send privileges to third-party libraries (resp. functions therein) and reviewing for potential security breaches if they choose to do so.
There is a special class of functions, however, that can be called from code that does not possess send capability but registers a callback that does. This kind of capability elevation is possible when adding timers (e.g. setTimer
in base
). To harden the actor
against supply-chain attacks (malicious sends masquerading behind a capability-starved call interface to third-party code), Motoko allows to declare functions that can potentially lead to capability elevation to require a system
capability.
The system
capability originates from the top-level actor and can be passed to functions that expect it by specifying a pseudo-type parameter <system, ...>
which must appear at the call site. Similarly, functions demanding the system
capability declare it in their signature:
func elevate<system>(ref : Int, callback : Int -> async* ()) {
ignore Timer.setTimer<system>(#seconds 0, func() : async () { await* callback ref })
}