Types (kernel)

2.1 Types

τ ::= α | τ → τ | T τ₁ … τₙ

2.2 Universal quantification

∀α. τ

This corresponds to * in surface syntax.

2.3 Row types (records)

{ l₁ : τ₁, … | ρ }

• open records
• structural typing
• patching relies on this

2.4 Row transforms (derived)

Pick, Omit, Optional, Required, Rename, and Defaulted are surface-level type operators that transform record rows. They are derived and elaborate to plain record types in the kernel.