Introduction

The Monad language is a dependently typed programming language with compatibility with Rust.

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

Hello World

Here is a simple example:

use io
open IO

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

Save this as hello.mo and run it with:

cargo run -- run hello.mo

Key Features

• Dependent types: Types can depend on values
• Type classes: Ad-hoc polymorphism with constraints
• Linear types: Resource-safe programming with compile-time enforcement
• Pattern matching: Destructure data with match
• Native functions: Call Rust code from Monad
• IO monad: Safe side effects

Quick Example

use io
use init
open IO

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

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

Getting Started

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

Prerequisites

Before getting started, ensure you have:

• A text editor with Monad syntax support (or basic text editing)
• The Monad compiler built (see README for instructions)

Your First Program

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

use io
open IO

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

Save this as hello.mo and run it with:

cargo run -- run hello.mo

You should see:

Hello, World!

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

Variables and Basic Types

Monad supports explicit type annotations. The basic types include:

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

You can also use other integer types: I32, U64, U32, U16, U8.

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

// With type annotation on the result
def greeting : String := "Hello"

Function Application

Function application is written with spaces:

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

Anonymous Functions (Lambdas)

Lambda expressions use fn, \, or ꟛ:

def square := fn n => n * n
def add_one := \ x => x + 1
def identity := ꟛ x => x

Pattern Matching

Match on values to deconstruct them:

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

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

Let Bindings

Local bindings with let:

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

You can also use semicolon-style let bindings:

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

Docstrings

Document your declarations with /// docstrings. They are retained through module loading for tooling and inspection:

/// Greet a user by name
def greet (name : String) : IO Unit := println name

/// Module-level documentation (at top of file)

Comments

// Single line comment

/* Multi-line
   comment */

Operators

Monad supports infix operators with defined precedence:

use init
use math

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

Built-in operators include: | Operator | Description | |----------|-------------| | +, - | Add / subtract | | *, / | Multiply / divide | | ++ | Append (list concat, etc.) | | &&, \|\| | Boolean and / or | | ==, != | Equality / inequality | | >>= | Monad bind | | \|> | Forward pipe (x \|> f) | | <\| | Backward pipe (f <\| x) | | <*> | Applicative apply | | <\ | > | Alt / choice | | . | Dot macro (path concatenation) | | >>, << | Shift / fork |

Summary

In this chapter, you learned:

• How to write a basic Monad program
• Variable declarations and basic types
• Function definitions and lambdas
• Pattern matching with match
• Local bindings with let
• Comments 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 Bool {
    true,
    false
}

This defines a type Bool with two constructors: true and false.

Constructors with Fields

Constructors can carry data:

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

Natural Numbers

The canonical example of inductive types is natural numbers:

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 using the FromListLiteral class:

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

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 on types, use pattern matching:

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

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

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

Recursive Functions

Functions on inductive types can be recursive:

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

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

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

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 several built-in types in the prelude:

Summary

• Types define new types through constructors
• Pattern matching destructs values
• Recursive functions operate on types
• Type parameters (A) make types polymorphic

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 Functor (F : Type -> Type) {
    def map (f : A -> B) : (F A) -> F B
}

Default Implementations

Class methods can provide default implementations using :=:

class Show A {
    def show (a : A) : String := "<generic>"
}

Instances can override defaults:

instance Show I64 {
    def show x := "int"  // overrides the default
}

instance Show Bool {
    // uses default "<generic>"
}

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
}

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

Multiple Parameters

Classes can have multiple type parameters:

class HAdd A B C {
    def add : A -> B -> C
}

Constraints on Classes

A class can add constraints that must be satisfied:

class [HAdd A A A] Add A {
    def add : A -> A -> A
}

This means Add A requires HAdd A A A to exist.

Standard Type Classes

Functor

class Functor (F : Type -> Type) {
    def map (f : A -> B) : (F A) -> F B
}

FromListLiteral

Used for list literal desugaring:

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

HAdd and Add

class HAdd A B C {
    def add : A -> B -> C
}

class [HAdd A A A] Add A {
    def add : A -> A -> A
}

Applicative

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

Monad

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

From

class From T A {
    def from (t : T) : A
}

HMul

class HMul A B C {
    def mul : A -> B -> C
}

BEq

class BEq A {
    def beq : A -> A -> Bool
}

BOrd

class BOrd A {
    def cmp : A -> A -> I64
}

Show

class Show A {
    def show (a : A) : String := "<generic>"
}

Sub

class Sub A {
    def sub : A -> A -> A
}

Div

class Div A {
    def div : A -> A -> A
}

Append

class Append A {
    def append : A -> A -> A
}

DefaultValue

class DefaultValue A {
    def default : A
}

Type Class Constraints

Functions can require type class instances using bracket syntax:

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

The [Functor F] syntax means "an instance of Functor for F must exist".

Infix Operators from Classes

You can create infix operators that reference class methods:

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

Summary

• Type classes define interfaces for types
• Constraints [C A] require instances
• Classes can depend on other classes
• Instance chaining enables polymorphic behavior

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:

instance FromListLiteral List {
    def cons (a : A) (l : List A) : List A := List.cons a l
    def empty : List A := List.empty
}

Instances with Constraints

Instances can require other instances as constraints:

instance [Add A] Add (List A) {
    def add (a b : List A) : List A :=
        List.append a b
}

Named Instances

Instances can have optional names for organization:

instance List.FromListLiteral : FromListLiteral List {
    def cons (a : A) (l : List A) : List A := List.cons a l
    def empty : List A := List.empty
}

IO Monad Instance

The IO type has a Monad instance:

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

Implicit Instance Parameters

Type class parameters can be implicit and auto-resolved:

def doubleList [Add A] (xs : List A) : List A :=
    // Uses Add.add through instance resolution
    ...

Instance Resolution

Monad uses instance resolution to find matching instances:

1. The type checker searches for instances matching the required class and type
2. Constraints on instances are recursively resolved
3. If no matching instance is found, a type error occurs

Using Instances

Once an instance is defined, its methods are available through the class:

use init
use math

def result : I64 := 3 + 4  // Uses I64.add via Add instance

Summary

• instance declares implementations for type classes
• Instances can have constraints on other instances
• Instance resolution finds matching implementations automatically
• Methods become available through class access

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

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

Forall Types (Implicit Arguments)

The {A : Type} syntax introduces implicit arguments that are inferred by the type checker:

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

// Called without specifying A:
def result := identity 42  // A is inferred as I64

Type Annotations

You can add type annotations with ::

def x : I64 := 42

Holes (Type Inference)

The _ placeholder (Hole) tells the type checker to infer the type:

def x := _  // Type will be inferred

Universe Levels

Type represents the universe of types (universe 0). You can also use higher universes:

Type      // Universe 0
Type 1    // Universe 1
Type 2    // Universe 2

Prop

Prop is the type of propositions, used for logical statements:

def myProp : Prop := ...

Type-Level Functions

Types can be computed from values:

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

// Result takes type parameters E and A
def success : Result String I64 := ok 42

Dependent Type Examples

Option with Default

def Option.get_or_default (default : A) (self : Option A) : A :=
    match self {
        some a => a,
        none => default
    }

The return type A depends on the type parameter of Option A.

Polymorphic List Operations

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

The return type Option A depends on the element type of the list.

Summary

• Pi types represent function types
• Forall types {A : Type} introduce implicit arguments
• Holes _ enable type inference
• Universe levels (Type, Type 1) organize types
• Prop represents logical propositions
• Dependent types enable precise specifications

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
}

Field Default Values

Fields can have default values using :=:

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

def origin := { x := 0, y := 0 }
// z defaults to 0

Linear and Affine Fields

Field access can be restricted with multiplicity annotations ! (linear, exactly once) or ? (affine, at most once):

struct Resource {
    !handle : FileHandle,   // linear — must be used exactly once
    ?label : String,        // affine — may be unused
    metadata : I64          // unrestricted (default)
}

Creating Struct Values

Struct values are created with brace syntax:

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

Field Access

Access fields using dot notation:

def getX (p : Point) : I64 := p.x
def getY (p : Point) : I64 := p.y

Structs vs Types

A struct is equivalent to a single-constructor type. This struct:

struct Point {
    x : I64,
    y : I64
}

Is equivalent to:

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

Generic Structs

Structs can have type parameters:

struct Pair A B {
    first : A,
    second : B
}

def example := { first := "hello", second := 42 }

Pattern Matching on Structs

You can pattern match on struct constructors:

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

Summary

• struct defines record types with named fields
• Struct values use { field := value } syntax
• Field access uses dot notation
• Structs are equivalent to single-constructor types

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

Error Handling

Monad provides functional error handling through the Result and Option types.

The Result Type

The Result type represents computations that may fail with an error:

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

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 handleResult (r : Result String I64) : String :=
    match r {
        ok n => "Success: " ++ n,
        err e => "Error: " ++ e
    }

Chaining Results with Monad

The Result type can have a Monad instance for chaining:

def compute (x : I64) (y : I64) : Result String I64 :=
    divide x y >>= fn result =>
        ok (result * 2)

The Option Type

The Option type represents computations that may return nothing:

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

Basic Usage

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

Handling Options

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

Using get_or_default

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

Custom Error Types

Define domain-specific error types:

type DatabaseError {
    notFound,
    connectionFailed,
    permissionDenied,
    timeout
}

def findUser (id : I64) : Result DatabaseError String :=
    err notFound

Combining with the IO Monad

Error handling in effectful code:

use io
open IO

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

Summary

• Result E A for errors with payloads
• Option A for simple failure cases
• Pattern matching for handling both types
• Monad instances enable chaining with >>=
• Define custom error types for domain-specific errors

Next, we'll explore modules and imports for organizing code.

Linear Types

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

Overview

Every variable in Monad has a multiplicity that controls how many times it can be used:

Syntax

Multiplicity is declared with a prefix on the parameter name:

// Many (default) — no prefix
def add (a : I64) (b : I64) : I64 := a + b

// Linear — must be used exactly once
def process (!handle : FileHandle) : IO Unit := close handle

// Affine — may be used 0 or 1 time  
def log (?msg : String) : IO Unit :=
    match msg {
        some s => println s,
        none => pure ()
    }

Multiplicity annotations work in all parameter positions:

// Lambda parameters
\!x : I64 => x

// Implicit parameters
{!A : Type}

// Function definitions
def f (!x : I64) (?y : I64) (z : I64) : I64 := x

Usage Rules

The type checker enforces these rules at compile time (no runtime overhead):

1. Linear (!x): Must appear exactly once in the function body
2. Affine (?x): Must appear at most once (0 or 1 occurrence)
3. Many (x): No restriction — can be used 0, 1, or many times

// ✓ Passes: x used exactly once
def ok (!x : I64) : I64 := x

// ✗ Fails: x not used
def unused (!x : I64) : I64 := 42

// ✗ Fails: x used twice
def overused (!x : I64) : I64 := x + x

// ✓ Passes: affine can be unused
def affine_ok (?x : I64) : I64 := 42

// ✓ Passes: many can be used many times  
def many_ok (x : I64) : I64 := x + x + x

Nested Lambdas and Scope

Linear type checking is per-function-boundary. Each lambda's linear parameters are verified independently:

// ✓ Passes: x used in outer scope (after inner lambda)
def outer (!x : I64) : I64 :=
    let f := \y : I64 => y in
    x

// ✗ Fails: x used twice (once inside inner lambda, once outside)
def bad (!x : I64) : I64 :=
    (\y : I64 => x) + x

Current Limitations

• Pattern matching with linear constructor fields is not yet enforced
• Arrow multiplicity (Pi.mult) is not yet checked at application sites
• Let-bound variables are not yet tracked for linearity
• No subtyping/subsumption rules (Many subsumes Linear/Affine)

Comparison to Rust

Future Work

• Subtyping: Many subsumes both Linear and Affine
• Pattern matching with linear constructor fields
• LLVM codegen: noalias attributes for linear parameters
• In-place update optimization for linear values

Modules and Imports

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

Basic Module Structure

Each .mo file is a module. The module name is derived from the file path.

Importing Modules

Use use to bring a module into scope:

use io
use init
use math

After use io, you can access definitions with their full path:

use io

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

Opening Modules

Use open to make a module's definitions available without prefixes:

use io
open IO

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

Now println is available directly instead of IO.println.

Opening Standard Types

The prelude opens several types by default:

open Unit    // makes `unit` available
open Bool    // makes `true`, `false` available
open Result  // makes `ok`, `err` available
open Option  // makes `some`, `none` available

Module Paths

Definitions are accessed using dot notation:

use init

def result : I64 := I64.add 3 4

The Standard Library

Monad ships with several standard modules:

Complete Example

use io
use init
open IO

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
• use brings modules into scope
• open makes definitions available without prefixes
• Dot notation accesses definitions by path
• Standard library modules provide common functionality

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

The IO Monad

Monad provides a safe way to perform 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:

use io
open IO

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

Basic IO Operations

Printing Output

use io
open IO

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

IO.println takes a String and returns IO Unit.

The IO Type

The IO type is defined as:

type IO A {
    io A
}

IO Monad Instance

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

Do Notation

The do block sequences IO actions. Two equivalent syntaxes are available:

Standard do { ... } syntax

use io
open IO

def greet : IO Unit :=
    do {
        println "Enter your name:"
        // name <- getLine  // Note: getLine not yet implemented
        println "Hello!"
    }

Inline do block syntax

Functions can use { ... } directly instead of := do { ... }:

use io
open IO

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

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

Do Block Statements

Multiple statements are separated by semicolons:

def multiStep : IO Unit {
    println "Step 1";
    let value := 42
    println "Step 2"
}

Native Functions

IO operations are implemented as native functions that call Rust code:

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

The @[native name] attribute marks a function as implemented in Rust.

Running IO Programs

The runtime executes the main function:

use io
open IO

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

Run with:

cargo run -- run program.mo

Command-line arguments are passed to main as List String.

Combining IO with Other Types

use io
use init
open IO

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

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

Summary

• IO A encapsulates side effects
• IO.println is the primary output function
• do notation sequences IO actions
• IO is a proper monad with pure and bind
• main is the program entry point, receiving List String arguments
• Native functions bridge Monad and Rust

This concludes the tutorial series. Continue to the reference documentation for detailed API information.

Reference

This chapter provides a quick reference for Monad syntax and built-in features.

Keywords

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

Reserved names: Type, Pred

Comments

// Single line comment

/* Multi-line
   comment */

Docstrings

/// Documentation for the following declaration
def greet (name : String) : IO Unit := println name

/// Module-level documentation (at top of file)

Docstrings are parsed and stored on declarations, retained through module loading for tooling and inspection.

Lambda Expressions

Three equivalent syntaxes:

fn x => x + 1
\ x => x + 1
ꟛ x => x + 1

Backtick Operators

x `f` y   // Equivalent to f x y

Identifiers in backticks are treated as infix operators (like Haskell).

Let Expressions

// Inline style
let x := 10 in x + 1

// Semicolon style
let x := 10;
let y := 20;
in x + y

// With type annotation
let x : I64 := 10 in x + 1

Numeric Literals

42        // I64 (default)
42i8      // I8
42i16     // I16
42i32     // I32
42i64     // I64
42u8      // U8
42u16     // U16
42u32     // U32
42u64     // U64
3.14      // F64 (default)
3.14f32   // F32
3.14f64   // F64

Type Annotations

(expr : Type)

Any term can be annotated with its type using (term : Type) syntax.

Method Call Syntax

x.fun        // Desugared to A.fun x (where A is the type of x)
x.fun args   // Desugared to A.fun args x

Method calls are desugared in the type checker. The receiver type is extracted and prepended to the method name.

Match Expressions

match value {
    constructor args => body,
    constructor => body
}

If Expressions

if condition then thenBranch else elseBranch

Do Notation

Two equivalent syntaxes are available:

// Standard syntax
def example : IO Unit := do {
    let name <- action;
    let x := value;
    return value
}

// Inline do block (equivalent)
def example : IO Unit {
    let name <- action;
    let x := value;
    return value
}

Statement Types

Multiple statements are separated by semicolons.

Struct Values

struct Point {
    x : I64,
    y : I64
}

def p := { x := 3, y := 4 }

Attributes

Declarations can be annotated with @[...] attributes:

@[native "function_name"]   // Declare a Rust-native function
@[test]                     // Mark as a test (run via `cargo run -- test <file>`)

Native Functions

Mark functions as implemented in Rust:

@[native nativeName]
def functionName (params) : ReturnType

Example from the standard library:

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

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

Infix Operators

infix (operator) := functionName

Built-in Operators

Type Definitions

// Simple type
type Bool {
    true,
    false
}

// Type with parameters
type Result E A {
    ok (a : A),
    err (e : E)
}

// Type with constructors carrying data
type Option A {
    some (a : A),
    none
}

// Empty type
type Void {}

Struct Definitions

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

Class Definitions

// Simple class
class Functor (F : Type -> Type) {
    def map (f : A -> B) : (F A) -> F B
}

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

Instance Definitions

// Simple instance
instance FromListLiteral List {
    def cons (a : A) (l : List A) : List A := List.cons a l
    def empty : List A := List.empty
}

// Instance with constraints
instance [Add A] Add (List A) {
    def add (a b : List A) : List A := List.append a b
}

Function Definitions

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

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

// With constraints
def double [Add A] (x : A) : A := HAdd.add x x

// Do block syntax (alternative to :=)
def greet (name : String) : IO Unit {
    println name
}

// Do block with multiple statements
def multiStep : IO Unit {
    println "Step 1";
    println "Step 2"
}

// Native function
@[native println]
def IO.println (s : String) : IO Unit

Modules

// Import module
use io

// Open module (no prefix needed)
open IO

// Access by path
IO.println "hello"

Dot Macro

The . operator (x.y.z) is treated as a compile-time macro that concatenates module paths into a single variable reference. This is how module paths like List.append work.

Constraint Solver

Recursive instance constraints (e.g., instance [Show A] Show (List A) { ... }) are handled by the constraint solver. It uses a visiting set to detect and resolve cyclic constraint dependencies during instance resolution.

Standard Library Types

Standard Library Classes

Standard Library Functions

Bool

• Bool.not (b : Bool) : Bool
• Bool.and (a b : Bool) : Bool
• Bool.or (a b : Bool) : Bool

Option

• Option.get_or_default (default : A) (self : Option A) : A

List

• List.is_empty (self : List A) : Bool
• List.append (a b : List A) : List A
• List.first (self : List A) : Option A
• List.last (self : List A) : Option A
• List.flatten (self : List (List A)) : List A
• List.tail (l : List A) : List A

IO

• IO.println (s : String) : IO Unit

I64

• I64.add (a b : I64) : I64

Pipeline

• fun_apply (f : A -> B) (a : A) : B — f <| a
• apply_fun (a : A) (f : A -> B) : B — a |> f

CLI Usage

# Build the compiler
cargo build --package monad-core

# Run a Monad file
cargo run -- run file.mo

# Run with debug output
cargo run -- run file.mo -- --debug

# Run @[test] annotated definitions
cargo run -- test file.mo

# Compile to native binary (requires llvm feature)
cargo run -- compile file.mo

# Start the REPL (requires repl feature)
cargo run -- repl