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.

use io {}
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 #

use io {}
open IO {println}

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

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

Statement	Syntax	Desugars to
Bind	let x <- action	Monad.bind action (fn x => ...)
Let	let x := value	let x := value in ...
Return	return value	Monad.pure value
Expression	expr	Monad.bind expr (fn _ => ...)

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 #

Operator	Precedence	Associativity	Bound to
|>	5	Left	apply_fun
<|	5	Right	fun_apply
>>=	10	Right	Monad.bind
.	12	Right	path / field access (not bindable)
<*>	15	Left	—
<|>	20	Left	—
||	25	Right	Bool.or
&&	30	Right	Bool.and
==	40	Left	BEq.beq
<	40	Left	BOrd.lt
>	40	Left	BOrd.gt
!=, =, <=, >=	40	Left	—
++	50	Right	Append.append
@	50	Right	—
>>, <<	60	Left	—
+	65	Left	HAdd.add
-	65	Left	Sub.sub
*	70	Left	HMul.mul
/	70	Left	Div.div

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 io {IO}          // import, naming what you need
use io {*}           // import everything
use io {}            // load for qualified access and instances only
open IO {println}    // drop the prefix for these names

A bare use io with no braces parses but is deprecated. 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 compile 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.