Local definitions and decisions

Local bindings name intermediate results. Conditionals and pattern matching choose among results while preserving one checked result type.

Single bindings

let x = 20 in x + 22

The name exists only in the body after in. A type annotation can guide checking:

let x : Int = 42 in x

Sequential let blocks

let {
    x = 3;
    double(n:Int) : Int = n * 2;
    y = double(x)
} in x + y

Bindings are sequential: double sees x, and y sees both. A local function may optionally repeat function before its name. Semicolons separate bindings; commas remain data separators.

Let blocks desugar to nested lexical bindings. They are not mutable statement blocks.

Conditionals

if temperature < 0.0 then "freezing" else "above freezing"

The condition must be Bool, and both branches must check against one result type. if is an expression, so it may appear anywhere a value is expected.

Conceptually, conditionals are matching on Bool; they do not introduce a separate truthiness conversion.

Match expressions

function fromMaybe(fallback:a, item:Maybe(a)) : a = match item
    | Nothing -> fallback
    | Just * value -> value;

Patterns include constructors, literals, variables, wildcards, tuples, and named fields. A function body may omit the explicit scrutinee when its parameters form the matched input:

function length(xs:List(a)) : Nat = match
    | Nil -> Z
    | Cons * head * tail -> Succ(length(tail));

Exhaustiveness and redundancy

Closed data must be covered. Omitting Nothing above is a compile-time coverage error. Redundant cases are diagnosed because they often reveal a mistaken assumption.

Sealed class hierarchies can be exhaustive. Open class hierarchies need a fallback because another subclass may exist.

Annotations are not casts

(40 : Int) + 2

An annotation supplies an expected type and checks the expression against it. It does not convert a value. Representation conversion uses as only when a declared repr mapping justifies it; class downcasting uses downcast.

Scope and shadowing

Names follow lexical scope. Prefer distinct, descriptive local names where shadowing would make dependent types, effect labels, or evidence selection hard to read. Type variables introduced by existential unpacking have stricter escape rules discussed in Chapter 17.

Common mistakes

Both branches of if and every branch of match need a compatible result type. A block let is sequential, so an earlier binding cannot refer forward to a later sibling.

Recap

Use let to name pure intermediate values, if for two-way Boolean choice, and match when the structure of data matters. All are expressions with checked result types.

Normative details: Language Reference §8.