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:

Type	Constructors	Description
Unit	unit	Single value
Bool	true, false	Boolean
I64 … I8	(primitive)	Signed integers, 64/32/16/8 bit
U64 … U8	(primitive)	Unsigned integers, 64/32/16/8 bit
F64, F32	(primitive)	Floats
String	of_bytes	UTF-8 string
Char	of_bytes	One Unicode codepoint, written 'x' — but see the caveat below
Nat	zero, succ	Natural numbers
List A	empty, cons	Linked list
Option A	some, none	Optional value
Result E A	ok, err	Success or error
Pair A B	pair	Two-element product; the target of tuple syntax
Void	(none)	Empty type
Any	any	Existential wrapper
IO A	io	The IO monad
True	trivial	Trivially true proposition (in Prop)
Eq A a b	refl	Propositional equality (in Prop)
Vec n A	nil, cons	Length-indexed vector

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.