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

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

You can add type annotations with ::

def x : I64 := 42

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

def x := _  // Type will be inferred

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 is the type of propositions, used for logical statements:

def myProp : Prop := ...

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

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.

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.

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