04 / Types

Types you never write down

B-Lambda has no type annotations at all. Every type you see was inferred from the structure of the term — and the Typing derivation tab will show you the proof, rule by rule, for any program you build.

The type vocabulary

Deliberately tiny. Four things:

Type	Written	Comes from
Integer	`int`	number literals, arithmetic
Boolean	`bool`	boolean literals, comparison, connectives
Type variable	`'a`, `'b`, …	an unconstrained parameter
Function	`'a -> 'b`	abstraction

Function types associate to the right, as usual: a two-parameter curried function has type int -> int -> int, which is int -> (int -> int).

How inference runs

Inference is Hindley-Milner. It re-runs on every workspace change and on every code refresh, and it is scheduled incrementally so that editing a large program stays responsive.

A λ parameter starts as a fresh type variable, and gets refined by how the body uses it.
An abstraction gets a function type from its parameter and body.
An application unifies the function's argument type with the actual argument, and takes the function's result type.
Literals, operators, comparison and conditionals contribute the int / bool constraints from the table in Blocks.
A let generalises its binding into a type scheme — see below.
A letrec is inferred monomorphically.

The results surface in four places: the Inferred types tab, the type comment on each block, a type comment in the generated code, and warning bubbles on any block that does not check.

Let-polymorphism

This is the one place where the type system does something you might not expect from the term alone. A let-bound value is generalised: its type variables are quantified, so each use of the name can instantiate them differently.

let id = λx. x in
  if (id True) then (id 42) else 0

Here id is used at bool -> bool and at int -> int in the same expression. Without generalisation the two uses would be forced to agree and the program would not type-check. The Let-Polymorphism example loads exactly this shape.

The identity function is the smallest demonstration

λx. x alone infers 'a -> 'a. The type variable is not a placeholder for something inference failed to work out — it is the answer. Nothing in the term constrains x, so the function genuinely works at every type.

The typing derivation

Types → Typing derivation renders the proof as nested premises-over-a-bar trees, the way a paper would print them. Each box is a sub-derivation; the label at the right of each bar is the rule that was applied.

Reading the judgement

The judgement is the standard one on the left of the colon and a pair on the right:

Γ ⊢ x : int ⊗ lambda_variable

Read it as “in context Γ, the term x has type int, and it is a variable block.” The left of the ⊗ is the inferred type; the right is which kind of block carries it. This is deliberate: B-Lambda is a visual language, so the thing being typed is not a bare term but a term with a shape, and the derivation says so rather than leaving you to infer it from the picture.

Function types are parenthesised before the pair, so the ⊗ can never be misread as binding inside the arrow:

Γ ⊢ λx. x : ('a -> 'a) ⊗ lambda_abstraction

The membership premise of T-Var carries the pair too — x : int ⊗ lambda_variable ∈ Γ — and when a block has an error the turnstile flips to ⊬, with ∈ becoming ∉ for an unbound variable.

Two places the pair does not appear

An empty socket derives Γ ⊢ □ : unknown with no ⊗, because a hole has no block to name yet. And the side conditions — assume: x : τ on T-Abs, bind: on T-Let, recursive bind: on T-LetRec — print the bare type. So a half-finished term will show pairs on its filled sub-terms and a plain unknown on its holes; that is expected, not an inconsistency.

A typing derivation for lambda y. ((2 + 3) + y), with T-Int on the literals, T-Var on y, T-NumOp on each addition, and T-Abs concluding a function type, each judgement showing its type paired with the block type that carries it. — **Fig. 1** The derivation for `λy. ((2 + 3) + y)`. Read bottom-up: `T-Int` on the literals, `T-Var` on `y`, `T-NumOp` on each addition, and `T-Abs` concluding `int -> int` — every judgement pairing its type with the block that carries it.

For a recursive program the derivation opens with the binding's own judgement, so you can see the type letrec committed to before it started checking the body:

The typing derivation for the factorial example, headed by a recursive bind side condition giving factorial a function type, with the condition, then and else branches each derived below. — **Fig. 2** *Factorial 5*. The header reads `recursive bind: factorial : int -> int` — the monomorphic type assumed for the recursive call, and one of the two places that prints a bare type rather than a pair — with each branch derived beneath it.

The corresponding Inferred types tab is the summary view: one line per top-level term with its type, plus a Selected block pane that reports the term, type and status of whichever block you have clicked.

Rule names

The rules you will see on the bars, and what each one concludes:

Rule	Concludes
`T-Var`	A variable's type, by looking it up in the context: `x : τ ∈ Γ`
`T-Int`	A number literal is `int`
`T-Bool`	A boolean literal is `bool`
`T-Abs`	An abstraction is a function type
`T-App`	An application, after unifying argument with parameter
`T-Paren`	A grouping block: the type of the term inside it, unchanged
`T-Let`	A `let`, after generalising the bound value
`T-LetRec`	A `letrec`, with the binding assumed monomorphically while its own body is checked
`T-NumOp`	Arithmetic: two `int`s give an `int`
`T-Cmp`	Comparison: two `int`s give a `bool`
`T-BoolOp`	`and` / `or`: two `bool`s give a `bool`
`T-Eq`	The `equal` case of the boolean operator, which gets its own rule name rather than reusing `T-BoolOp`
`T-If`	A conditional, after checking the condition is `bool` and unifying the two branches
`T-Hole`	An empty socket. Concludes `unknown`, and is the one rule with no `⊗` pair
`T-Unsupported`	A block the derivation generator has no rule for — you should not normally see this one

Additions to the context are written as assume: x : τ at the top of the box that introduces them, with bind: and recursive bind: for the two binding forms. Premises are labelled by their role — function, argument, body, condition, then, else, left, right — so a wide derivation stays readable. Top-level terms are headed Term 1, Term 2, and so on.

Comparing notations across the workshop

B-MJ uses the same T-* prefix for expression rules and adds WF-* rules for statements — see B-MJ's types chapter. MnL writes its judgement as Γ ⊢ term : Category ⊗ Type, and B-Lambda now pairs on the same ⊗ — but the two halves are the other way round, and they mean different things. MnL's left operand is the block's grammatical category; B-Lambda's right operand is the block type that carries the term, and its grammar is single-sorted, so nothing is being checked by the pair. It is there to say which visual form the type belongs to.

When it goes wrong

Two kinds of thing can be wrong: a term can be incomplete (an empty socket), or it can be ill-typed. Both are reported the same three ways.

A warning bubble on the block. Blockly's own warning icon, on the specific block that failed — not on its parent.
The Problems tab in the bottom panel, which lists every diagnostic. When there is nothing to report it says No problems detected. Type inference is current. — the second sentence matters, because it tells you the empty list is up to date rather than stale.
The status bar count, so you can see there is a problem without opening the panel.

An incomplete term is not treated as an error to be shouted about — a term you are halfway through building is expected. Inference gives what it can and reports the missing input, which is why the count usually drops to zero on its own as you finish connecting blocks.

Block Lambda is developed at L-Workshop. This help was written against Block Lambda 1.2.0.