Introduction

The Monad language is a dependently typed, purely functional systems programming language that compiles through LLVM.

🌐 monad-lang.org

[!WARNING] Monad is in alpha release and under heavy development. Many features are not implemented yet and are not tested properly. Expect breaking changes, incomplete functionality, and potential bugs.

Read the Maturity Matrix first — it says, area by area, what actually works today and what is still a sketch.

Hello World

Here is a simple example:

open IO {println}

def main (args : List String) : IO Unit := println "Hello, World!"

Save this as hello.mo and run it:

monad run hello.mo

run compiles the program and executes the result: a Monad program is always a native binary. (monad eval interprets one instead, but reaches only a handful of pure natives.) See Compiling and Running, which also covers where the monad binary itself comes from.

Key Features

• Dependent types: types can depend on values, including a Prop universe, propositional equality with a J eliminator, and length-indexed vectors
• Type classes: ad-hoc polymorphism with constraints and instance resolution
• Termination checking: recursive definitions must be structurally decreasing unless you opt out
• Macros: defmacro, quote, and compile-time reflection, which is how #[derive] is implemented — in Monad, not in the compiler
• Pattern matching: destructure data with match
• Native functions: call Rust code from Monad
• IO monad: managed side effects
• Self-hosting: the compiler in lang/ is written in Monad and compiles itself

Linear and affine types are a stated goal of the language. Their syntax is accepted everywhere it is meant to be — struct fields, parameters, lambdas — but nothing is enforced yet; the multiplicity is dropped before type checking. See Linear Types.

Quick Example

open IO {println}

#[terminating]
def factorial (n : I64) : I64 :=
    if n == 0
    then 1
    else n * factorial (n - 1)

def main (args : List String) : IO Unit :=
    println (I64.to_string (factorial 5))

Two things in that example are worth noticing straight away, because they trip up everyone writing their first Monad program:

• factorial needs #[terminating]. Recursion on n - 1 is not structurally decreasing, so the termination checker rejects it unless you assert that the function is well-founded. See Termination Checking.
• println takes a String, not "anything printable". Numbers go through I64.to_string (or the ToString class).

Where to go next

• Maturity Matrix — what works, what doesn't, at a glance
• Getting Started — the language tutorial
• Compiling and Running — the compiler and its commands
• Reference — the syntax and standard-library reference
• The Bootstrap Host — the Rust implementation, what it is for, and where the two differ

Maturity Matrix

Monad is in alpha. This chapter says, area by area, what actually works today — so you can tell the parts you can build on from the parts that are still a sketch.

This rates the self-hosted compiler, the monad binary written in Monad that compiles itself. That is the language. Where the Rust bootstrap host differs it is called out, because the difference currently matters.

Every row here was checked against the compilers' own source and tests at the commit this book ships with, not inferred from intent.

How to Read This

Language

Implementation

Ecosystem

Scale

For context on what "alpha" means here:

The Short Version

Monad is a real, self-hosting language: the compiler is written in Monad, compiles itself, and reaches a fixpoint. The type checker, the class system, the module system, and a genuine macro system all work.

What it is not yet: safe by construction (the self-hosted compiler checks termination but not linearity — the multiplicity syntax parses everywhere now, and means nothing), scalable in concurrency (fibers are 1:1 pthreads with 128 MB stacks, real but not the design that ships), or distributable (nightly binaries exist; a lockfile and a registry do not). Its test runner compiles and runs a driver binary per test file, and covers the whole corpus with no exclusion list — every file that used to be reported as a gap now runs self-hosted.

The single largest gap is linear types — and because deterministic memory management is meant to be built on them, that gap is also why compiled binaries need a garbage collector.

Getting Started

Welcome to the Monad language! This tutorial walks through the fundamentals of programming in Monad, a dependently typed language.

Prerequisites

Before getting started, ensure you have:

• A monad binary. The compiler is written in Monad, so the first one is either built by the bootstrap host or installed as a nightly with monadup — see Compiling and Running. (Nightlies are Linux x86_64 and currently need Nix; building from source is the portable route. A nightly also installs the init, std, llvm and runtime sources, so it can compile a program that lives outside a checkout.)
• llc, clang, and the Boehm GC development files, which the compiler links against. devenv shell provides all three.
• A text editor. There is no syntax-highlighting plugin yet; the bootstrap host ships an LSP server for diagnostics.

Your First Program

Let's start with the classic "Hello, World!" program:

open IO {println}

def main (args : List String) : IO Unit := println "Hello, World!"

Save this as hello.mo, then run it:

monad run hello.mo

You should see:

Hello, World!

run compiles the program and executes the result — a Monad program is always a native binary. To keep the binary, use compile and give it an absolute output path, since a relative one lands in the compiler's scratch directory:

monad build hello.mo -o "$PWD/hello"
./hello

Your Own Mote

A mote is a package: a directory with a mote.toml in it. That single file is what turns a pile of .mo files into something the compiler can resolve against, and it is why a program of your own in its own repository can find init, std and the C runtime without naming any of them.

The smallest one that is a mote is one table:

[mote]
name = "game"

Put it next to your sources and the bare forms of the commands work from anywhere inside the directory:

cd game
monad check              # check the mote containing the working directory
monad test               # build and run its #[test] defs
monad build . -o "$PWD/game"   # build the mote's binary target

Two more tables are worth having. [[bin]] is what monad build . reads to decide which file is the program and what to call it; [dependencies.X] is a path to another mote — the form to reach for when you have a compiler checkout rather than an install, and want init/std out of it:

[mote]
name = "game"

[[bin]]
name = "game"
path = "src/main.mo"

[dependencies.std]
path = "../monad/std"

[dependencies.init]
path = "../monad/init"

[dependencies.runtime]
path = "../monad/runtime"

Absolute paths are fine here, and monad check bare inside the mote handles them. If you installed the compiler with monadup, you do not need those three entries at all: an install ships the init, std, llvm and runtime sources beside the binary, and the compiler finds them there. Nothing in your mote.toml has to mention the standard library.

Both target tables have defaults, so a mote that follows the conventions never declares either one:

• [lib] path defaults to src/lib.mo, the file that makes use game resolve from another mote. Write lib.mo for a library, skip it for a binary-only mote.
• [[bin]] is a list of targets, each with a name (defaulting to the mote's own name) and a path (defaulting to src/main.mo). With no bin table at all, a mote has exactly one target: src/main.mo, named after the mote. Several targets are how one mote ships several programs — monad build <mote> --bin <name> picks between them, and monad build refuses rather than guessing when more than one is there.

A mote needs at least one target that exists on disk — a library root, or a binary — and monad check says so if it has neither.

A single file outside any mote still works — that is a script module, and it names its own dependencies with a file-level annotation:

#![mote { name := "scratch", deps := [init, std] }]

See Modules and Imports for the search order the compiler uses, and Compiling and Running for installing the toolchain in the first place.

Understanding the Structure

Every Monad program follows this basic structure:

1. Imports (use): bring modules into scope
2. Open declarations (open): make definitions available without prefixes
3. Definitions (def): declare functions and values
4. Type signatures: annotate the types of definitions

Point 4 is not optional. Every def must carry a type annotation — there is no top-level type inference. def x := 42 is a parse error; write def x : I64 := 42.

Variables and Basic Types

def x : I64 := 42            // 64-bit signed integer
def name : String := "Monad" // String
def flag : Bool := true      // Boolean
def nothing : Unit := unit   // Unit type (single value)
def ratio : F64 := 3.14      // 64-bit float

The other fixed-width numeric types are I32, I16, I8, U64, U32, U16, U8, and F32. Integer literals default to I64 and float literals to F64; a suffix picks another width (42u8, 3.14f32).

Character literals are written with single quotes, and take the same escapes as strings:

def letter : Char := 'M'
def newline : Char := '\n'
def lambda : Char := 'λ'

A literal holds one Unicode codepoint. There is no \u{...} escape — write the character itself. Be aware that Char is a stub type: it has no operations at all, no equality and no ToString, so you can hold and pass a Char but not yet inspect one. For text you work with, use String.

Functions

Functions are defined using def with curried parameters:

// Simple function
def double (n : I64) : I64 := n + n

// Multi-parameter function (curried)
def add (a : I64) (b : I64) : I64 := a + b

// Two parameters of the same type share one annotation
def mul (a b : I64) : I64 := a * b

// A plain value
def greeting : String := "Hello"

Function Application

Function application is written with spaces:

def double (n : I64) : I64 := n + n
def add (a : I64) (b : I64) : I64 := a + b

def result : I64 := double (add 3 4)  // 14

Anonymous Functions (Lambdas)

Lambda expressions use fn, \, or ꟛ — the three spellings are identical:

def square : I64 -> I64 := fn n => n * n
def add_one : I64 -> I64 := \ x => x + 1
def identity {A : Type} : A -> A := ꟛ x => x

The annotation on the def is what gives the lambda's parameter its type, so a lambda-bodied definition always needs a function type in its signature.

Pattern Matching

Match on values to deconstruct them:

def is_zero (n : Nat) : Bool :=
  match n {
    zero => true,
    succ _ => false
  }

// Pattern matching on booleans
def negate (b : Bool) : Bool :=
  match b {
    true => false,
    false => true
  }

Patterns are one level deep: each constructor argument is a fresh name or _. Nested patterns, literal patterns, and guards are not supported, and match expressions are not checked for exhaustiveness — see the Maturity Matrix.

Let Bindings

A let binds one name, and in gives the body:

def compute : I64 :=
  let x := 10 in
  let y := x * 2 in
  x + y

Chain them for several bindings, as above. Unlike a top-level def, a let binding infers its type; you can still annotate one explicitly:

def hypotenuse_squared (a : I64) (b : I64) : I64 :=
  let a2 : I64 := a * a in
  let b2 : I64 := b * b in
  a2 + b2

Several bindings can also share one let, separated by ;:

def multi : I64 := let x := 10; y := 20 in x + y

Each binding sees the ones before it, and each may carry its own annotation. The ; is required — the bootstrap host lets you leave it out, the self-hosted compiler does not. Nested let … in works everywhere and is the form used through most of this book.

Docstrings

Document your declarations with /// docstrings. They are retained through module loading, so the bootstrap host's LSP server can show them:

/// Greet a user by name.
def greet (name : String) : String := "Hello, " ++ name

Comments

// Single line comment

/* Multi-line
   comment */

def answer : I64 := 42

Operators

Monad supports infix operators with defined precedence:

def result : I64 := 3 + 4 * 2  // 11 (multiplication binds tighter)

Most operators are bound to a type-class method in the prelude, so they work for any type with the right instance:

A handful of operator tokens have a precedence but no binding in the prelude yet, so using them is an error: !=, <=, >=, <*>, <\|>, >>, <<, and @. The Reference has the full precedence table, and you can bind any of them yourself with infix (op) := someFunction.

Summary

In this chapter, you learned:

• How to write a basic Monad program
• That every def needs a type annotation
• Function definitions and lambdas
• Pattern matching with match
• Local bindings with let … in, chained or separated by ;
• Comments, docstrings, and operators

Next, we'll explore types, the foundation of data structures in Monad.

Types

Types are the foundation of data structures in Monad. This chapter covers inductive types, the primary way to define new types.

Basic Syntax

Types are declared with the type keyword:

type Colour {
    red,
    green,
    blue
}

This defines a type Colour with three constructors.

Constructors with Fields

Constructors can carry data:

type Shape {
    circle (radius : I64),
    rectangle (width : I64) (height : I64)
}

Natural Numbers

The canonical example of an inductive type is the natural numbers, defined in the prelude as:

type Nat {
    zero,
    succ (n : Nat)
}

This defines:

• zero: the natural number 0
• succ n: the successor of n (i.e. n + 1)

So 3 is represented as succ (succ (succ zero)).

Lists

Lists are defined inductively:

type List A {
    empty,
    cons (a : A) (List A) : List A
}

The type parameter A makes this polymorphic:

• List I64: a list of 64-bit integers
• List String: a list of strings
• List (List Bool): a list of boolean lists

List Literals

Monad supports list literal syntax [a, b, c], which desugars through the FromListLiteral class:

def nums : List I64 := [1, 2, 3]
// Desugars to:
// FromListLiteral.cons 1 (FromListLiteral.cons 2
//   (FromListLiteral.cons 3 FromListLiteral.empty))

The annotation matters: the literal is polymorphic in its container, so the checker needs the target type to pick the instance.

Tuples

Parenthesised comma-separated values are tuple literals. They desugar to right-nested Pair.pair applications, so (x, y, z) is Pair.pair x (Pair.pair y z):

def point : Pair I64 I64 := (3, 4)
def triple : Pair I64 (Pair String Bool) := (1, "two", true)

(x,) and (x) both mean just x.

Result Type

For representing computations that may fail:

type Result E A {
    ok (a : A),
    err (e : E)
}

Pattern Matching on Types

When defining functions over a type, use pattern matching:

def is_zero (n : Nat) : Bool :=
  match n {
    zero => true,
    succ _ => false
  }

def pred (n : Nat) : Nat :=
  match n {
    zero => Nat.zero,
    succ m => m
  }

def plus (n : Nat) (m : Nat) : Nat :=
  match n {
    zero => m,
    succ k => Nat.succ (plus k m)
  }

Constructors used in a pattern are written bare (zero, succ k), but constructors used to build a value need their qualified name (Nat.succ) unless the type has been opened. The prelude opens Bool, Option, Result, and Unit, which is why true, some, and ok work bare everywhere.

Recursive Functions

Functions over inductive types can be recursive:

def is_empty {A : Type} (self : List A) : Bool :=
  match self {
    empty => true,
    cons a tail => false
  }

def append {A : Type} (a : List A) (b : List A) : List A :=
  match a {
    empty => b,
    cons el_a tail => List.cons el_a (append tail b)
  }

def first {A : Type} (self : List A) : Option A :=
  match self {
    empty => none,
    cons a tail => some a
  }

Each of these recurses on a structural subterm of its argument, so the termination checker accepts them without an attribute. (List.is_empty, List.append, and List.first already exist in the prelude — these are shown as illustrations.)

Strict Positivity

A recursive type must mention itself in a strictly positive position. Its own name may appear to the right of an arrow, or as an argument to something else, but it may not sit to the left of an arrow — a constructor field whose type is a function from the type being declared:

type Bad {
    mkBad (f : Bad -> I64)      // rejected
}

error: non-strictly positive occurrence of Bad in Bad
  --> bad.mo

Both compilers apply the rule and both name the type; they differ only in how they frame the error. The host adds an In Bad: header line and a source span (error: … at 1:1, then --> bad.mo:1:1), where this compiler's syntax tree carries no span to print, so it puts the type's name after in instead. The wording of the message itself is the same on both sides.

The rule is about polarity, and it flips once per arrow. Recursing in the codomain is fine (type Fwd { mkFwd (k : I64 -> Fwd) }), and so is an arrow whose domain is itself an arrow, because two flips land back on positive (type Neg { mkNeg (h : (Neg -> I64) -> I64) }). What is rejected is an odd number of flips between the declaration and the occurrence — which is exactly the shape that lets you write a non-terminating term without any recursion at all.

This is checked for type, not for struct. The two compilers agree on the rule and both reject the example above.

Type Parameters

Types can have type parameters for polymorphism:

type Option A {
    some (a : A),
    none
}

type Result E A {
    ok (a : A),
    err (e : E)
}

Built-in Types

Monad provides these types in the prelude, available without any import:

True, Eq, and Vec are the dependently typed corner of the prelude — see Dependent Types.

Char is a stub type. Character literals ('M', '\n', 'λ') parse, type-check and compile in both implementations, but Char has no operations at all — no BEq, no ToString, no Char.* functions. A Char can be written, typed, passed and stored; nothing can inspect one. Use String for text you need to work with.

Summary

• type defines new types through constructors
• Pattern matching destructures values, one constructor level at a time
• Recursive functions operate on inductive types
• Type parameters (A) make types polymorphic
• A recursive occurrence must be strictly positive
• Tuple syntax (a, b) is sugar for Pair

Next, we'll explore type classes, Monad's mechanism for ad-hoc polymorphism.

Type Classes

Type classes provide ad-hoc polymorphism in Monad, similar to Haskell type classes and Rust traits. They allow you to define interfaces that types can implement.

Basic Syntax

Define a type class with the class keyword:

class Container (F : Type -> Type) {
    def wrap : A -> F A
    def size (fa : F A) : I64
}

Default Implementations

Class methods may provide a default body with :=:

class Describe A {
    def describe (a : A) : String := "<generic>"
    def shout (a : A) : String
}

Two limitations to be aware of today:

• An instance must still list every method it wants, including ones it is happy to take the default of. An empty instance body { } is a parse error, so there is no way to write "use all the defaults". The prelude's MonadState is the first shipped class with real defaults, and examples/state_monad.mo duly spells out all five of its methods, modify and get_map included.
• Instance methods need full type annotations. def describe x := "int" does not parse; write def describe (x : I64) : String := "int".

class Describe A {
    def describe (a : A) : String := "<generic>"
}

instance Describe I64 {
    def describe (x : I64) : String := "int"
}

Classes with Constraints

Type classes can require other classes as constraints:

class [Functor F] Applicative (F : Type -> Type) {
    def pure : A -> F A
    def apply : F (A -> B) -> F A -> F B
}

class [Applicative M] Monad (M : Type -> Type) {
    def bind (a : M A) (f : A -> M B) : M B
    def pure : A -> M A
}

The [Functor F] syntax means "F must have a Functor instance".

Multiple Parameters

Classes can have multiple type parameters:

class Convert A B {
    def convert : A -> B
}

Default Type Parameters

A class parameter can have a default, which is used when the class is named without one:

class FromListLiteral (L : Type -> Type := List) {
    def cons (a : A) (L A) : L A
    def empty : L A
}

Type Class Constraints on Functions

Functions can require instances using bracket syntax:

def process [Functor F] {A B : Type} (f : A -> B) (fa : F A) : F B :=
    Functor.map f fa

Infix Operators from Classes

You can bind an infix operator to any function, including a class method:

infix (>>=) := Monad.bind
infix (+) := HAdd.add
infix (*) := HMul.mul

The Standard Classes

These are the classes that actually ship. Note where each one lives — only the prelude ones are available without an import.

In the prelude (no import needed)

Add and HAdd are wired to each other in both directions: an HAdd A A A instance gives you Add A, and vice versa.

Elsewhere in the standard library

Known wart. Semigroup and Monoid are declared twice — once in init/foldable.mo and once in std/base.mo — with different method names (mempty vs empty). They are unrelated classes that happen to share a name. Import only one of them in a given file.

Show and Debug are deliberately different: Debug is a Rust-style diagnostic representation (it quotes strings), Show is a display string. ToString, in the prelude, is what the numeric types implement.

There is no Mul class (only HMul), and DefaultValue in the prelude is a type, not a class — the class you want is Default in std.base.

Instance Resolution Is Not Fully Checked

Instance resolution happens during evaluation, not during check. A program that uses a class method with no matching instance will type-check cleanly and then fail at run time:

eval error: unresolved global: Monad.bind

This is a real gap, not a subtlety of the design — see the Maturity Matrix. If you are relying on an instance, run the code (or a #[test]), do not just check it.

There is a second, quieter version of the same problem. Resolution keys on the head of the instance's type, so an instance whose head is a type variable can never be matched. The prelude ships two — instance MonadLiftT m m and the instance {I : Type} [IndexedMonad M] Monad (M I I) bridge — and both are, in practice, declarations of intent. Write the concrete instance out instead; see Instances.

Summary

• Type classes define interfaces for types
• Constraints [C A] require instances, on both classes and functions
• Instance methods need full annotations, and instance bodies cannot be empty
• A missing instance is currently a run-time error, not a check-time one

Next, we'll learn about instances and how to implement type classes.

Instances

Instances in Monad provide concrete implementations for type classes.

Instance Declaration

Instances are declared with instance:

type Colour {
    red,
    green,
    blue
}

instance ToString Colour {
    def to_string (c : Colour) : String :=
        match c {
            red => "red",
            green => "green",
            blue => "blue"
        }
}

Every method the class declares must appear, with full type annotations on its parameters and result. Instance bodies cannot be empty.

Instances with Constraints

Instances can require other instances as constraints, and can bind their own type parameters implicitly:

instance {A : Type} Append (List A) {
    def append (a b : List A) : List A := List.append a b
}

type Wrapper A {
    wrap (a : A)
}

instance [BEq A] BEq (Wrapper A) {
    def beq (x y : Wrapper A) : Bool :=
        match x {
            wrap a => match y {
                wrap b => BEq.beq a b
            }
        }
}

Named Instances

Instances can carry a name, which is useful when several instances for the same class would otherwise be hard to tell apart in diagnostics:

type Token {
    token (text : String)
}

instance Token.Equality : BEq Token {
    def beq (a b : Token) : Bool :=
        match a {
            token x => match b {
                token y => x == y
            }
        }
}

The name is recorded and then read by nothing: no syntax anywhere selects an instance by name. The self-hosted compiler also accepts only a single bare identifier here, where the bootstrap host takes a dotted path like the one above — write instance TokenEquality : BEq Token for code that must compile with both.

A Full Monad Instance

Monad sits on top of Applicative, which sits on top of Functor, so a new monad needs all three:

type Box A {
    box (a : A)
}

instance Functor Box {
    def map (f : A -> B) (b : Box A) : Box B :=
        match b {
            box a => Box.box (f a)
        }
}

instance Applicative Box {
    def pure (a : A) : Box A := Box.box a
    def apply (f : Box (A -> B)) (b : Box A) : Box B :=
        match f {
            box g => match b {
                box a => Box.box (g a)
            }
        }
}

instance Monad Box {
    def pure (a : A) : Box A := Box.box a
    def bind (b : Box A) (f : A -> Box B) : Box B :=
        match b {
            box a => f a
        }
}

Note that Monad declares both bind and pure; an instance that provides only bind is incomplete.

The IO Monad Instance

For comparison, here is the prelude's own instance, from init/io.mo:

type IO A {
    io A
}

def IO.pure (a : A) : IO A := IO.io a

instance Monad IO {
    def pure (a : A) : IO A := IO.pure a
    def bind (a : IO A) (f : A -> IO B) : IO B :=
        match a {
            io a => f a
        }
}

IO.pure is the constructor call sites are meant to use and Monad.bind the way to reach a value's contents; the raw io constructor is kept for those two (bind matches on it) and is not named anywhere else, which leaves it free to become an implementation detail.

Instance Resolution

Monad resolves instances by searching for one matching the required class and type, then recursively resolving that instance's own constraints. Cyclic constraint dependencies are detected with a visiting set.

Resolution happens during evaluation, not during check. If no instance matches, the program type-checks and then fails at run time:

eval error: unresolved global: Monad.bind

The most common way to hit this is assuming an instance exists when it does not.

Instances with a variable head never match

Resolution keys on the head of the instance's type. An instance whose head is a type variable rather than a concrete type therefore type-checks and is never found. The prelude ships two:

instance MonadLiftT m m { … }                              // head is `m`
instance {I : Type} [IndexedMonad M] Monad (M I I) { … }    // head is `M`

Both are written as they would be in a language with full instance resolution, and neither dispatches today. The workaround, which examples/indexed_monads.mo uses, is to write the concrete instance out: for an indexed monad Protocol, declare instance Monad (Protocol I I) with its own pure and bind rather than relying on the bridge. For example there is no Monad Result instance in the standard library, so >>= on a Result compiles and then fails. See Error Handling.

Which Instances Exist

The standard library ships 135 instances. The ones worth knowing about:

• Every fixed-width numeric type (I8–I64, U8–U64, F32, F64) has Add, Sub, HMul, Div, BEq, BOrd, and ToString
• String has BEq, BOrd, ToString, Add, Append, and Hashable
• List A has Functor, FromListLiteral, Append, and (with BEq A) BEq
• Option A has BEq (given BEq A) and Foldable
• IO and Id have Functor, Applicative, and Monad
• HashMap and BTreeMap implement Map (in std.map)
• Array (in std.array) implements nothing — Array.map and Array.foldl are plain functions, not Functor/Foldable methods

Summary

• instance declares implementations for type classes
• Instances can have constraints, implicit type parameters, and names — though nothing selects an instance by its name
• Every class method must be given, fully annotated; empty bodies are rejected
• Instance resolution is a run-time step, so exercise your code, don't just check it

Next, we'll explore structs, a convenient way to define record types.

Structs

Structs define record types with named fields, providing a convenient syntax for single-constructor types.

Basic Syntax

Structs are declared with the struct keyword:

struct Point {
    x : I64,
    y : I64
}

Creating Struct Values

Struct values are created with brace syntax. The literal is not inferrable on its own, so it needs a type from context — usually the def's own annotation:

struct Point {
    x : I64,
    y : I64
}

def origin : Point := { x := 0, y := 0 }
def p : Point := { x := 3, y := 4 }

Field Default Values

Fields can have default values using :=, and may then be omitted:

struct Rect {
    w : I64,
    h : I64 := 100
}

def wide : Rect := { w := 50 }   // h defaults to 100

Struct Update

{ base with field := value } copies a value, replacing the named fields:

struct Point {
    x : I64,
    y : I64
}

def p1 : Point := { x := 1, y := 2 }
def p2 : Point := { p1 with x := 10 }   // { x := 10, y := 2 }

Field Access

Access fields using dot notation, which chains:

struct Inner { v : I64 }
struct Outer { inner : Inner }

def get_v (o : Outer) : I64 := o.inner.v

Dot notation is field access only. x.some_function does not call Type.some_function x — there is no UFCS-style method dispatch, and naming something that is not a declared field is an error. Call functions with their qualified name: String.length s, not s.length.

The subject can be any value, including a top-level def (vzero.x), but the Rust host does not accept that form yet — see the bootstrap host appendix for why, and use a local subject when you want both compilers to accept the file.

Pattern Matching on Structs

A struct's implicit constructor is called mk, so you can match positionally:

struct Point {
    x : I64,
    y : I64
}

def swap (p : Point) : Point :=
    match p {
        mk x y => { x := y, y := x }
    }

Or match on field names, in any order, with .. to ignore the rest:

struct Point3 {
    x : I64,
    y : I64,
    z : I64
}

def flatten (p : Point3) : I64 :=
    match p {
        {y, x, ..} => x + y
    }

Destructuring in Parameters

The same field pattern works directly in a parameter position:

struct Point {
    x : I64,
    y : I64
}

def sum_point ({x, y} : Point) : I64 := x + y

Keyword Arguments

A constructor or a def can be called with its parameters named, in any order:

type Shape {
    circle (radius : I64),
    rectangle (width : I64) (height : I64)
}

def area (s : Shape) : I64 :=
    match s {
        circle r => r * r,
        rectangle w h => w * h
    }

def r : Shape := Shape.rectangle { height := 3, width := 4 }
def c : Shape := Shape.circle { radius := 5 }

A def can also declare its whole parameter list as one brace block, which is the only spelling that allows parameter defaults:

def scale {factor : I64 := 2, p : I64} : I64 := factor * p

def a : I64 := scale { p := 4, factor := 3 }   // 12
def b : I64 := scale { p := 4 }                // 8, factor defaulted

Both compilers honour it. A def's own parameter defaults now behave exactly like a struct/type field's: scale { p := 4 } is 8 everywhere, and an omitted parameter is an error only when it declares no default. See The Bootstrap Host for what is still host-only.

Linear and Affine Fields

Fields can carry a multiplicity annotation — ! (linear, exactly once), ? (affine, at most once), or nothing (unrestricted):

struct Buffer {
    !data : String,
    ?label : String,
    size : I64
}

These parse and are stored, but are not currently enforced — see Linear Types.

Structs vs Types

A struct is a single-constructor type whose constructor is named mk. This struct:

struct Point {
    x : I64,
    y : I64
}

is equivalent to:

type Point {
    mk (x : I64) (y : I64)
}

Generic Structs: a Known Limitation

struct accepts type parameters, but a generic struct is currently very hard to construct: the brace literal cannot be inferred even with an annotation (cannot infer the type of { .. }), and calling mk directly reports a type mismatch between the bare type constructor and its application.

Until that is fixed, write a generic record as a type with a positional constructor instead:

type Box A {
    mk (item : A)
}

def b : Box I64 := Box.mk 42

Summary

• struct defines record types with named fields
• Struct values use { field := value } and need a type from context
• { base with f := v } updates; {x, y} destructures, in patterns and params
• Constructors and defs accept keyword arguments; brace-form params take defaults
• Dot notation is field access, not method dispatch
• Generic structs are not usable yet — use a type instead

Next, we'll explore error handling patterns in Monad.

Error Handling

Monad provides functional error handling through the Result and Option types, both in the prelude.

The Result Type

Result E A represents a computation that may fail with an error of type E:

type Result E A {
    ok (a : A),
    err (e : E)
}

The prelude does open Result {err, ok}, so both constructors are available bare.

Basic Usage

def divide (a : I64) (b : I64) : Result String I64 :=
    if b == 0
    then err "division by zero"
    else ok (a / b)

Handling Results

Use pattern matching to handle both cases:

def handle (r : Result String I64) : String :=
    match r {
        ok n => "Success: " ++ I64.to_string n,
        err e => "Error: " ++ e
    }

++ is Append.append, which is defined for String — but it does not coerce. An I64 has to go through I64.to_string (or ToString.to_string) first.

Chaining Results

There is no Monad Result instance in the standard library, so >>= does not work on a Result. Writing it type-checks and then fails at run time with eval error: unresolved global: Monad.bind. Chain with match instead:

def divide (a : I64) (b : I64) : Result String I64 :=
    if b == 0
    then err "division by zero"
    else ok (a / b)

def double_quotient (x : I64) (y : I64) : Result String I64 :=
    match divide x y {
        ok n => ok (n * 2),
        err e => err e
    }

If you want the monadic style, define the instances yourself for your own error type — see Instances for the shape.

The Option Type

Option A represents a computation that may return nothing:

type Option A {
    some (a : A),
    none
}

Basic Usage

List.first is the prelude's canonical example:

def first_or_zero (xs : List I64) : I64 :=
    match List.first xs {
        some a => a,
        none => 0
    }

Using get_or_default

def first_or (xs : List I64) : I64 :=
    Option.get_or_default 0 (List.first xs)

Option does have a Foldable instance (in init.foldable) and, given BEq A, a BEq instance.

Custom Error Types

Define domain-specific error types as ordinary inductive types:

type DatabaseError {
    not_found,
    connection_failed,
    permission_denied,
    timeout
}

def find_user (id : I64) : Result DatabaseError String :=
    err DatabaseError.not_found

def describe (e : DatabaseError) : String :=
    match e {
        not_found => "not found",
        connection_failed => "connection failed",
        permission_denied => "permission denied",
        timeout => "timed out"
    }

Note the asymmetry: in a pattern, constructors are bare (not_found), but to build one you need DatabaseError.not_found unless you open DatabaseError.

Combining with the IO Monad

open IO {println}

def print_result (r : Result String I64) : IO Unit :=
    match r {
        ok n => println ("Success: " ++ I64.to_string n),
        err e => println ("Error: " ++ e)
    }

def main (args : List String) : IO Unit :=
    match List.first args {
        some arg => println ("First arg: " ++ arg),
        none => println "No arguments provided"
    }

Errors That Are Not Values

Not every failure is a Result. Two other kinds exist:

• Check-time errors — type mismatches, unbound variables, failed termination checks. These come out of monad check with a source span. (Termination is the exception — only the bootstrap host checks it.)
• Run-time evaluation errors — an unresolved instance, a partial match with no arm taken. These abort the program with an eval error: message. There is no exception mechanism and no way to catch them from Monad code.

Summary

• Result E A for errors with payloads, Option A for simple absence
• Pattern matching handles both; ++ needs explicit to_string conversions
• There is no Monad Result instance — chain with match
• Define custom error types as ordinary inductive types
• Evaluation errors are not catchable values

Next, we'll look at termination checking.

Modules and Imports

Monad organizes code into modules, allowing you to structure, reuse, and namespace your code.

Basic Module Structure

Each .mo file is a module. The module name is derived from its path relative to a search-path root: std/concurrent/fiber.mo is the module std.concurrent.fiber.

Importing Modules

Use use to bring a module into scope, listing exactly the names you want in {...}:

use std::process {exec_cmd, process_id}

def pid : I64 := process_id
def run : IO I64 := exec_cmd "true" []

The names in {...} are the module's own top-level definitions, and only the bare ones: a dotted definition such as List.intercalate is never bound bare — reach it by its dotted name once the module is loaded, or open its namespace.

:: separates module path segments

A use path uses :: between its segments, the way Rust does. :: is only for use: open paths name a namespace rather than a file, and dotted definition names (String.length), member access (x.field) and constructor paths (List.cons) all keep .. The separator is what tells a module path apart from a name path on sight.

:: is the only spelling a use path accepts — the corpus migration is complete, so a dotted use std.list is a parse error rather than a synonym. Both parsers enforce it (use_path_sep in lang/src/parser.mo, use_path_expression in core/src/parser.rs). The three-way rule in full:

Inside a mote, lib names that mote's own library root — Rust's crate:

use lib::parser::core {ParseResult}   // this mote's own src/parser/core.mo

That block is tagged ignore because lib only means something inside a mote, and the examples here are checked standing alone. lib is root-relative within its mote, so it reads the same from any file in it.

An empty {} still loads the module — for qualified access, and for its instances — without binding any bare names:

use std::map {}
open IO {println}

def main (args : List String) : IO Unit := println "Hello"

{*} imports every name of the module, bare and qualified; {…} imports exactly the names you list, bare and qualified; {} imports nothing but the module itself — its qualified names and its instances. The first segment must name a mote (init, std, runtime, a motes/*) or lib, the reserved alias for the importing mote's own modules. A bare use io is an error: io is a module of init, not a mote, so a bare name would silently mean whichever io.mo happened to sit beside the importing file.

Every name inside {…} must name a top-level declaration of the target module — a def, type, struct, class, instance or defmacro — by its own spelled name. A dot inside a brace item is part of a declaration's spelling, not a path separator: a dotted def is declared as one name containing a dot (def IO.println), so it is named the same way, use std::io {IO.println}. The item is a name path — one .-joined spelling — the same kind of thing you write at the call site. Naming such a def by its tail, use std::io {println}, is rejected rather than silently binding nothing, with a hint naming the spelling that works: List.length and String.length are two different declarations, so a bare length could not say which one is meant. The same rule covers a rename — {n as m} is checked against n, and use std::io {IO.println as println} is how you get the bare println — and {*}/{} are unaffected.

Opening Modules

open makes a module's definitions available without their prefix:

open IO {println}

def main (args : List String) : IO Unit := println "Hello"

Without the open, write the full path — which always works:

def main (args : List String) : IO Unit := IO.println "Hello"

What the Prelude Opens

The prelude is loaded into every file and opens these, which is why their constructors are available bare:

open Unit {unit}
open Bool {and, false, not, or, true}
open Result {err, ok}
open Option {none, some}
open True {trivial}

The Standard Library

The library is split in two, and the split is a rule, not a convention:

• init/ — pure, portable core. Code that must work in any environment, including wasm and embedded targets. No OS-specific natives.
• std/ — OS-specific implementations and genuine side effects.

IO itself (the type and its Monad instance) lives in init/io.mo; IO.println and file access live in std/io.mo, because they touch the operating system.

What is available without importing

Twelve modules are loaded ambiently: the prelude, plus id, io, number, math, string, list, the init hub, std.path, std.io, std.process, and the std hub. Everything else must be imported.

prelude is loaded for you, so there is nothing to use it for — and naming it is an error in either spelling (use prelude, use init::prelude). The prelude is ambient, so an import of it is redundant by construction; banning it also keeps its one-file-two-names wart (prelude is the one module whose name is not its file name) from spreading. The loader's own seed of it is a module path rather than a use, so the ban costs nothing.

The re-export hubs do not cover everything

use init {...} resolves to init/lib.mo, which re-exports only id, io, number, math, string, and list. use std {...} resolves to std/lib.mo, which re-exports only std.path, std.io, and std.process.

Everything else needs an explicit qualified import. This catches people out, so here is the full list:

See The Standard Library for what is in each.

How Modules Are Found

Resolution is mote-based, with the directory conventions kept underneath as the script-mode fallback. For a module path a::b, the compiler tries, in order:

First hit wins. init and std need their own cases because their module names no longer match their file names — both resolve to a lib.mo re-export hub.

A mote's library root is the file a bare use <mote> resolves to. It defaults to src/lib.mo, and the manifest's [lib] path can put it elsewhere — read into MoteManifest.lib_path and followed by resolution, so path = "lib/main.mo" is where use <mote> then reads. Only the one-segment case moves: a qualified use <mote>::foo is still <mote>/src/foo.mo, because [lib] declares a library root file and not a source directory.

Not every mote has a library root — a binary-only mote has none, and needs none. What monad check requires is that a mote name at least one target that exists on disk: a library root, or a [[bin]]. Binary targets are the build's business rather than resolution's; see Compiling and Running for [[bin]] and --bin.

One asymmetry, deliberate: the Rust host reads [lib] path but does not resolve through it, keeping its src/lib.mo convention the way it carries [link] libs without linking anything. A mote with a non-default library root is compiled by the self-hosted compiler; under monad-rs it fails as an ordinary unresolved import. That host resolves its modules relative to the checkout and cannot be aimed at a foreign mote anyway, which is why scripts/check-external-mote.sh requires the self-hosted binary.

Every one of those is anchored at the working directory or at the importing file, so all of them miss for a mote in its own repository, standing somewhere that is not a compiler checkout. That is what the rest of the search is for, and this half is what makes the word mote load-bearing rather than decorative. In order, and only after every candidate above has missed:

1. The motes/ convention. motes/{head}/src/{rest}.mo answers the qualified spelling (use example::greet reads motes/example/src/greet.mo) — the shape the fixture in examples/test_mote.mo uses. The bare-name scan beside it, which once let a one-segment use greet find the same file without naming its mote, is unreachable for a use now that a use path must begin with a mote or lib; it is kept because the dependency walk and the prelude/toolchain probes run through the same cascade.
2. The importing file's own manifest. mote.toml's declared dependency paths answer the lookup, so use std::list resolves to the dependency's real src/list.mo rather than to a directory that happens to be named like it. This is the step that makes resolution key off the mote, not the working directory, and it covers both the file's own mote root ({importing file's mote root}/a/b.mo) and its declared [dependencies.X] path entries.
3. An installed toolchain root. $MONAD_ROOT if it is set, else $MONAD_HOME (default ~/.monad) — read through active and downloads/<tag>/ — which is the directory monadup install leaves the binary and the mote sources in. This is the tier that lets a mote in its own repository build with nothing declared at all, and it is why init, std, llvm and runtime ship as an install asset rather than only as this repository.

The first three candidates are spelled relative to the checkout root, so from a directory that is not the root they miss — which is why they also consult the manifest, and why monad check src/main.mo from inside cli/ now loads its own init/std and reports nothing. Run the compiler from the checkout root and nothing changes, because the first candidate always hits there.

If none of the three tiers answers and the module was one of the ambient few (prelude, init, std), the compiler says so on one line and names the way out — monadup install, $MONAD_ROOT/$MONAD_HOME, or a path dependency — rather than only listing the modules it could not resolve.

check and test each take the same three modes: explicit paths, --workspace/-w (every mote in the enclosing workspace), or bare — the mote containing the working directory. A bare check or test outside any mote says there is nothing to do and exits non-zero; it does not print usage and report success. build now has the same three forms: an explicit file, a mote directory, or bare — the mote you are standing in. It used to print usage instead, which made it the one verb with no zero-argument form:

monad check --workspace
monad test src/main.mo
monad build cli/src/main.mo
monad build                       # the mote containing the working directory

A file with no mote.toml above it is a script module: it declares the mote it belongs to inline, with a file-level #![mote { … }] annotation whose deps are validated the way a manifest's are.

#![mote { name := "structs", deps := [init, std] }]

Three keys are accepted: name, deps and libs (the last mirroring a manifest's [link] libs). Anything else is an unknown_mote_key_error — an inline annotation never silently swallows a misspelled key.

There is still no search-path flag; that belongs to the bootstrap host. Resolution itself does have an install root, though — tier 3 above — because a mote in its own repository has no checkout to read init/std out of: the directory $MONAD_ROOT names, else $MONAD_HOME/downloads/<tag> for the tag in $MONAD_HOME/active ($MONAD_HOME defaulting to $HOME/.monad). monadup lays a nightly out in exactly that shape; see Compiling and testing for the install walkthrough.

That root is the last tier for modules, not the first, so the candidate table above can shadow it: a std/ directory that happens to sit in your working directory — the compiler's own checkout, most obviously — answers use std::map before an installed root is ever consulted. The C runtime is resolved in the opposite order (resolve_runtime_src, lang/src/module.mo), where a declared [dependencies.runtime] path and the installed root both outrank the working-directory walk. Neither order is an accident: a module path is looked up by the file doing the use, which is what makes the checkout win there, while the runtime is one file a build either has or does not.

Visibility

Declarations have three visibility levels:

pub def exported : I64 := 1        // visible everywhere
priv def internal : I64 := 2       // visible only in this file
def package_private : I64 := 3     // the default

The default is package-private. pub use module {*} re-exports an import, which is how the init and std hubs work.

Unused Imports

The compiler warns when a name listed in a use/open is never referenced:

warning: unused import `Path` from `std.path`

That warning only fires for a name that binds. An entry that binds nothing — a dotted tail, or a typo — is not a warning but an error, reported at the use line rather than left for the call site to discover (use std::list {length} is rejected because length is the dotted def List.length). So a clean use list is one whose every name is a bare declaration of its target, and the warning then tells you which of the surviving bindings are unused.

The bootstrap host can rewrite the declarations for you — monad-rs organize-imports --write computes the minimal name list, converts bare use/open to the explicit form, and deletes imports that contribute nothing. There is no equivalent in the self-hosted compiler.

Complete Example

open IO {println}

def say_hello (s : String) : IO Unit := println s

def main (args : List String) : IO Unit :=
    args
        |> List.last
        |> (Option.get_or_default "no arguments")
        |> say_hello

Summary

• Each .mo file is a module; a use path uses :: between segments
• use Module {names} loads a module; open Module {names} drops the prefix
• {*} imports everything; bare use/open is deprecated
• init/ is pure and portable, std/ is OS-specific
• Only 12 modules are ambient — most of std/ needs an explicit import
• Resolution is mote-based: a mote's own root first, the directory cascade only as the script-mode fallback
• check/test each take explicit paths, --workspace, or the mote you are standing in; compile takes a file or a mote directory
• A script module names its mote with a leading #![mote { name := …, deps := […] }]
• pub/priv/package-private control visibility

Next, we'll explore the IO monad for effectful programming.

The IO Monad

Monad manages side effects through the IO monad.

IO as a Monad

IO A represents a computation that, when executed, produces an A and may have side effects:

open IO {println}

def main (args : List String) : IO Unit := println "Hello, World!"

The IO Type

IO is defined in init/io.mo, the pure and portable half of the standard library:

type IO A {
    io A
}

def IO.pure (a : A) : IO A := IO.io a

instance Monad IO {
    def pure (a : A) : IO A := IO.pure a
    def bind (a : IO A) (f : A -> IO B) : IO B :=
        match a {
            io a => f a
        }
}

Never name the io constructor outside init/src/io.mo. Wrap a pure value with IO.pure, and reach a value's contents with Monad.bind — let x <- action; in a do block — which is what the instance above does. Constructing with IO.io, or matching on it, is not what the constructor is for, and keeping every other file off it is what leaves it free to become a native.

The operations — printing, files, the clock — live in std/io.mo, because they touch the operating system.

Basic IO Operations

open IO {println}

def main (args : List String) : IO Unit :=
    println "Hello, World!"

IO.println takes a String and returns IO Unit. It does not coerce, so print a number via I64.to_string or ToString.to_string.

Other operations in std.io:

There is no getLine — reading stdin is not implemented yet.

A wart worth knowing. Naming IO in a non-empty use filter can break do-notation's implicit Monad IO lookup at run time ("instance-Monad-IO not found"), even though the file type-checks. open's filtering is unaffected. Since IO and its instance are ambient, the fix is to import nothing at all: open IO {println} for the bare names you write, and no use line. This is a known bug in how instance resolution interacts with non-empty use filters.

Sockets and TCP

std.io also holds the whole TCP surface — two opaque types and eight blocking natives:

Socket and Listener are opaque. Each has a single zero-arity constructor so that the type checker has a name for the type; the runtime value is never one of them. That is what lets the implementation carry a bare file descriptor instead of a handle — so nothing may pattern-match, compare or print either.

/// Send one request over a fresh connection and return whatever comes back.
/// Every step can fail, so each is matched on rather than discarded.
def fetch (host : String) (port : U16) : IO (Result String String) := do {
    let opened <- IO.tcp_connect host port;
    match opened {
        Result.err e => return (Result.err e),
        Result.ok sock => do {
            let sent <- IO.tcp_write sock (String.to_list "GET / HTTP/1.0\r\n\r\n");
            match sent {
                Result.err e => do {
                    IO.tcp_close sock;
                    return (Result.err e)
                },
                Result.ok _ => do {
                    let got <- IO.tcp_read sock 4096u64;
                    IO.tcp_close sock;
                    match got {
                        Result.err e => return (Result.err e),
                        Result.ok bytes => return (Result.ok (String.from_list bytes))
                    }
                }
            }
        }
    }
}

IO.tcp_listen 0u16 binds 0.0.0.0 on an OS-assigned port; read the port it actually settled on back with IO.tcp_local_port:

open IO {println}

/// Listen on an OS-assigned port, print it, accept one connection, echo back
/// what it sends, and close everything.
def echo_once : IO Unit := do {
    let bound <- IO.tcp_listen 0u16;
    match bound {
        Result.err e => println e,
        Result.ok listener => do {
            let port <- IO.tcp_local_port listener;
            println (U16.to_string port);
            let accepted <- IO.tcp_accept listener;
            IO.tcp_close_listener listener;
            match accepted {
                Result.err e => println e,
                Result.ok conn => do {
                    let got <- IO.tcp_read conn 1024u64;
                    match got {
                        Result.err e => println e,
                        Result.ok bytes => do {
                            let written <- IO.tcp_write conn bytes;
                            match written {
                                Result.err e => println e,
                                Result.ok n => println (U64.to_string n)
                            }
                        }
                    };
                    IO.tcp_close conn
                }
            }
        }
    }
}

IO.tcp_close_listener closes the listening socket only; connections already accepted from it keep working, which is why the snippet above can close the listener and then talk on conn. IO.tcp_write writes all of the bytes it is given — the count it returns is the full length, never a partial one, so there is no write loop to write.

What is not there

• TCP is self-hosted only. The eight natives are implemented by runtime/src/runtime.c, which the self-hosted backend compiles; the Rust bootstrap host deliberately has no TCP implementation at all, so under it any of these fails at run time with unknown native: tcp_listen (or whichever was called). A socket test therefore cannot run under cargo run -- test, and the examples/ HTTP entry is pure by design for exactly that reason.
• No read timeout, and no non-blocking mode. tcp_connect, tcp_accept and tcp_read block until they complete. A peer that connects and then sends nothing holds the accepting fiber and its OS thread indefinitely; nothing in the library breaks that. The mitigation in motes/moon/src/server.mo is a cap on requests served per connection, which bounds an idle keep-alive client, not a silent one. A real timeout is not implemented.
• EOF is not an error. When the peer closes, IO.tcp_read returns Result.ok List.empty rather than failing, and read loops terminate on exactly that. IO.tcp_close never fails.

A working server and client built on these live in motes/moon/src/server.mo and motes/moose/src/client.mo.

Do Notation

A do block sequences monadic actions. Two equivalent spellings:

do { ... }

open IO {println}

def greet : IO Unit := do {
    println "Enter your name:";
    println "Hello!"
}

Inline block on the definition

A definition can use { ... } directly in place of := do { ... }:

open IO {println}

def greet : IO Unit {
    println "Enter your name:";
    println "Hello!"
}

def greet_with_name (name : String) : IO Unit {
    let greeting := "Hello, " ++ name;
    println greeting
}

Separate statements with ;. Two adjacent expressions without a semicolon are parsed as a single application, which produces a confusing error like expected a function type, found (IO Unit).

Do Block Statements

A worked example using all four:

open IO {println}

def show_home : IO Unit {
    println "Looking up $HOME";
    let home <- IO.get_env "HOME";
    let shown := Option.get_or_default "(unset)" home;
    println shown
}

def five : IO I64 {
    let x := 5;
    return x
}

Do notation is not IO-specific — it works for any type with a Monad instance. The standard library provides Monad IO and Monad Id; notably not Monad Result or Monad Option.

Native Functions

IO operations are implemented as natives that call into Rust:

#[native print_str]
def IO.println (s : String) : IO Unit

The #[native name] attribute marks a definition as implemented outside Monad, and such a definition has no body. The name in the attribute is the runtime's identifier for the operation, which is not always the Monad-side name — the native behind IO.println is print_str.

There are 146 natives declared across init/ and std/. Three — eq_rec, string_to_chars, and string_from_chars — are declared but not implemented anywhere, and calling one fails at run time with unknown native. The compiler backend wires a subset of the rest; see Compiling and Running. The eight tcp_* natives above are among the wired ones, but only in the self-hosted backend — the Rust host has no TCP implementation at all.

Running IO Programs

The runtime executes main, passing command-line arguments as a List String:

open IO {println}

def main (args : List String) : IO Unit :=
    println "Starting..."

monad build program.mo -o program
./program arg1 arg2      # args reach `main`

main may also return I64, in which case it becomes the process exit code. See Compiling and Running.

Combining IO with Other Types

open IO {println}

def print_result (r : Result String I64) : IO Unit :=
    match r {
        ok n => println ("Success: " ++ I64.to_string n),
        err e => println ("Error: " ++ e)
    }

def main (args : List String) : IO Unit :=
    print_result (ok 42)

Summary

• IO A encapsulates side effects; the type is in init.io, the operations in std.io
• do notation sequences actions, in both do { } and inline def f : T { } form
• Statements must be separated by ;
• IO is a proper monad with pure and bind
• main is the entry point, receiving List String
• Natives bridge Monad and Rust

That concludes the tutorial. The Advanced chapters go deeper: dependent types, macros, linear types, and concurrency.

Dependent Types

Monad supports dependent types, where types can depend on values. This enables precise specifications and expressive type signatures.

Pi Types (Function Types)

The standard function type A -> B is a Pi type where the result type does not depend on the input value:

def add (a : I64) (b : I64) : I64 := a + b

A parameter can be named in the type, which is what makes the dependent case possible — a later parameter's type may mention an earlier parameter.

Forall Types (Implicit Arguments)

The {A : Type} syntax introduces implicit arguments, inferred by the checker:

def identity {A : Type} (x : A) : A := x

// Called without specifying A:
def n : I64 := identity 42
def s : String := identity "hello"

Holes

The _ placeholder is a hole: it asks the checker to infer that type.

def f (x : I64) : I64 := (x : _)

Holes work in type position inside a definition — an annotation, a parameter type — where unification treats them as matching anything. They do not let you omit a def's own signature: def x := _ is a parse error, because the signature itself is mandatory.

A hole in value position is accepted and then goes nowhere. Writing _ where a value belongs parses, but lowering rejects it as a type-level term under monad eval and emits a void placeholder under monad build. Use holes for types you want inferred, not as a stand-in for code you have not written.

Universes

Monad's universes are written with Sort:

def a : Sort 1 := I64
def b : Sort 2 := Sort 1

Type and Prop are names for the first two levels:

So I64 : Type, and Type itself is Sort 2. Note that Type takes no argument: Type 1 is not universe syntax — it parses as Type applied to the integer 1, which is not what you want. Use Sort 2.

def i : Type := I64
def same : Sort 1 := I64

Prop and Propositions

Prop is Sort 0, the universe of propositions. The prelude defines the trivially true proposition:

def t : True := trivial

Propositional Equality

The prelude defines equality as an inductive family in Prop, with the usual single constructor refl:

type Eq (A : Sort 1) (a : A) (b : A) : Prop {
    refl : Eq A a a
}

/// The J eliminator
#[native "eq_rec"]
def Eq.rec (A : Sort 1) (a : A) (P : (b : A) -> Eq A a b -> Sort 1)
    (h : P a (Eq.refl a)) (b : A) (e : Eq A a b) : P b e

Because refl only builds Eq A a a, a value of type Eq A x y is a proof that x and y are definitionally equal:

def one_is_one : Eq I64 1 1 := Eq.refl 1
def a_is_a : Eq String "a" "a" := Eq.refl "a"

[!WARNING] Eq is type-checking-only today. Constructing and annotating an equality proof works, but there is no way to use one: Eq.rec's native (eq_rec) is declared and not implemented, and pattern matching on refl fails at run time with expected 0 constructor fields, got 1. The prelude's own tests for Eq acknowledge this — they check that construction type-checks and stop there.

So Eq currently documents an intent in the type system rather than enabling proof-carrying code.

Length-Indexed Vectors

The prelude's Vec is indexed by its length, so the type records how many elements the value has:

type Vec (len : Nat) A {
    nil : Vec Nat.zero A,
    cons (head : A) (tail : Vec len A) : Vec (Nat.succ len) A
}

Each constructor produces a different index, so a Vec of the wrong length is a type error:

def empty_vec : Vec Nat.zero I64 := Vec.nil
def one_vec : Vec (Nat.succ Nat.zero) I64 := Vec.cons 1 Vec.nil

What Is Not Implemented Yet

Monad is deliberately not a proof assistant, and the dependently typed surface is correspondingly small. Today there is:

• No dependent pattern matching. A match does not refine the types of other variables in scope based on which constructor matched, so writing functions that consume a Vec while tracking its length is painful.
• No usable equality elimination. See the warning above: Eq proofs can be built but not consumed.
• No tactics, no proof automation, no Decidable. Proofs are written by hand as terms.
• No universe polymorphism. Levels are concrete numbers.
• No definitional unfolding controls (@[reducible] and friends).

See the Maturity Matrix for where this sits relative to the rest of the language.

Summary

• Pi types are function types; naming a parameter lets later types depend on it
• {A : Type} introduces implicit arguments, inferred at the call site
• Holes _ infer a type inside a definition, but never the definition's own signature
• Universes are Sort N; Prop is Sort 0 and Type is Sort 1
• Eq/refl and Eq.rec give propositional equality with a J eliminator
• Vec is a working length-indexed vector

Next, we'll explore macros and derive.

Macros and Derive

Monad has a real macro system: defmacro, quote, and compile-time reflection. It is not a bolted-on preprocessor — #[derive] is implemented in Monad, in std/derive.mo, on top of these primitives. The compiler only supplies a few reflection intrinsics.

This is the one area where the self-hosted compiler is ahead of the bootstrap host: term macros work here and not there. #[derive …] is the reverse, and is marked below.

Quoting

quote { ... } turns a term into data instead of evaluating it:

quote { 1 + 2 }

Defining a Macro

There are two forms of defmacro.

Term macros produce an expression:

defmacro double x := x + x
def y : I64 := double! 9

Self-hosted only. Term macros are rejected by the bootstrap host, which fails with "macro double did not return a Term value". Declaration macros (below) work on both.

Declaration macros produce a list of top-level declarations, using a decls { ... } template:

defmacro derive_lens T := decls {
    reflect_type_info! T derive_lens_meta
}

A macro is invoked with a ! suffix — double! 9, derive_lens! Point.

Reflection as Data

The interesting half is reflect_type_info!, a compiler intrinsic that hands a type's structure to an ordinary Monad function as an ordinary value. That function computes a List Decl, and the compiler splices the result back into the program.

The data model lives in init/meta.mo:

type FieldInfo {
    field_info (name : String) (typ : Expr) (attrs : List String)
}

type CtorInfo {
    ctor_info (name : String) (fields : List FieldInfo)
}

type TypeInfo {
    type_info (name : String) (ctors : List CtorInfo)
}

and a deliberately minimal mirror of the compiler's own term and declaration surface:

type Expr {
    e_var (name : String),
    e_str (value : String),
    e_int (value : I64),
    e_bool (value : Bool),
    e_app (func : Expr) (arg : Expr),
    e_lam (param_name : String) (param_typ : Expr) (body : Expr),
    e_if (cond : Expr) (then_ : Expr) (else_ : Expr),
    e_match (scrutinee : Expr) (arms : List MatchArm),
    e_ctor (ctor_name : String) (args : List Expr)
}

type Decl {
    d_def (name : String) (params : List Param) (ret_typ : Expr) (body : Expr),
    d_instance (class_name : String) (target_typ : Expr) (methods : List Decl),
    d_error (message : String)
}

The payoff is that a "macro" is a normal function you can read, test, and debug. A derive backend is written with List.map, match, and recursion — not with quasi-quotation gymnastics:

pub def derive_lens_meta (info : TypeInfo) : List Decl :=
    match info {
        type_info type_name ctors =>
            match ctors {
                cons c tail =>
                    match tail {
                        empty => lens_decls_for_ctor type_name c,
                        cons _ _ => List.empty
                    },
                empty => List.empty
            }
    }

d_error is the escape hatch: returning one anywhere in the list fails macro expansion with that message, which is how a derive rejects a type it cannot handle.

#[derive ...]

Works on both compilers. The self-hosted compiler bridges the attribute to the same std/derive.mo macros the host calls (derive_bridge_decls, lang/src/typecheck/macro_queue.mo), so #[derive BEq BOrd Debug Lens] generates its instances either way. What you must do on both is import the backend — #[derive BEq] dispatches by name to a macro, and a macro that is not in scope is "macro derive_beq not found".

The attribute form dispatches to those macros by name. Arguments are space-separated bare names — not #[derive(BEq, BOrd)]:

use std::derive {derive_beq, derive_bord, derive_debug, derive_lens}
use init::optics {Lens, set, view}
use std::debug {Debug}

#[derive BEq BOrd Debug Lens]
struct Point {
    x : I64,
    y : I64
}

#[test]
def test_equality : Bool :=
    let p1 : Point := { x := 1, y := 2 } in
    let p2 : Point := { x := 1, y := 2 } in
    let p3 : Point := { x := 1, y := 3 } in
    p1 == p2 && Bool.not (p1 == p3)

#[test]
def test_debug : Bool :=
    let p : Point := { x := 1, y := 2 } in
    Debug.debug p == "Point { x: 1, y: 2 }"

#[test]
def test_lens : Bool :=
    let p : Point := { x := 1, y := 2 } in
    view Point.x p == 1 && view Point.y (set Point.y 9 p) == 9

What can be derived

Derives work on multi-constructor types too:

use std::derive {derive_beq, derive_bord, derive_debug}
use std::debug {Debug}

#[derive BEq BOrd Debug]
type Suit {
    hearts,
    spades,
    number (rank : I64)
}

#[test]
def test_suit : Bool :=
    Suit.number 7 == Suit.number 7
        && Suit.hearts < Suit.spades
        && Debug.debug (Suit.number 7) == "Suit::number { rank: 7 }"

Lens is deliberately absent there — a lens focuses on one field of one shape. For sum types, init.optics provides Prism instead.

You must import the backend

#[derive BEq] dispatches to derive_beq by name, so the module defining it has to be in scope:

use std::derive {derive_beq, derive_bord, derive_debug, derive_lens}

The compiler's unused-import analysis does not see macro-name dispatch as a reference, so it will report these as unused. Keep them — removing the import makes #[derive BEq] fail with "macro derive_beq not found".

Writing Your Own Derive

Because a derive is just a TypeInfo -> List Decl function plus a two-line defmacro, adding one is ordinary programming. lang/cli.mo does exactly this for #[derive_cli], generating an argv parser from a struct's fields and their #[arg] annotations — the field attributes come through in FieldInfo.attrs.

Limitations

• Only the four targets above are wired into the #[derive ...] attribute; your own macros are called with ! syntax.
• Expr is not a full mirror of the compiler's Term: Pi, Forall, Sort, Ann, and Quote are excluded, because no shipped derive needs them.
• TypeInfo does not carry a type's generic parameters, per-field defaults, or field multiplicities.

cli/src/main.mo hand-writes its own argv parser rather than using #[derive_cli], and stays free of macro syntax on purpose: the self-hosted parse/scope/typecheck suite re-parses that file through the self-hosted pipeline, and it is the one file where an attribute would be load-bearing for the bootstrap itself. cli/src/tests/cli_derive_tests.mo is the derived equivalent.

Summary

• defmacro defines term macros and declaration macros; quote { } makes syntax data
• reflect_type_info! passes a type's structure to an ordinary Monad function
• #[derive BEq BOrd Debug Lens] — space-separated, and the backend must be imported
• Derives are library code in std/derive.mo, not compiler built-ins
• Both compilers expand #[derive …]; term macros (double!) are self-hosted-only, which is the one divergence left in this area

Next, we'll look at linear types.

Termination Checking

Monad checks recursive definitions for termination. The check is structural, and both compilers run it, on every def, by default.

[!WARNING] The check is structural, and both compilers enforce it. A recursive call is accepted only when one of its arguments is a subterm bound by pattern matching inside the corresponding parameter, so recursion over List, Nat or any inductive type is fine while counting down an I64 is not — that needs #[terminating] or #[partial]. It is the case you are most likely to hit.

Why It Exists

In a dependently typed language, the type checker evaluates terms. A non-terminating definition would make the checker loop, and — because a looping definition can be given any type — would make the logic unsound. Only definitions that provably terminate can be unfolded safely.

The Rule: Structural Recursion

A recursive call is accepted when at least one argument is a structural subterm of the corresponding parameter: something bound by pattern matching inside that parameter, and therefore strictly smaller.

This is accepted, because tail comes out of destructuring xs:

def length {A : Type} (xs : List A) : I64 :=
    match xs {
        empty => 0,
        cons a tail => 1 + length tail
    }

So is this, recursing on m from succ m:

def double_nat (n : Nat) : Nat :=
    match n {
        zero => Nat.zero,
        succ m => Nat.succ (Nat.succ (double_nat m))
    }

Mutual recursion works too, as long as each step is structural:

def is_even (n : Nat) : Bool :=
    match n {
        zero => true,
        succ m => is_odd m
    }

def is_odd (n : Nat) : Bool :=
    match n {
        zero => false,
        succ m => is_even m
    }

What Gets Rejected

Arithmetic recursion is the common case. n - 1 is a computed value, not a subterm of n, so the check cannot see that it decreases:

def countdown (n : I64) : I64 :=
    if n == 0 then 0 else countdown (n - 1)

Both compilers reject it, in the same words — below is the host's output, with the elaborated call elided:

error: Termination check failed for 'countdown'
  Recursive call: (countdown (... n 1i64))
  Argument(s) (...) are not structural subterms of parameter(s) (n)
    — add #[terminating] if this function is well-founded

The error prints the recursive call after elaboration, so the subtraction arrives as its desugared Sub dispatch — and the two compilers spell that dispatch differently (the host inlines the dictionary into a match, this compiler keeps it as a call), so the middle line is the one line of the message that differs between them. It is noisy either way, but the parameter names at the end tell you what it wanted.

The Attributes

Three attributes turn the check off for one definition, in both compilers. They are the only way to write recursion the structural rule cannot see.

#[terminating]

"I have checked this by hand; it is well-founded." Use it when the recursion really does decrease but not structurally — the arithmetic case above.

#[terminating]
def factorial (n : I64) : I64 :=
    if n == 0
    then 1
    else n * factorial (n - 1)

#[partial]

"This may not terminate, and that is intended." Use it for interpreters, driver loops, and search that may not converge.

#[partial]
def spin (n : I64) : I64 := spin n

#[decreasing <measure>]

#[terminating], plus a note to the reader of which argument is meant to be shrinking. Use it where "it terminates" alone would leave the next reader guessing.

#[decreasing n]
def fact_acc (n : I64) (acc : I64) : I64 :=
    if n == 0 then acc else fact_acc (n - 1) (n * acc)

The named measure is not checked — not against the parameter list, not against the recursive calls. It is documentation the compiler agrees to accept, and it exempts the definition exactly as #[terminating] does.

The difference between the three is what you are telling the reader: #[terminating] is a claim about the code, #[decreasing x] is the same claim with its reason named, and #[partial] is an admission. Nothing verifies any of them, so an incorrect #[terminating] passes both compilers — and a definition the host's checker unfolds while type-checking will hang it.

Practical Guidance

The rule is narrow, so most recursion falls into one of three cases:

• Recursing over List, Nat, or any inductive type usually just works — recurse on what the match bound, not on something you computed.
• Counting down an I64 needs #[terminating]. This is by far the most common case.
• Converting the loop counter to Nat makes the recursion structural and removes the need for the attribute, at the cost of unary arithmetic.
• The standard library uses these attributes freely; they are not a code smell.

Code written this way is accepted by both compilers, and stays accepted if the checker ever grows stricter than the structural rule.

Limitations

In both implementations the check is deliberately simple:

• No termination inference beyond the structural rule — no size measures, no lexicographic orderings, no user-supplied well-founded relations.
• The attributes are trusted, not verified.
• Accumulator-passing recursion where the decreasing argument is not the structurally-matched one is not recognised.

Next, we'll look at linear types.

Linear Types

Monad's design calls for linear and affine types for resource-safe programming, inspired by Rust's ownership system and Idris's Quantitative Type Theory (QTT).

[!WARNING] The syntax parses; nothing is enforced. Struct fields, def parameters, lambda parameters and destructured parameters all accept !, ? and % in the self-hosted compiler. Every one of those annotations is then dropped before type checking — no use is counted, and every binder the checker builds is Many.

So today a multiplicity is documentation that the compiler carries as far as its own AST and no further. This chapter documents the intended design; see Where this actually stands for the state of the implementation.

Overview

Every variable in Monad is meant to carry a multiplicity controlling how many times it may be used:

What Parses Today

Struct fields accept all four, in both implementations:

struct Buffer {
    !data : String,
    ?label : String,
    size : I64
}

So do parameters, on definitions and on typed lambda parameters:

def f (!a : I64) (?b : I64) (%c : I64) (d : I64) : I64 := a + b + c + d
def h : I64 -> I64 := fn (!x : I64) => x

Two things about the parameter form are easy to get wrong:

• The prefix applies to the whole group, not one name. (!x y : I64) marks both x and y linear. Write separate groups if you meant otherwise.
• A lambda parameter must be parenthesised and annotated. Bare \ !x => x is a parse error in both implementations.

A destructured parameter takes a prefix too:

struct Coord { fst : I64, snd : I64 }

// Self-hosted only -- the bootstrap host rejects a prefix on this form.
def sum_coord (!{fst, snd} : Coord) : I64 := fst + snd

All of it is recorded on the parse tree and then discarded.

Usage Rules (design)

The intent is that these are checked at compile time, with no run-time overhead:

1. Linear (!x): must appear exactly once in the body
2. Affine (?x): must appear at most once
3. Many (x): unrestricted
4. Zero (%x): must not appear in run-time position at all

def ok (!x : I64) : I64 := x           // intended: passes
def unused (!x : I64) : I64 := 42      // intended: fails — never used
def overused (!x : I64) : I64 := x + x // intended: fails — used twice
def affine_ok (?x : I64) : I64 := 42   // intended: passes
def many_ok (x : I64) : I64 := x + x   // passes

Today all five compile, in both implementations.

Where This Actually Stands

Parsing is done. What is left is everything after it:

1. Lowering keeps nothing. The parser records a multiplicity on each parameter, and the pass that builds the core pi/lam terms has nowhere to put it — those terms have no multiplicity field. It is dropped there.
2. Usage checking, in both implementations. Counting machinery was written against an earlier version of the host's type checker. That checker has been replaced and the current one does not call it — every function type it builds uses Many.
3. Codegen use, in the self-hosted backend. Nothing consumes multiplicities.

So the annotations are documentation that the compiler carries as far as its own parse tree.

Why It Matters Beyond Correctness

Multiplicities are also the intended basis for memory management. Compiled binaries currently reach for a conservative garbage collector because codegen never emits a free — see Compiling and Running. The plan is for linear and affine information to tell the backend exactly where a value's last use is, so it can free deterministically and drop the GC.

That is the strongest argument for finishing this work, and it is why the GC is described as a stopgap rather than a design choice.

Comparison to Rust

Roadmap

Roughly in order:

• Wire multiplicity_prefix into the self-hosted definition- and lambda-parameter parsers — done, destructured parameters included
• Carry the multiplicity through lowering, so pi and lam can hold one
• Reinstate usage checking in the current type checker
• Track let-bound variables, not just parameters
• Check arrow multiplicity at application sites
• Enforce multiplicities on constructor fields under pattern matching
• Subsumption: Many should subsume Linear and Affine
• Drive codegen's memory reclamation from multiplicities, replacing the GC
• noalias attributes on linear parameters in the emitted LLVM IR

Next, we'll explore concurrency.

Concurrency

Monad ships fiber-based concurrency primitives in std.concurrent. Read the constraints in this chapter before designing around them: the compiled backend runs fibers on real OS threads, so forkIO is genuinely parallel — and the bootstrap host is the one that is lazy.

That is the reverse of how this chapter used to read, and of how most runtimes work. Both implementations accept the same programs; they differ in what a forkIO means.

What It Actually Does

forkIO starts a thread. It creates a pthread running the action, returns an opaque handle immediately, and the thread proceeds on its own. await_fiber joins that thread and yields its result.

let f <- forkIO action;
let result <- await_fiber f;

Above, action is already running by the time await_fiber is called, and a second forkIO before the first await starts a second thread that really does overlap with it.

The model is 1:1 pthreads, deliberately: compiled Monad code recurses deeply (main raises RLIMIT_STACK to 128 MB), so a small green-thread stack would overflow on the first recursive helper. Each fiber therefore reserves the same 128 MB of address space, committed only as it is touched, so a fiber that does not recurse deeply costs nothing in RSS. This does not scale to a hundred thousand fibers, and it is explicitly the interim design — the plan is to replace the handle's atomic refcount with the ownership discipline in Linear & Affine Types.

cancel_fiber records the cancellation; it does not preempt. pthread_cancel would leave Boehm's allocator lock held and the thread unregistered, so the cancellation is a flag that await_fiber refuses to hand a result for — the same observable behaviour as the host, which can only cancel a fiber it has never started. A scope_drop likewise cancels the fibers forked through that scope rather than waiting on them.

The host's model, for contrast: forkIO captures the action and returns, and await_fiber applies the closure synchronously on the calling thread. Nothing there can interleave or run in parallel, which is why it is the host's interpreter — not the compiled binary — that cannot make anything faster.

Which Backend Am I On?

Almost every test in std/src/concurrent/ passes under both models, because it awaits the fiber it just forked — a deferred thunk plus an inline await satisfies those identically. combine_test.mo's test_sleepIO_fibers_run_concurrently is the one that can tell them apart: it forks four 500 ms sleeps before awaiting any of them, and asserts the whole thing finishes in under 1200 ms.

compiled  -> the sleeps overlap  -> ~500 ms   -> passes
host      -> the sleeps are a sum -> ~2000 ms -> fails

That test is therefore a self-hosted-only expectation, and CI's sweep runs it self-hosted.

Fibers

std.concurrent.fiber:

type Fiber (A : Type) {
  fiber
}

#[native fork_io]    def forkIO (action : Unit -> IO A) : IO (Fiber A)
#[native await_fiber] def await_fiber (f : Fiber A) : IO A
#[native cancel_fiber] def cancel_fiber (f : Fiber A) : IO Unit

Fiber handles are opaque runtime objects — do not pattern match on them.

use std::concurrent::fiber {await_fiber, forkIO}

def answer (_ : Unit) : IO I64 := IO.pure 42

#[test]
def test_fork_and_await : IO Bool {
    let f <- forkIO answer;
    let result <- await_fiber f;
    return (result == 42)
}

Combinators

std.concurrent.combine builds structured-concurrency combinators on top:

sleepIO is a real blocking sleep (nanosleep), so it costs a whole thread while it runs.

race "wins" by taking the head of the list, not by observing which fiber finishes first. It is therefore deterministic, and it is the right primitive only when every fiber computes the same thing — race is a cancellation shorthand, not a scheduler. That is a choice in combine.mo and not a limit of the runtime: the threads really do race, this function simply does not look at who won.

use std::concurrent::fiber {Fiber, forkIO}
use std::concurrent::combine {all}
use std::list {}

def answer (_ : Unit) : IO I64 := IO.pure 42

#[test]
def test_all : IO Bool {
    let f1 <- forkIO answer;
    let f2 <- forkIO answer;
    let results <- all [f1, f2];
    return (List.length results == 2)
}

Duration is defined as a struct wrapping milliseconds, but sleepIO currently takes a bare I64.

What It Costs

Fiber handles are opaque runtime objects tagged in their header, so a match on one fails loudly rather than reading a heap address as a constructor tag. The refcount in that header is what keeps a Scope's fibers alive, and it is the only thing in the compiled runtime that uses it — the compiler still emits no retain/release calls for ordinary values, because deterministic freeing is blocked on linear types.

A fiber nobody ever awaits or cancels keeps its thread entry until the process exits: a few hundred bytes each. Reclaiming it would mean joining threads whose result nobody wants, so scope_drop does not.

What Does Not Exist

• A way to spawn a raw OS thread from Monad code — the only entry point is forkIO, which gives you a Fiber
• A scheduler, work stealing, or preemption
• async/await syntax
• Channels, mutexes, or semaphores exposed to Monad
• Futures, or any notion of a task completing "later"
• A guarantee about the order threads run in, or which of two racing fibers finishes first

The Rust side of the repository does contain a real threaded scheduler (core/src/runtime/, with scheduler.rs, channel.rs, mutex.rs, semaphore.rs, reactor.rs), but nothing in std/concurrent/*.mo reaches it: the compiler's own runtime is the C one in runtime/src/runtime.c. Treat that Rust code as groundwork for a future runtime, not as something you can use today.

Summary

• Compiled forkIO starts a real thread; await_fiber joins it. That is parallelism.
• The host is the lazy one: it defers to the first await, so nothing there interleaves
• Cancellation is recorded, never preemptive
• all, race, scoped, and cancel_all are combinators over either model; race takes the head rather than observing a winner
• sleepIO genuinely sleeps, and holds a thread while it does
• std/src/concurrent/combine_test.mo carries the one test that distinguishes the two backends

See the Maturity Matrix, and The Standard Library for what else std/ provides.

Compiling and Running

Monad compiles to native binaries through LLVM. The compiler is written in Monad, lives in lang/, and compiles itself.

To run a program you compile it and execute the binary — monad run does both in one step. There is also monad eval, a built-in interpreter, but only eight pure natives are wired into it, so it is a tool for arithmetic-and-strings programs rather than a way to run real ones.

Getting a Compiler

The compiler is written in the language it compiles, so the first one has to come from somewhere else. That is what the Rust bootstrap host is for:

cargo build --release
cargo run --release -- run cli/src/main.mo build cli/src/main.mo -o "$PWD/monad"

That produces monad, a native binary that needs nothing else. Everything below uses it.

The absolute -o is not decoration. A relative output name is resolved against the compiler's default output directory, /tmp/monad_out_<pid> — see Where the binary lands.

You will also need llc, clang, and the Boehm GC development files on the system — devenv shell provides all three.

Or install a nightly

Every push to main publishes a prerelease, and scripts/monadup installs one:

curl -fsSL https://raw.githubusercontent.com/monad-lang/monad/main/scripts/monadup -o monadup
chmod +x monadup
./monadup self-install
export PATH="$HOME/.monad/bin:$PATH"
monadup default       # install the latest nightly and make it active
monad version

monadup list / use <tag> / update / uninstall <tag> manage the installed set under ~/.monad. It needs curl, tar and either jq or python3.

The nightly is built inside the Nix devenv and links against store paths, so on a machine without those it will not run — monadup says so rather than leaving you to discover it. Until that is fixed, building from source is the portable route.

An install directory holds more than the compiler:

~/.monad/downloads/<tag>/
  monad-nightly-x86_64-linux   the compiler
  commit.txt                   the commit it was built from
  init/  std/  llvm/  runtime/ the mote sources
  mote.toml                    those four, as a workspace

Those motes are what let you use the compiler on a program of your own — use std::map and the C runtime both resolve out of that directory. Without them, only a checkout of the compiler repository can compile anything. Nightlies published before the sources asset existed install the binary alone and say so; re-running monadup install adds the sources once a release ships them.

MONAD_ROOT points the compiler at a different set of sources, for a root that is not a monadup install (an unpacked copy, or a checkout):

MONAD_ROOT=/path/to/tree-with-init-std-runtime monad check

Two artifacts, both Linux x86_64 only: monad-nightly-x86_64-linux (the compiler) and monad-src-x86_64-linux.tar.gz (the sources above).

Your First Program

open IO {println}

def main (args : List String) : IO Unit := println "Hello, World!"

monad run hello.mo

Hello, World!

Or compile it and keep the binary — with an absolute output path, for the reason just above:

monad build hello.mo -o "$PWD/hello"
./hello

The Commands

monad build [<path>] [name] [--bin <name>] [--output/-o <name>] [--verbose/-v] [--debug/-g] [--release] [--no-cache]
        Parse, type-check and compile a .mo source file to a native binary.
        <path> may also be a mote DIRECTORY, in which case one of its [[bin]]
        targets is built: `monad build cli` builds cli/src/main.mo as `monad`,
        the name that mote's [[bin]] declares. A mote that declares no [[bin]]
        table has one target anyway -- src/main.mo, named after the mote --
        and a library mote that declares none and has no src/main.mo is
        refused rather than guessed at.
        `--bin <name>` picks one when several of a mote's [[bin]] targets
        exist on disk -- which is what the refusal above counts, rather than
        what the manifest declares.
        With NO <path>, builds the mote containing the working directory --
        the same default `check` and `test` have. `monad build` and
        `monad build .` are one code path.

        This verb was called `monad compile` until 2026-09-29. There is no
        alias: two verbs that both produce a binary differ only in which one
        you remember.

monad run <path> [--verbose/-v] [--debug/-g] [--release]
        Compile and then execute. The binary is always called `run_out`, so
        there is no -o; the program's exit code becomes monad's.

monad eval <path> [--verbose/-v]
        Evaluate with the built-in interpreter. Pure programs only.

monad pretty <path>
        Parse and pretty-print a .mo source file.

monad check [<path>...] [--workspace/-w] [--verbose/-v] [--no-cache]
        Parse and type-check; no execution.
        Any <path> that is a directory is expanded recursively to its *.mo files.
        With no <path>, checks the mote containing the working directory;
        --workspace checks every mote in the enclosing workspace.
        --no-cache (or MONAD_NO_CACHE) skips the cache; a single-file run always does.
        With no <path> and no mote above the working directory it prints why
        and exits 1, rather than reporting a pass for having checked nothing.

monad test [<path>...] [--workspace/-w] [--verbose/-v]
        Compile each file's own #[test] defs into a native binary and run it.
        Any <path> that is a directory is expanded recursively to its *.mo files.
        With no <path>, tests the mote containing the working directory;
        --workspace tests every mote in the enclosing workspace.
        A file with no #[test]s is skipped rather than failed. A file that
        defines its own main is fine: that main is renamed out of the way
        and the generated test driver becomes the entry point.

monad version
        Print the git commit this binary was built from.

Running monad with no arguments prints this usage.

Flags are position-independent — monad build -v hello.mo and monad build hello.mo -v are the same command. --output/-o takes its value as a separate argument: --output=NAME is not recognised.

monad test with no paths covers the mote containing the working directory, so it enumerates that mote's sources; --workspace covers every member. Pass explicit paths for anything else. With no paths and no mote above the working directory it says so and exits 1, exactly as check does — there is nothing to test, and reporting a pass for it would read as one. Resolution keys off the mote doing the use, so an invocation from inside a mote finds its own init/std dependencies — there is no need to run it from the workspace root.

monad test reads each driver's failure count from a result file the driver itself writes, not from its exit code, so a file's test count is no longer capped at 255. Every file in the corpus runs self-hosted; CI's sweep carries no exclusion list.

monad eval is not a general interpreter. Eight natives are wired into it — i64_add, i64_sub, i64_mul, i64_eq, i64_lt, string_concat, string_eq, string_to_lowercase — and everything else, println included, stops with unknown native. It evaluates the file's main and prints Eval result <value>. Use monad run for a real program.

Where the binary lands

build resolves the output name against the target directory: the nearest [build] target-dir in a .monad/config.toml above the source, else plain target/. MONAD_TARGET_DIR overrides that, and --target-dir overrides both. The setting lives in the tool's config rather than in a mote's mote.toml: where output goes is not a property of the thing being built, and a script-mode file in no mote at all still needs an answer. This repository holds two toolchains, so it names their output apart: cargo's is target-rust/ and monad's is target-monad/ — they must not eat each other, because a cargo clean must not delete a monad binary.

Debug info is on by default, so a plain build is a debug build:

monad build hello.mo -o hello            # -> target-monad/debug/hello
monad build hello.mo -o hello --release  # -> target-monad/release/hello
monad build hello.mo -o "$PWD/hello"     # -> ./hello

An absolute output name replaces the directory outright; a relative one — including one with slashes in it — is placed inside it, because -o is a NAME, not a path. A relative name that looks like a path is nested rather than rejected:

monad build hello.mo -o sub/hello        # -> target-monad/debug/sub/hello

This surprises everyone once. When you want the binary somewhere specific, say so with an absolute path.

monad run is the exception: it compiles to /tmp/monad_out_<pid>, the pid being there so parallel invocations cannot collide.

The build cache

Artifacts are input-addressed. build hashes the source file's own bytes, its mote's whole declared closure, the compiler binary itself, the profile and the target triple, and if the store already holds a binary under that hash it copies it out instead of compiling — so rebuilding an unchanged tree is a file copy, not a build, and cached: <dest> (<hash>) is what a hit prints.

The file's bytes are in the key because the closure alone does not name the file. A .mo with no mote.toml above it roots at the directory it sits in, so one.mo and two.mo side by side share a root and a closure digest — keyed on that alone they shared an entry, and building two.mo after one.mo printed cached: and handed back one's binary. The directory is still hashed as well, since a file's siblings are reachable from it and its #![mote {…}] dependency list is a property of the file, not of the tree above it.

The key is the whole name: nothing you type with -o is part of it. Keeping that true took a fix upstream of the cache. The intermediate .ll used to be named after -o, and llc records its input file's name in the object it emits, so two builds of one unchanged source under two output names differed by a byte. The IR is now named by the cache key and kept in the store (<target-dir>/store/<hash>.ll), which makes the artifact a function of the key alone; the .ll your -o implies is still written beside the binary as a convenience copy, for anyone reading the IR by hand. A cache hit writes it too — from the copy in the store, and only when the bytes there differ — so a build leaves the same two files behind whether or not it had to compile.

check caches the same way, one entry per file, under <target-dir>/check/<hash>: a corpus check that takes minutes cold takes about a second warm, and a hit replays the recorded output byte for byte.

Two properties are worth knowing before you trust it. The key covers the compiler as well, so editing the compiler invalidates everything it built — and where an input cannot be determined the cache turns itself off rather than answering from a weaker key, because a stale binary is worse than a slow build. And the key is coarse by direction, not by accident: it covers the file's entire declared closure, so a one-line edit can re-check more files than it changed. Anything that needs the real work to happen — a gate that inspects the emitted IR, say — says so with one of two switches, which mean the same thing: nothing is read, and nothing is written.

monad build hello.mo --no-cache
MONAD_NO_CACHE=1 monad check init std

--verbose on check turns the cache off too: its trace is a record of what the checker did, and a replayed entry has no trace to show.

Debug info and --release

DWARF debug info is emitted by default, with a distinct source location per term. --release turns it off; an explicit --debug/-g turns it back on and wins over --release in either order.

The cost of debug info is real: every module is re-parsed with source positions before codegen. Pass --release for a build you are not going to debug — the nightly and the CI bootstrap both do.

--verbose

--verbose/-v is accepted by every command that does work. It prints each module as it loads (before loading it, so a hang names the culprit), one line per pipeline stage, and the elapsed time for each:

  loading module: lang.parser
-> stage: load + elaborate modules
   load + elaborate modules 1843ms
-> stage: typecheck target

Success and failure lines print with or without it. Colour comes from std.ansi, which honours NO_COLOR (always off), then FORCE_COLOR (on), then TERM=dumb (off). There is no tty check, so piped output is coloured unless you set NO_COLOR=1.

monad version

Prints the git commit the binary was built from. The hash is baked in at link time by the compiler that built it, read from the working directory it was invoked in — build outside a git checkout and you get unknown.

main and Exit Codes

main may return IO Unit, or I64 — in which case it becomes the process exit code:

def main : I64 := 42

monad build main.mo -o "$PWD/main" && ./main; echo $?   # 42

It may also take the command line, which the C runtime builds from argc/argv:

def main (args : List String) : I64 := 0

What the Pipeline Does

1. Parse and type-check the source — the same front end as check
2. Lower to the codegen IR and emit LLVM IR
3. Run llc to produce an object file
4. Link with clang, against the C runtime and -lgc

Bootstrapping

Once you have a monad binary, it can build its own successor:

monad build cli/src/main.mo -o "$PWD/monad-next" --release
./monad-next check cli/src/main.mo

CI runs exactly this on every push, and the second step is the one with teeth: compile succeeding only says llc and clang were happy with the emitted IR. Making the result type-check the compiler's own source — the largest input in the tree — exercises the whole front end.

The bootstrap has reached a fixpoint: the compiler compiles itself, that binary compiles itself again, and the output is identical.

Memory

Compiled binaries use the Boehm conservative garbage collector, and this is explicitly a stopgap.

Every heap object carries a header with a refcount, and monad_retain / monad_release exist — but codegen never emits calls to them, so before the GC was added nothing was ever freed. Measured on check cli/src/main.mo, that meant 5.99 GiB allocated of which 98.24% was garbage, and compiling cli/src/main.mo was OOM-killed at 29.7 GB.

So monad_alloc calls GC_malloc, string buffers go through GC_malloc_atomic (so the collector does not scan text bytes and mistake them for pointers), and monad_release deliberately does not free — that would corrupt the Boehm heap. The refcount field is currently vestigial.

The intended replacement is for the compiler to track ownership through the linear and affine multiplicities the language is designed around, at which point the allocator gets real frees and the GC dependency goes away. That is blocked on multiplicity checking existing at all.

Fail-Fast Gates

Before emitting anything, the backend runs four validation passes over the reachable declarations. Each exists because the silent miscompile it catches actually shipped once:

All four run only on reachable declarations, so a problem in dead code cannot block a build that never touches it.

The undefined symbols gate is a backstop, and one case used to reach it that should never have: a class-method call naming a method its class does not declare (Map.get — class Map declares empty/insert/lookup/delete). The resolver rewrites a class-method reference to a mangled name built from the class's declared method list, so such a call produced a name nothing emits and landed here as call to undefined symbol(s): std.map::Map_BTreeMap_get — a symbol and no call site. The gate's own reasoning assumes a successful resolution implies the definition exists; class_method_ref (lang/src/scope.mo) now requires the qualifier's class to declare the method, so that assumption holds and the call is rejected during typecheck instead, naming the reference exactly as written (unknown variable 'Map.get').

Native Coverage

There are 146 natives declared across init/ and std/. The backend wires I64 arithmetic and comparison, string operations, print_str, the file and directory natives, get_env, current_time, process_id, exec_cmd, and the eight tcp_* socket natives.

Not wired: the entire concurrency surface — see Concurrency. A program that reaches one of those fails to compile with a clear message rather than producing a broken binary.

The tcp_* natives are wired here and nowhere else. The Rust bootstrap host has no TCP implementation, so a socket test cannot run under cargo run -- test; motes/moon and motes/moose are exercised by the self-hosted runner.

Three natives are declared but unimplemented in both implementations — eq_rec, string_to_chars, string_from_chars — and fail at run time with unknown native.

A few natives are not written in C at all: lang/codegen/runtime.mo emits LLVM IR directly for thirteen simple operations.

Known Rough Edges

• Compiling a large program is slow — a full self-compile takes minutes.
• Deep recursion in compiled code can exhaust the stack; raise it with ulimit -s when compiling large inputs.
• monad eval reaches only eight natives (above), so it is not a substitute for monad run.
• monad test compiles one driver binary per test file and runs it; a file whose tests reach a native the backend does not wire (the concurrency ones especially) is skipped with that reason rather than run.
• A relative -o lands in /tmp/monad_out_<pid> (above).
• A struct literal the checker cannot give a type to — most often one written directly under return — is rejected with "cannot infer struct type". Annotate it ({ … : Point }) or bind it to an annotated local first.

See the Maturity Matrix.

The Standard Library

The standard library is split into two directories, and the split is a rule, not a convention:

• init/ — pure, portable core. Code that must work in any environment, including wasm and embedded targets. No OS-specific natives.
• std/ — OS-specific implementations and genuine side effects.

IO the type lives in init/; IO.println lives in std/, because printing touches the operating system.

Roughly 440 public definitions, 35 classes, and 132 instances across the two, not counting their test modules.

What Is Available Without Importing

Twelve modules load ambiently: the prelude, id, io, number, math, string, list, the init hub, std.path, std.io, std.process, and the std hub.

Everything else needs an explicit import, and the re-export hubs do not help: init/lib.mo re-exports only id, io, number, math, string, list, and std/lib.mo only std.path, std.io, std.process. So init.foldable, init.optics, init.meta, and all of std beyond those three — std.array included — are opt-in.

init/ — pure and portable

prelude — ambient, not importable

The core types (Bool, List, Option, Result, Pair, Nat, String, Char, Unit, Void, Any, Vec, Eq, True, the numeric primitives) and the core classes (Functor, Applicative, Monad, MonadState, MonadLift, MonadLiftT, IndexedMonad, IndexedMonadState, IndexedMonadLift, FromListLiteral, HAdd, Add, Sub, HMul, Div, Append, BEq, BOrd, ToString, Hashable).

MonadState and IndexedMonadState take the monad as their only parameter — the state type is an implicit forall — so that instance resolution can key on a concrete monad head. examples/state_monad.mo and examples/indexed_monads.mo show both in use.

Functions: Bool.not/and/or, List.is_empty/append/first/last/flatten/tail/map, Option.get_or_default, Nat.add/sub/mul/eq, fun_apply/apply_fun.

init (init/lib.mo) — the hub

Re-exports the modules below, defines the From class, BEq (Option A), and rebinds infix (+) := I64.add.

init.number / init.math

The numeric workhorse — about 600 lines of instances. For each of I8, I16, I32, I64, U8, U16, U32, U64, F32, F64: add, sub, mul, div, beq, lt, gt, to_string natives plus Add, Sub, HMul, Div, BEq, BOrd, and ToString instances. Also Hashable I64/U64, U32 bitwise operations (and, or, xor, shl, shr), and width conversions.

init.string

String.beq, concat, concat_all, concat_list, length, is_empty, slice, drop, get, get_char, to_lowercase, starts_with, ends_with, contains, repeat, reverse, trim, find_last, to_list/from_list, to_chars/from_chars (declared but not implemented — these fail at run time with unknown native), hash, plus List.reverse and List.singleton. Instances: BEq, BOrd, ToString, Add, Append, Hashable.

init.list

List.get. Most list operations are in the prelude or std.list.

init.id

The identity monad: Id A, Id.run, and Functor/Applicative/Monad instances. Useful as the trivial case when writing code generic over a monad.

init.foldable — not ambient

Semigroup (combine), Monoid (mempty), Foldable (foldr, foldl), Traversable (traverse). Instances for List, Option, and String.

init.optics — not ambient

Van Laarhoven-style optics: the Lens and Prism types, with lens, view, set, over, preview, review, over_prism, set_prism. #[derive Lens] generates one lens per struct field.

init.meta — not ambient

The reflection-as-data types (TypeInfo, CtorInfo, FieldInfo, Expr, MatchArm, Param, Decl) that the macro system passes to derive backends. See Macros and Derive.

io

type IO A, def IO.pure, and instance Monad IO. Nothing else — deliberately. Construct with IO.pure, unwrap with Monad.bind; the io constructor itself is not for call sites and is meant to become an implementation detail.

std/ — OS-specific

std.io — ambient

IO.println and the filesystem: read_file, write_file, file_exists, is_dir, list_dir (all Path-typed), plus IO.get_env and IO.current_time (monotonic milliseconds — only differences are meaningful).

It also holds the entire TCP surface: the opaque Socket and Listener types and eight blocking natives — tcp_connect, tcp_listen, tcp_accept, tcp_read, tcp_write, tcp_close, tcp_close_listener, tcp_local_port. These are implemented only by the self-hosted backend; the Rust bootstrap host has no TCP at all, so a socket test cannot run under cargo run -- test. The IO Monad has the signatures, the two worked snippets, and the caveats.

std.path — ambient

A validated Path newtype: Path.of (the validating constructor), to_string, is_absolute, join, with_suffix, beq, and BEq Path.

std.process — ambient

exec_cmd and process_id.

std.list — not ambient

List.length, filter, any, all, sum, find_by, filter_map, contains_by, intercalate, dedup_by; instances BEq (List A) and Append (List A).

std.map — not ambient

A real persistent-map implementation, not a stub:

• BTreeMap K V — AVL-balanced, with insert, lookup, delete, fold, to_list, and instance [BOrd K] Map BTreeMap
• HashMap K V — 256 buckets, with instance [Hashable K, BOrd K] Map HashMap
• class Map (M := HashMap) — empty, insert, lookup, delete

std.base — not ambient

The Ordering type and the value classes: Ord (three-way compare), Semigroup, Monoid, Default, Enum, Bounded, with instances for Ordering, String, Bool, and every numeric width.

Note that Semigroup and Monoid are declared twice — here and in init.foldable — with different method names. They are unrelated classes that share a name. Import one or the other, not both.

std.show and std.debug — not ambient

class Show A { def show : A -> String } and class Debug A { def debug : A -> String }. Debug is a Rust-style diagnostic representation and quotes strings; Show is a display string. The prelude's ToString is what the numeric types implement.

std.derive — not ambient

derive_beq_meta, derive_bord_meta, derive_debug_meta, derive_lens_meta and the defmacros that wrap them. Must be imported for #[derive ...] to resolve — see Macros and Derive.

std.test — not ambient

Test.assert (condition : Bool) : Bool := condition. That is the entire assertion library — an identity function. There is no assert_eq, no failure message, no matcher DSL. In practice most tests just return a Bool expression directly, which is why Test.assert has only a handful of callers across 1600 tests.

std.bench — not ambient

Bench.now, Bench.since, Bench.report, Bench.report_since — all IO, over the monotonic clock. Micro-benchmarks live in bench/ and are deliberately excluded from the ordinary test sweep.

std.array — not ambient

Array A, a native-backed sequence with O(1) length and get, alongside a mutable ArrayBuilder A for filling one under IO.

Array.set_in_place is O(1) in a compiled binary and O(n) under the bootstrap host's interpreter, which copies on write. Both are correct; only the cost differs, so a hot fill loop belongs in compiled code. Array.freeze deliberately copies, so writing to the builder afterwards cannot disturb the frozen array.

Array implements no classes at all — Array.map and Array.foldl are ordinary functions, not Functor/Foldable methods.

std.ansi — not ambient

Terminal colours: the Color, Style, and Modifier types, with red, green, yellow, bold, dim, Ansi.fail, Ansi.pass, warn, colored, the escape/color_fg_code/color_bg_code/style_code builders, and an environment-aware colors_enabled (NO_COLOR wins, then FORCE_COLOR, then TERM=dumb).

Ansi.fail and Ansi.pass were once bare fail and pass. The dotted names are load-bearing: a bare fail here captured ParseResult.fail elsewhere in the tree during module qualification and produced a segfault.

std.sha256 — not ambient

A complete SHA-256 implementation in pure Monad, with no natives, built on the U32 bitwise operations. A good demonstration that the numeric tower is real.

std.concurrent.fiber / std.concurrent.combine — not ambient

Fibers and structured-concurrency combinators. Read Concurrency before using them — compiled binaries run fibers on real OS threads, while the bootstrap host's interpreter is lazy and cooperative, so the two backends disagree about what a forkIO means.

Gaps Worth Knowing About

• Assertions. Test.assert is an identity function; there is no equality assertion or failure message.
• No Iterator class. Iteration is Foldable or direct recursion.
• No stdin. IO can print and touch files, but cannot read a line.
• Traversable has no instances at all — the class is declared and nothing implements it.
• Duplicate Show. std.list declares a local class Show A alongside its import of std.show's. Prefer std.show.
• Three declared-but-unimplemented natives: eq_rec (so Eq.rec cannot be called), string_to_chars, and string_from_chars.
• TCP has no timeout and no non-blocking mode: tcp_connect, tcp_accept and tcp_read block until they complete, so a peer that connects and then stays silent holds a fiber and its OS thread indefinitely. And TCP is self-hosted only — the Rust host cannot run a socket at all.

See the Maturity Matrix for the summary view.

Reference

A quick reference for Monad syntax and built-in features. Anything marked not implemented parses in some form but does not work — see the Maturity Matrix.

Keywords

def, defmacro, let, in, use, open, class, struct, instance, type,
fn, ꟛ, match, if, then, else, infix, return, for, do, quote, with,
pub, priv

Reserved names: Type, Prop, Pred, Sort.

for is reserved but has no grammar rule — there is no loop syntax.

Comments

// Single line comment

/* Multi-line
   comment */

def answer : I64 := 42

Docstrings

/// Documentation for the following declaration
def greet (name : String) : String := "Hello, " ++ name

Docstrings are stored on declarations and retained through module loading, so the bootstrap host's LSP server can surface them.

Definitions

Every def requires a type annotation. There is no top-level inference.

open IO {println}

// Basic function
def add (a : I64) (b : I64) : I64 := a + b

// Shared annotation for same-typed parameters
def mul (a b : I64) : I64 := a * b

// Implicit parameters
def identity {A : Type} (x : A) : A := x

// Class constraints
def twice [Add A] (x : A) : A := Add.add x x

// Field destructuring in a parameter
struct Coord { fst : I64, snd : I64 }
def sum_coord ({fst, snd} : Coord) : I64 := fst + snd

// Do-block body (alternative to `:=`)
def steps : IO Unit {
    println "one";
    println "two"
}

A parameter list can also be written as one brace block, which is the only spelling that allows defaults:

def scale {factor : I64 := 2, p : I64} : I64 := factor * p

The block is all-or-nothing: no further (…) groups may follow it, and it takes no multiplicity prefixes. A one-parameter block needs the := default or a trailing comma — def f {x : I64} : I64 := x is read as an implicit type binder clause instead.

The default is applied by both compilers: omitting a parameter that declares one is accepted, and the declared default stands in for it, so def scale {factor : I64 := 2, p : I64} makes scale { p := 4 } equal 8. See The Bootstrap Host for what is still host-only.

Visibility

pub def exported : I64 := 1
priv def internal : I64 := 2
def package_private : I64 := 3

Package-private is the default. pub use module {*} re-exports an import.

Lambda Expressions

Three equivalent spellings:

def a : I64 -> I64 := fn x => x + 1
def b : I64 -> I64 := \ x => x + 1
def c : I64 -> I64 := ꟛ x => x + 1

A lambda gets its parameter type from the definition's signature, or from an explicit parenthesised annotation:

def d : I64 -> I64 := fn (x : I64) => x + 1

Backtick Operators — not implemented

x `f` y   // intended: f x y

The parser recognises the backtick form, but the expression parser only reduces symbolic operators, so this never becomes an application. Write f x y.

Let Expressions

One let binds one name; chain them for several:

def one : I64 := let x := 10 in x + 1

def two : I64 :=
    let x := 10 in
    let y := 20 in
    x + y

def three : I64 := let x : I64 := 10 in x + 1

Several bindings may share one let, separated by ;. Each may carry its own annotation, and each sees the bindings before it:

def multi : I64 := let x := 10; y : I64 := 20 in x + y

The ; is required here; the bootstrap host also accepts it omitted. The form desugars to nested lambdas, so the bindings are sequential and non-recursive.

Literals

Numeric

def a : I64 := 42        // I64 (default)
def b : I8 := 42i8
def c : I16 := 42i16
def d : I32 := 42i32
def e : U8 := 42u8
def f : U32 := 42u32
def g : U64 := 42u64
def h : F64 := 3.14      // F64 (default)
def i : F32 := 3.14f32
def j : I64 := 0xFF      // hex
def k : U32 := 0xFFu32   // hex with suffix

There are no binary or octal literals, and no _ digit separators.

Strings and characters

def s : String := "hello\n"
def raw : String := r"C:\Users\monad\main.mo"
def raw_hash : String := r#"{"name": "monad"}"#
def raw_hash3 : String := r###"a "## b"###

def c : Char := 'M'
def nl : Char := '\n'
def lam : Char := 'λ'

A char literal holds exactly one Unicode codepoint and takes the same escapes as a string (\n \r \t \b \f \\ \/ \" \'). \u{XXXX} is not accepted self-hosted — write the character itself; the bootstrap host does accept it.

Char has no operations of any kind — no equality, no ToString, no Char.* functions — so a Char can be written, typed and passed, but not inspected.

Raw strings take their body verbatim — no \ escape processing. The closing delimiter is " followed by the same number of # as the opener, so escalating the hash count lets any content be embedded.

Escapes in ordinary strings: \n \r \t \b \f \\ \/ \" \' \u{XXXX}, plus backslash-newline line continuation. There are no octal escapes.

Lists and tuples

def xs : List I64 := [1, 2, 3]
def pair : Pair I64 String := (1, "two")

List literals desugar through FromListLiteral; tuples desugar to right-nested Pair.pair.

Type Annotations

Any term can be annotated:

def x : I64 := (42 : I64)
def y : I64 := (42 : _)

Field Access

struct Inner { v : I64 }
struct Outer { inner : Inner }

def get (o : Outer) : I64 := o.inner.v

Dot notation on a value is field access only. There is no UFCS method dispatch: s.length does not mean String.length s, and naming something that is not a declared field is an error. Use the qualified name.

Match Expressions

type Shape {
    circle (radius : I64),
    rectangle (width : I64) (height : I64)
}

def area (s : Shape) : I64 :=
    match s {
        circle r => r * r,
        rectangle w h => w * h
    }

Patterns are one constructor deep. _ is a wildcard. Not supported: nested constructor patterns, literal patterns, guards, or-patterns, and exhaustiveness checking.

Struct values also match on field names:

struct Point3 { x : I64, y : I64, z : I64 }

def xy (p : Point3) : I64 :=
    match p {
        {x, y, ..} => x + y
    }

If Expressions

def sign (n : I64) : I64 := if n < 0 then 0 - 1 else 1

Do Notation

open IO {println}

def a : IO Unit := do {
    println "one";
    println "two"
}

def b : IO Unit {
    println "one";
    println "two"
}

Separate statements with ;.

Struct Values

struct Point { x : I64, y : I64, z : I64 := 0 }

def p : Point := { x := 3, y := 4 }
def q : Point := { p with x := 10 }

Struct literals are not inferrable on their own — they need a type from context.

Attributes

Attributes are written #[name arg1 arg2] — space-separated arguments, no parentheses or commas:

#[native print_str]         // implemented in Rust; no body follows
#[test]                     // a test, run by `monad test`
#[terminating]              // assert well-foundedness; skip the termination check
#[partial]                  // this definition may not terminate
#[derive BEq BOrd Debug]    // generate instances via macros
#[derive_cli]               // generate an argv parser
#[cfg ...]                  // conditional compilation

Attributes come before visibility: #[test] pub def ..., not pub #[test] def ....

Native Functions

#[native print_str]
def IO.println (s : String) : IO Unit

#[native "num_add"]
def I64.add (a b : I64) : I64

A native has no body. The attribute's argument is the runtime's identifier, which need not match the Monad-side name.

Infix Operators

infix (operator) := functionName

Built-in Operators

Operators marked — have a precedence but no binding in the prelude, so using them is an error until you bind one yourself. !=, <=, and >= are commented out in init/prelude.mo pending default-method support on BEq/BOrd.

@ is deliberately left free for libraries to claim.

Note that init/lib.mo rebinds infix (+) := I64.add, shadowing the prelude's class-based HAdd.add where init is in scope.

Type Definitions

type Colour {
    red,
    green,
    blue
}

type Shape {
    circle (radius : I64),
    rectangle (width : I64) (height : I64)
}

type Tree A {
    leaf,
    node (left : Tree A) (value : A) (right : Tree A)
}

type Empty {}

A type can be placed in a universe explicitly, which is how propositions are declared:

type Truthy : Prop {
    yes
}

Struct Definitions

struct Point {
    x : I64,
    y : I64,
    z : I64 := 0,     // default value
    !name : String,   // linear field (`!`) or affine (`?`)
    ?tag : String
}

Multiplicity annotations are not enforced — see Linear Types.

Class Definitions

class Container (F : Type -> Type) {
    def wrap : A -> F A
    def size (fa : F A) : I64
}

class [Container F] Sized (F : Type -> Type) {
    def is_empty (fa : F A) : Bool
}

class Convert A B {
    def convert : A -> B
}

A class parameter may have a default (class FromListLiteral (L : Type -> Type := List)). Methods may have default bodies, but an instance still has to list every method it wants — empty instance bodies do not parse.

Instance Definitions

type Colour { red, green, blue }

instance ToString Colour {
    def to_string (c : Colour) : String :=
        match c {
            red => "red",
            green => "green",
            blue => "blue"
        }
}

instance {A : Type} Append (List A) {
    def append (a b : List A) : List A := List.append a b
}

Instances may be named — one bare identifier self-hosted, a dotted path on the bootstrap host:

type Colour2 { red2, green2 }

instance ColourEq : BEq Colour2 {
    def beq (a b : Colour2) : Bool := true
}

The name is recorded and nothing reads it: no syntax selects an instance by name in either implementation.

Multiplicities

Struct fields accept ! (linear), ? (affine) and % (erased) in both implementations:

struct Res { !handle : String, ?tag : String, size : I64 }

Parameters accept them too — on definitions and on typed lambda parameters:

def f (!linear : I64) (?affine : I64) (%erased : I64) (many : I64) : I64 :=
    linear + affine + erased + many

def g : I64 -> I64 := fn (!x : I64) => x

The prefix applies to the whole group, so (!x y : I64) makes both names linear. A destructured parameter takes one as well — (!{fst, snd} : Coord) — though that spelling is self-hosted only; the bootstrap host rejects it.

Nothing enforces multiplicities in either implementation. Lowering drops the annotation and every binder becomes Many — see Linear Types.

Modules

use std::process {exec_cmd, process_id}   // import, naming what you need
use std::list {*}             // import everything
use std::map {}               // load for qualified access and instances only
open IO {println}    // drop the prefix for these names

The first segment must name a mote or lib; a bare use io is an error. Every name inside the braces must be a top-level declaration of the target module, matched by its spelled name — a brace item is a name path (IO.println), not a module path, so a dotted def is imported as use std::list {List.intercalate} and the bare tail use std::list {length} is an error. {*} and {} are unaffected. See Modules and Imports.

Dot Macro

x.y.z is resolved at compile time. If x is a module path it becomes a single qualified name (List.append); if x is a local value it becomes struct field access. The disambiguation happens during lowering.

Macros

defmacro, quote { ... }, macro calls (name! args), and compile-time reflection are real and are how #[derive] is implemented. See Macros and Derive.

Constraint Solver

Recursive instance constraints (e.g. instance [Show A] Show (List A) { ... }) are handled by a constraint solver that uses a visiting set to detect cyclic constraint dependencies. Resolution happens at evaluation time, so an unsatisfiable constraint surfaces as a run-time unresolved global: error rather than a check failure.

Standard Library

The prelude types and classes are listed in Types and Type Classes. For the module map and each module's contents, see The Standard Library.

For scale: the standard library is about 440 public definitions, 35 classes, and 132 instances across init/ and std/, excluding their test modules.

CLI

monad build file.mo -o "$PWD/out"  # compile to a native binary
monad run file.mo                    # compile and execute
monad eval file.mo                   # interpret (pure programs only)
monad check file.mo                  # type-check, no execution
monad check init std lang            # directories are expanded recursively
monad test file.mo                   # compile and run this file's #[test] defs
monad test                           # the mote containing the working directory
monad test --workspace               # every mote in the enclosing workspace
monad pretty file.mo                 # parse and pretty-print
monad version                        # the git commit this binary was built from

compile and run take --verbose/-v, --debug/-g and --release; eval, check and test take --verbose/-v. Debug info is on unless you pass --release. Flags may go before or after the paths, --output=NAME is not recognised (use a space), and a relative output name lands in /tmp/monad_out_<pid>. See Compiling and Running, and The Bootstrap Host for the Rust implementation's additional commands.

Appendix: The Bootstrap Host

This book documents the self-hosted Monad compiler — lang/, written in Monad, which compiles itself. That is the language.

There is a second implementation: monad-rs, a compiler and interpreter written in Rust. It exists to bootstrap the first one, and it is still what runs the self-hosted compiler's source before you have a binary. It is a host, not the language.

This appendix exists because the two are not yet identical, and because the host currently provides some things the self-hosted compiler does not have at all — including every piece of editor tooling. Nothing in here is a language feature.

Getting it

cargo build --release        # produces target-rust/release/monad-rs
cargo install --path cli     # or install it

The binary is monad-rs; the crate is monad-cli.

What the host has that the self-hosted compiler does not

An interpreter that runs real programs

monad-rs run file.mo
monad-rs run file.mo -- arg1 arg2     # everything after -- reaches `main`

The self-hosted compiler has run (compile, then execute) and eval, but eval's interpreter reaches only eight pure natives — no println, no files. The host's interpreter runs the whole language, and skips llc and clang, so it is still the faster way to iterate on an effectful program.

A test runner with machine-readable output and parallelism

monad-rs test init std
monad-rs test lang --json -j 8 --timeout 30

The self-hosted monad test now runs the whole corpus, including the concurrency tests — CI's sweep uses it and carries no exclusions — but it runs files one at a time and has no --json, -j, or --timeout. For parallelism, machine-readable output, or a per-test timeout, use the host.

Editor and agent tooling

The repository also ships a Claude Code plugin in .claude-plugin/ that wires up the MCP server.

Packages (motes)

A mote is a package: a directory with a mote.toml and a src/.

[mote]
name = "example"
version = "0.1.0"
edition = "2026"

[dependencies]
local = { path = "../other-mote" }

monad-rs test examples/test_mote.mo -p motes/example/src
monad-rs check --workspace

Local path dependencies resolve fully, with transitive walking, workspaces ([workspace] members = ["motes/*"]), a mote.lock format, and version-conflict detection. Registry and git dependencies parse and are then rejected:

dependency from-registry 1.0: registry deps not yet supported

There are no build/add/publish commands. The self-hosted compiler reads manifests too — check and test share one mode dispatch (explicit paths, --workspace, or the mote you are standing in; compile takes an explicit path, and a bare one prints its usage) and all three resolve a module path from the mote doing the use, falling back to the directory conventions for script modules. See How Modules Are Found. What remains host-only is everything beyond a manifest's declared paths: transitive walking, the mote.lock format, version-conflict detection, and the registry.

Module resolution knobs

--mote-path DIR (repeatable), --manifest-path PATH and MONAD_STDLIB all belong to the host, and resolution there is relative to the working directory. --workspace/-w is on both, which is what makes monad check --workspace mean the same thing either way.

Behaviour the two compilers read differently

This section used to be a syntax table, and it is empty now. Everything that was in it has been implemented self-hosted: char literals, named instances, _ holes, multi-binding let, brace-parameter declarations, multiplicity prefixes on parameters, #[derive …], \u{XXXX} escapes and dotted instance names.

"Empty" means the entries that table held, not every construct either grammar can spell, and one family sits outside it. A lambda's parameter list: fn (x) => x, fn (x := 5) => x and fn ({x, y} : P) => x all parse under the host — its parameter annotation is optional, and a destructured group is accepted — and are a hard parse failure self-hosted, because the dispatch after fn sends every ( to the typed-parameter path, which requires a :. The reverse holds in the same place: the host requires whitespace after fn, so fn(x : I64) => x parses only self-hosted. No file in the corpus writes a bare fn (x), so this is latent rather than live, and it predates the rewrite above; it is named here because "no construct left" was read as covering it.

One behavioural difference remains — code both compilers accept, which they then read differently. It is not a syntax gap. A second one, the un-inferable _, closed on this branch and is recorded below rather than deleted.

A missing ; between let bindings. Both parse it. Self-hosted, the binding's value expression is atom (atom)*, so it swallows the next statement as an argument whenever that statement's head is an expression atom:

def f : I64 := do {
  let a : I64 := 1
  I64.add a 2       // absorbed: the value became `1 I64.add a 2`
}                   // error: unknown variable 'a' in f

The binder then never scopes where you meant it to. The host's grammar requires a path head for an application, so it cannot swallow and reads the statement correctly. The missing ; is harmless when the next statement begins with a keyword rather than an expression (let b : I64 := 2 follows fine), which is what makes this one easy to write by accident: write the ;. This is the same grammar difference as the atom-in-function-position entry below, seen from the other side.

A _ whose type cannot be inferred — closed. def h : I64 := _ is accepted by both, and by both it lowers to a value that is not what you wanted (I64.beq h 0 fails under each): write the value. The un-inferable shape used to be the divergence — the host rejects a hole no expected type reaches (def k : I64 := (fn x => x) _ is "cannot infer the type of a hole") while self-hosted accepted it silently — and it is not one any more. The reason it could not be closed by a predicate over the hole is worth keeping: the self-hosted parser wrote the sort Type onto every unannotated lambda parameter where the reference writes a hole, so a callee's own term shape (fn x => x, as opposed to an application) could not be read at all, and the argument side was checking against Type besides. Both halves were fixed together, and the port now rejects exactly the two rows of the probe matrix the host rejects ((fn x => x) _ and (fn (x : _) => x) _) and accepts the other twelve.

Syntax the self-hosted compiler accepts and the host rejects

Five, in this direction.

Term macros:

defmacro double x := x + x
def y : I64 := double! 9

The host fails with "macro double did not return a Term value". Declaration macros (defmacro name T := decls { … }) work on the host — it is specifically the term form that diverges. See Macros and Derive.

A multiplicity prefix on a destructured parameter:

def sum_coord (!{fst, snd} : Coord) : I64 := fst + snd

The host's destructured-parameter parser never reads a prefix, so this is a parse error there. See Linear Types.

An atom in function position — an application whose head is a literal rather than a path:

def g : I64 := 1 5

Self-hosted this parses ("s" 5 and (1) 5 do too; nothing checks the head is callable). The host rejects it: a bare literal head is a parse error, and a parenthesised one gets as far as "expected a function type, found I64". No real program wants this, so the portable alternative is simply not to write it — but it is worth knowing, because it is the grammar fact behind the missing-; mis-scope described above: the same atom (atom)* shape is what lets a let value swallow the statement after it.

A field access whose subject is a top-level def, rather than a local binding:

struct Vec3 { x : I64, y : I64 }
def vzero : Vec3 := { x := 40, y := 2 }
def vzero_x : I64 := vzero.x

Both parsers settle "module-qualified name, or field access?" on one question — is the path's first segment a local binder? — because neither has a scope to ask. A local subject (p.x) is therefore already a field-pattern match by the time either checker sees it. A top-level one is not, and the self-hosted checker rebuilds it there (try_global_field_access), so this works and compiles. The host's checker never rewrites terms, so it rejects the read with "unbound variable vzero.x" — meaning a read whose subject is a top-level def cannot appear in a file the host checks, which includes this book's monad blocks and the corpus the pre-commit hook sweeps. Read through a parameter or a let when you want both compilers to accept it. See Structs and Enums.

And a codegen behaviour rather than syntax: the self-hosted backend runs a pre-elaboration pass that desugars annotated struct literals, and aborts loudly if one ever reaches codegen undesugared. The host resolves struct literals in its own checker and has no equivalent.

Why this matters for what you write

If you are writing Monad, target the self-hosted compiler: everything in the main chapters works there. Use the host for its tooling — editor diagnostics, a REPL, and running test suites.

If you are working on the compiler itself, you need both. The host is the stricter one, and not only about holes. Measured at the end of the test-gap branch, the self-hosted checker accepts a concrete type mismatch in nine of the ten positions probed — def body, application body, return, if/else branches, lambda argument, named-def-call argument, constructor argument, struct-literal field, class-method return — and enforces only the match-arm result, which it enforces correctly. unify itself is sound; the comparison is simply never invoked at those boundaries, so a clean self-hosted check is not evidence of type soundness. (def f : I64 := "s" is the shortest way to see it: accepted self-hosted, one error under the host.) The self-hosted grammar is separately the more permissive one at the edges, in the four places listed above. Both directions are larger than the hole case this paragraph used to name, and the type-checking one is much the largest.

This appendix is the current record. The two plans it used to point at are historical: bootstrapping/self-hosted-parity-gaps.md was a 2026-09-07 inventory of constructs the host accepted and the self-hosted compiler did not, and eleven of its twelve sections have closed since — the twelfth is the term macro above, which is a host-side bug; bootstrapping/self-hosted-test-runner-multi-test.md tracked files the self-hosted test runner skipped, and the sweep now carries no exclusions at all. The checker gaps that remain are tracked in bootstrapping/self-hosted-compiler-review-2.md.