implementing-inference-rules.md

Implementing Inference Rules

When first reading programming language papers, it can be challenging to figure out how to translate the notation into working implementations. The following post is intended to help show how these rules correspond to working implementations in Prolog, OCaml, and Lean, for a very simple language of arithmetic expressions.

Natural deduction

T ::=
  | Int
  | Bool

t ::=
  | 0
  | t₁ + t₂
  | t₁ == t₂
  | true
  | false

The inference rules for the typing judgement, t : T, are defined below:

───────────
  n : Int

  t₁ : Int    t₂ : Int
────────────────────────
    t₁ + t₂ : Int

  t₁ : Int    t₂ : Int
────────────────────────
    t₁ == t₂ : Bool

───────────────     ────────────────
  true : Bool         false : Bool

Prolog

Prolog lets you prototype the inference rules in a very succinct way - but it can be a bit error-prone and brittle due to the lack of type and mode checking! The has_type/2 predicate can run in multiple 'modes' - for example as a type checker, or a type inferencer. You could even use it to generate terms based on a given type.

has_type(int(Num), int).
has_type(add(Tm1, Tm2), int) :-
  has_type(Tm1, int),
  has_type(Tm2, int).
has_type(equal(Tm1, Tm2), bool) :-
  has_type(Tm1, int),
  has_type(Tm2, int).
has_type(true, bool).
has_type(false, bool).

OCaml

In OCaml we first need to define some syntax trees. We do this using recusrive datatypes, and it should be pretty clear to see the correspondance between our definitions and the original grammars above:

type ty =
  | Bool
  | Int

type tm :=
  | Int of int
  | Add of tm * tm
  | Equal of tm * tm
  | True
  | False

We can now create a number of different implementations that satisfy the same typing rules, each corresponding to a different “mode” of the typing judgement.

Type checking is a function that assumes that both the term and the type are inputs:

let rec check (tm : tm) (ty : ty) : bool =
  match tm, ty with
  | Int n, Int -> true
  | Add (tm1, tm2), Int ->
      check tm1 Int && check tm2 Int
  | Equal (tm1, tm2), Bool ->
      check tm1 Int && check tm2 Int
  | True, Bool -> true
  | False, Bool -> true
  | _, _ -> false

Type inference assumes that the term is the input, and the type is an output:

let rec infer (tm : tm) : ty option =
  match tm with
  | Int n -> Some Int
  | Add (tm1, tm2) -> 
      begin match infer tm1, infer tm2 with
      | Some Int, Some Int -> Some Int
      | _, _ -> None
      end
  | Equal (tm1, tm2) -> 
      begin match infer tm1, infer tm2 with
      | Some Int, Some Int -> Some Bool
      | _, _ -> None
      end
  | True => Some Bool
  | False => Some Bool

The remaining modes of the type checker, corresponding to term generators, are left as an exercise to the reader¹. These could be used for property-based testing of the above type checking functions, and for testing evaluators and compilers.

Lean 4

In Lean (like in OCaml) we first need to define our syntax trees as inductive datatypes:

inductive Ty where
  | bool : Ty
  | int : Ty

inductive Tm where
  | int : Int → Tm
  | add : Tm → Tm → Tm
  | equal : Tm → Tm → Tm
  | true : Tm
  | false : Tm

The inference rules can be encoded as an inductive proposition:

inductive HasType : Tm → Ty → Prop where
  | int {n} : HasType (.int n) .int
  | add {tm₁ tm₂} :
      HasType tm₁ .int →
      HasType tm₂ .int →
      HasType (.add tm₁ tm₂) .int
  | equal {tm₁ tm₂} :
      HasType tm₁ .int →
      HasType tm₂ .int →
      HasType (.equal tm₁ tm₂) .bool
  | true : HasType .true .bool
  | false : HasType .false .bool

We can now define different modes of the typing judgement as functions:

def check : Tm → Ty → Bool
| .int _, .int  => true
| .add tm₁ tm₂, .int  => check tm₁ .int && check tm₂ .int
| .equal tm₁ tm₂, .bool  => check tm₁ .int && check tm₂ .int
| .true, .bool => true
| .false, .bool => true
| _, _ => false

def infer : Tm → Option Ty
| .int _ => some .int
| .add tm₁ tm₂ =>
    match infer tm₁, infer tm₂ with
    | some .int, some .int => some .int
    | _, _ => none
| .equal tm₁ tm₂ =>
    match infer tm₁, infer tm₂ with
    | some .int, some .int => some .bool
    | _, _ => none
| .true => some .bool
| .false => some .bool

We can now prove that our implementations match with the inference rules:

theorem check_correct (tm : Tm) (ty : Ty) : (check tm ty = true) = HasType tm ty := by
  sorry

theorem infer_correct (tm : Tm) (ty : Ty) : (infer tm = some ty) = HasType tm ty := by
  sorry

See this gist for full proofs.

Footnotes

1. That is to say, I've not got around to thinking about them yet! ↩