elab-stlc-row-unification

Simply typed lambda calculus with structural record and variant types

• Extends elab-stlc-unification (+ structural records, structural variants)

---

This elaborator introduces structural record and variant types to a simply typed lambda calculus. In order to reduce the need for up-front type annotations, we use row metavariables¹ to accumulate maps of labelled types during unification. This is similar to the “flexible records” approach used in some implementations of Standard ML. We could extend this to support row polymorphism in a future project, but for now this is limited to inferring monomorphic rows.

let point x y :=
  { x := x; y := y };

let add p1 p2 := point (p1.x + p2.x) (p1.y + p2.y);
let sub p1 p2 := point (p1.x - p2.x) (p1.y - p2.y);

let _ :=
  add (point 1 2) (point 3 4);

let apply x :=
  match x with {
    | [incr := x] => x + 1
    | [decr := x] => x - 1
    | [square := x] => x * x
  };

apply [incr := 1]

Elaboration output

let point : Int -> Int -> { x : Int; y : Int } :=
  fun (x : Int) => fun (y : Int) => { x := x; y := y };
let add :
      { x : Int; y : Int } -> { x : Int; y : Int } -> { x : Int; y : Int }
:=
  fun (p1 : { x : Int; y : Int }) => fun (p2 : { x : Int; y : Int }) =>
    point (#int-add p1.x p2.x) (#int-add p1.y p2.y);
let sub :
      { x : Int; y : Int } -> { x : Int; y : Int } -> { x : Int; y : Int }
:=
  fun (p1 : { x : Int; y : Int }) => fun (p2 : { x : Int; y : Int }) =>
    point (#int-sub p1.x p2.x) (#int-sub p1.y p2.y);
let _ : { x : Int; y : Int } := add (point 1 2) (point 3 4);
let apply : [decr : Int | incr : Int | square : Int] -> Int :=
  fun (x : [decr : Int | incr : Int | square : Int]) =>
    match x with {
      | [decr := x] => #int-sub x 1
      | [incr := x] => #int-add x 1
      | [square := x] => #int-mul x x
    };
apply ([incr := 1] : [decr : Int | incr : Int | square : Int]) : Int

Project overview

Module	Description
Main	Command line interface
Lexer	Lexer for the surface language
Parser	Parser for the surface language
Surface	Surface language, including elaboration
Core	Core language, including normalisation, unification, and pretty printing
Prim	Primitive operations

Examples

More examples can be found in the examples and tests directories.

Footnotes

1. The term “row” purportedly comes from Algol 68:

   Let $L$ be a fixed countable set of labels $a_1, a_2, \dots$. If $p: D \rarr X$, where $D$ is a finite subset of $L$, (that is a family of elements of $X$ indexed by a finite subset of $L$) then we call $\rho$ a row of $X$’s (This terminology is stolen from Algol 68) p a row of X's. If we fix an ordering on L, then any row has a canonical finite representation $\langle (a_{i_1}, x_1), \dots, (a_{i_n}, x_n)\rangle$ where the $a_{i_k}$ are in increasing order.

   -- Mitchell Wand, Complete Type Inference for Simple Objects, 1987

   Apparently Algol 68 used the term “row” to refer to arrays. ↩