Chapter 11: Datatypes and Pattern Matching

New files

src/data.rs

src/syn.rs

src/desugar.rs

Changed files

src/typecheck.rs

src/core.rs

src/elaborate.rs

src/ast.rs

src/core_lint.rs

src/core_type.rs

src/eval.rs

src/fixity.rs

src/layout.rs

src/lexer.rs

src/lib.rs

src/main.rs

src/parse.rs

src/rename.rs

src/renamed.rs

src/session.rs

src/types.rs

Motivation

Integers and functions have taken us a long way, but it’s time to build some proper data structures. A binary tree can be empty or contain a value and two subtrees. A lookup can fail or return a result. Algebraic datatypes let us say these things directly, without inventing special values to mean “nothing here”.

Pattern matching gives us an equally direct way to take the values apart. The shape of the data becomes the shape of the program. This is one of the beautiful parts of functional programming, and we’ll use it constantly from here on.

We’ll first implement matching by trying patterns in source order. That gives us a clear account of what a match means. In Chapter 16 we’ll turn the same matches into decision trees suitable for native code.

The Language, Now

Declarations introduce nominal types and their constructors. Constructor arguments are strict, and constructors can be passed around as curried functions.

data Tree a = Empty | Node (Tree a) a (Tree a)

size Empty = 0
size (Node left _ right) = 1 + size left + size right

main = size (Node Empty 42 Empty)

Read size beside the datatype. Empty contributes zero. A Node contributes one, plus the sizes of its two children. The definition follows the data almost word for word. That’s beautiful, and it scales to much more interesting trees.

We can mirror a tree just as directly.

data Tree a = Empty | Node (Tree a) a (Tree a)

mirror Empty = Empty
mirror (Node left x right) = Node (mirror right) x (mirror left)

main = mirror (Node Empty 1 (Node Empty 2 Empty))

Notice that mirror never examines x. Its type is Tree a -> Tree a, so it works for trees of any element type. The recursion changes the shape while leaving the values alone.

Equations may have nested constructor patterns, literals, wildcards, and as-patterns. Lists, pairs, triples, and unit have dedicated syntax. Guards must have type Bool. If all guards fail, matching continues with the next equation.

select all@(x : xs) | x < 0 = xs
select all = all

main = select [-1,2,3]

A where block belongs to its entire equation, including every guard. A case alternative may also have guards and a where block. Pattern lambdas and strict, non-recursive pattern bindings work as well: let (x,y) = (20,22) in x + y. Types remain first-order here. A datatype parameter has kind *, so Tree Int is valid but applying a parameter as in f Int waits for Chapter 13.

The initial Prelude is embedded from this actual Fun source:

data Bool = False | True

data Ordering = LT | EQ | GT

data Maybe a = Nothing | Just a

data Either a b = Left a | Right b

data [] a = [] | (:) a [a]

data () = ()

data (,) a b = (,) a b

data (,,) a b c = (,,) a b c

Theory

A datatype declaration supplies a polymorphic scheme for each constructor. For example, Node has type Tree a -> a -> Tree a -> Tree a, quantified over a. Each occurrence instantiates that scheme with fresh metavariables, just as a polymorphic function occurrence does [Marlow (2010); Pierce (2002)].

For a constructor with instantiated field types, a pattern judgment returns the bindings introduced by its subpatterns:

$\frac{K : τ _{1} \to τ _{2} \to T Γ ⊢ p _{1} : τ _{1} \Rightarrow Δ _{1} Γ ⊢ p _{2} : τ _{2} \Rightarrow Δ _{2}}{Γ ⊢ K p _{1} p _{2} : T \Rightarrow Δ _{1} , Δ _{2}} (Constructor pattern)$

The combined pattern environment must not bind a name twice. Each row is checked against the same scrutinee types, and every successful right-hand side must have the same result type. Guards additionally unify with Bool.

Fun evaluates fields before constructing a value. A failed match raises a runtime error. There are no lazy patterns or suspended constructor fields. Exhaustiveness and redundancy warnings require a separate analysis. They arrive with match compilation (Maranget 2007).

Implementation

Declaring names before checking fields

data.rs first allocates every type head, then converts constructor fields. This permits mutually recursive datatypes. The immutable table stores each type’s arity, each constructor’s scheme, and declaration-order tags. Duplicate names, unbound field variables, and incorrect type arities are diagnosed before expression inference begins.

The renamer resolves constructor names in expressions and patterns separately from ordinary variables. Pattern variables receive fresh identities for each row. Its scope then contains those variables and the row’s local declarations while visiting both guards and right-hand sides.

Lowering syntax into Syn

desugar.rs introduces an explicit pass between renaming and inference. Lists and tuples become constructor applications. if becomes a two-row match on True and False. Infix && and || first become conditionals. As first-class values those operators are ordinary eta-expanded functions, whose arguments are evaluated by call-by-value application.

A single equation containing only variable patterns can use ordinary lambdas and lets. Other equations become a lambda for each argument followed by a match:

#![allow(unused)]
fn main() {
let params: Vec<_> = (0..rows[0].patterns.len())
    .map(|_| self.sess.fresh_id("$match"))
    .collect();
let scruts = params
    .iter()
    .map(|id| self.node(Kind::Var(id.clone()), span))
    .collect();
let mut body = self.node(Kind::Match(scruts, rows), span);
for id in params.into_iter().rev() {
    body = self.node(Kind::Lam(id, Box::new(body)), span);
}
body
}

Strict pattern bindings use one checked bundle of their bound values, represented by nested pairs, followed by projections. The right-hand side is evaluated once. Its newly bound names are hidden while renaming that right-hand side, so an outer binding of the same spelling remains accessible. An unused top-level pattern binding still executes and can fail.

Inferring constructor patterns

The checker instantiates a constructor scheme, separates its field arrows from its result type, and unifies the result with the scrutinee. It then checks each subpattern against the corresponding instantiated field:

#![allow(unused)]
fn main() {
PatKind::Con(id, patterns) => {
    let info = self.data.con(id).clone();
    if patterns.len() != info.fields.len() {
        return Err(Diagnostic::error(
            ErrorCode::Mismatch,
            format!(
                "{} expects {} pattern fields",
                id.name,
                info.fields.len()
            ),
            pattern.span,
        ));
    }
    let mut ty = self.instantiate(&info.scheme);
    let mut fields = Vec::new();
    for _ in patterns {
        let Type::Arrow(a, b) = ty else {
            unreachable!("constructor arity")
        };
        fields.push(*a);
        ty = *b;
    }
    self.unify(expected, &ty, &site)?;
    for (pattern, ty) in patterns.iter().zip(fields) {
        self.pattern(env, pattern, &ty)?;
    }
}
}

Pattern variables enter the row environment monomorphically. Local bindings retain ordinary let-polymorphism. The checker records expression and pattern-binder types alongside the instantiation metadata already needed by System F elaboration.

Extending Core and lint

Elaboration eta-expands constructor values into lambdas whose bodies are saturated Con nodes. Strict lets evaluate match scrutinees once and in source order. Core keeps nested patterns until the decision-tree compiler is introduced:

#![allow(unused)]
fn main() {
/// Nested patterns remain until the decision-tree compiler in Chapter 16.
#[derive(Clone, Debug)]
pub enum Pat {
    Var(Id),
    Wild,
    As(Id, Box<Pat>),
    Con(crate::data::ConId, Vec<Pat>),
    Lit(Lit),
}

/// A guarded row falls through when all its Boolean tests fail.
#[derive(Clone, Debug)]
pub enum RowBody {
    Plain(Box<Expr>),
    Guarded(Vec<(Expr, Expr)>),
}

/// Row-local declarations run after patterns match and are shared by the guards.
#[derive(Clone, Debug)]
pub struct Row {
    pub pats: Vec<Pat>,
    pub locals: Vec<BindGroup>,
    pub body: RowBody,
    pub span: Span,
}

/// Scrutinees name strict preceding lets; the match records its result type and failure site.
#[derive(Clone, Debug)]
pub struct Match {
    pub scruts: Vec<Id>,
    pub rows: Vec<Row>,
    pub result: Type,
    pub span: Span,
}
}

Lint independently checks constructor type arguments, field counts and field types. For a constructor pattern it instantiates the declaration under the scrutinee’s type arguments, then checks each binder. Guards must be Boolean, and every row must produce the declared match result. Malformed-Core tests exercise these checks without asking the surface inferencer to validate their inputs.

Executing rows

The interpreter evaluates constructor fields left to right. Matching already evaluated values recursively tests constructors and literals, extending a private row environment with variables and as-patterns:

#![allow(unused)]
fn main() {
fn matches_pattern(p: &core::Pat, v: &Value, env: &mut Env) -> bool {
    match p {
        core::Pat::Wild => true,
        core::Pat::Var(id) => {
            env.push((id.clone(), v.clone()));
            true
        }
        core::Pat::As(id, p) => {
            env.push((id.clone(), v.clone()));
            matches_pattern(p, v, env)
        }
        core::Pat::Lit(l) => matches!(v,Value::Lit(actual) if l==actual),
        core::Pat::Con(id, ps) => match v {
            Value::Con(actual, vs)
                if id == actual && ps.len() == vs.len() =>
            {
                ps.iter().zip(vs).all(|(p, v)| matches_pattern(p, v, env))
            }
            _ => false,
        },
    }
}
}

A failed pattern discards that environment and tries the next row. A successful pattern evaluates its where groups once, then tests guards in order. If all fail, execution continues with the next row. Exhausting the rows reports fun: pattern match failure at FILE:LINE:COL and exits with status 1.

The value printer uses constructor precedence, so a nested application prints as Just (Left 3). Lists and tuples use their surface notation. A character list prints as ['a','b'], while primitive strings keep double quotes.

Running It

$ cd crates/ch11_data
$ cargo run -q -- run tests/programs/data/tree.fun --lint
(True,False)
$ cargo run -q -- dump --pass=syn tests/programs/data/bool-data.fun
nonrec { not#9 = (lambda $match#11 (match $match#11 [ (True) -> False ] [ (False) -> True ])); }
nonrec { main#10 = (app (app (,) (app not#9 True)) (app not#9 False)); }
$ cargo test --test data

Guard fallthrough is worth experimenting with. Make the first pattern match but its guard fail, then check that the next equation runs. Also try an unused top-level pattern binding that fails. Strict evaluation means “unused” doesn’t make the match disappear. These examples exercise the parts that an ordinary successful tree traversal might miss.

Exercises

Introductory. define a binary tree mirror function and test it on an asymmetric tree.
Intermediate. Explain the type errors from a constructor pattern with too few fields and from two equations returning different types.
Intermediate. Write two guards that fall through to a later equation. Move their shared computation into where and inspect the Syn dump.
Advanced. Compare strict pattern binding with Haskell’s ordinary pattern binding. Construct a program whose termination or error behavior differs.
Advanced. Design a lint test that swaps two differently typed constructor fields while preserving the field count.

Write You a Haskell