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.