porting-inference-rules.md

Inference Rules

Natural deduction

T ::=
  | Int
  | Bool

t1, t2 ::=
  | 0
  | t1 + t2
  | true
  | false

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

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

 ⊢ t1 : Int    ⊢ t2 : Int
──────────────────────────
    ⊢ t1 + t2  : Int

───────────────     ────────────────
 ⊢ 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 synthesizer. 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(true, bool).
has_type(false, bool).

Lean 4

Here we port the inference rules to an inductive proposition, and a couple of implementations (either a type checker or a type synthesizer).

inductive Ty :=
  | bool : Ty
  | int : Ty

inductive Tm :=
  | int : Int -> Tm
  | add : Tm -> Tm -> Tm
  | true : Tm
  | false : Tm

inductive HasType : Tm -> Ty -> Prop :=
  | int {n} : HasType (Tm.int n) Ty.int
  | add {tm1 tm2} :
      HasType tm1 Ty.int ->
      HasType tm2 Ty.int ->
      HasType (Tm.add tm1 tm2) Ty.int
  | true : HasType Tm.true Ty.bool
  | false : HasType Tm.false Ty.bool

def has_type : Tm -> Ty -> Bool
  | Tm.int n,       Ty.int  => true
  | Tm.add tm1 tm2, Ty.int  => has_type tm1 Ty.int && has_type tm2 Ty.int
  | Tm.true,        Ty.bool => true
  | Tm.false,       Ty.bool => true
  | _,              _       => false

def type_of : Tm -> Option Ty
  | Tm.int n => some Ty.int
  | Tm.add tm1 tm2 => 
      match type_of tm1, type_of tm2 with
        | some Ty.int, some Ty.int => some Ty.int
        | _,           _           => none
  | Tm.true => some Ty.bool
  | Tm.false => some Ty.bool