A Certified Type Checker

In this example, we build a certified type checker for a simple expression language.

Remark: this example is based on an example in the book Certified Programming with Dependent Types by Adam Chlipala.

inductive Expr where | nat : Nat → Expr | plus : Expr → Expr → Expr | bool : Bool → Expr | and : Expr → Expr → Expr

We define a simple language of types using the inductive datatype Ty, and its typing rules using the inductive predicate HasType.

inductive Ty where | nat | bool deriving DecidableEqinductive HasType : Expr → Ty → Prop | nat : HasType (.nat v) .nat | plus : HasType a .nat → HasType b .nat → HasType (.plus a b) .nat | bool : HasType (.bool v) .bool | and : HasType a .bool → HasType b .bool → HasType (.and a b) .bool

We can easily show that if e has type t₁ and type t₂, then t₁ and t₂ must be equal by using the cases tactic. This tactic creates a new subgoal for every constructor, and automatically discharges unreachable cases. The tactic combinator tac₁ <;> tac₂ applies tac₂ to each subgoal produced by tac₁. Then, the tactic rfl is used to close all produced goals using reflexivity.

theorem HasType.det (h₁ : HasType e t₁) (h₂ : HasType e t₂) : t₁ = t₂ := bye:Exprt₁:Tyt₂:Tyh₁:HasType e t₁h₂:HasType e t₂⊢ t₁ = t₂ cases h₁natt₂:Tyv✝:Nath₂:HasType (Expr.nat v✝) t₂⊢ Ty.nat = t₂plust₂:Tya✝²:Exprb✝:Expra✝¹:HasType a✝² Ty.nata✝:HasType b✝ Ty.nath₂:HasType (a✝².plus b✝) t₂⊢ Ty.nat = t₂boolt₂:Tyv✝:Boolh₂:HasType (Expr.bool v✝) t₂⊢ Ty.bool = t₂andt₂:Tya✝²:Exprb✝:Expra✝¹:HasType a✝² Ty.boola✝:HasType b✝ Ty.boolh₂:HasType (a✝².and b✝) t₂⊢ Ty.bool = t₂ <;>natt₂:Tyv✝:Nath₂:HasType (Expr.nat v✝) t₂⊢ Ty.nat = t₂plust₂:Tya✝²:Exprb✝:Expra✝¹:HasType a✝² Ty.nata✝:HasType b✝ Ty.nath₂:HasType (a✝².plus b✝) t₂⊢ Ty.nat = t₂boolt₂:Tyv✝:Boolh₂:HasType (Expr.bool v✝) t₂⊢ Ty.bool = t₂andt₂:Tya✝²:Exprb✝:Expra✝¹:HasType a✝² Ty.boola✝:HasType b✝ Ty.boolh₂:HasType (a✝².and b✝) t₂⊢ Ty.bool = t₂ cases h₂and.anda✝⁴:Exprb✝:Expra✝³:HasType a✝⁴ Ty.boola✝²:HasType b✝ Ty.boola✝¹:HasType a✝⁴ Ty.boola✝:HasType b✝ Ty.bool⊢ Ty.bool = Ty.bool <;>nat.natv✝:Nat⊢ Ty.nat = Ty.natplus.plusa✝⁴:Exprb✝:Expra✝³:HasType a✝⁴ Ty.nata✝²:HasType b✝ Ty.nata✝¹:HasType a✝⁴ Ty.nata✝:HasType b✝ Ty.nat⊢ Ty.nat = Ty.natbool.boolv✝:Bool⊢ Ty.bool = Ty.booland.anda✝⁴:Exprb✝:Expra✝³:HasType a✝⁴ Ty.boola✝²:HasType b✝ Ty.boola✝¹:HasType a✝⁴ Ty.boola✝:HasType b✝ Ty.bool⊢ Ty.bool = Ty.bool rflAll goals completed! 🐙

The inductive type Maybe p has two constructors: found a h and unknown. The former contains an element a : α and a proof that a satisfies the predicate p. The constructor unknown is used to encode "failure".

inductive Maybe (p : α → Prop) where | found : (a : α) → p a → Maybe p | unknown

We define a notation for Maybe that is similar to the builtin notation for the Lean builtin type Subtype.

notation "{{ " x " | " p " }}" => Maybe (fun x => p)

The function Expr.typeCheck e returns a type ty and a proof that e has type ty, or unknown. Recall that, def Expr.typeCheck ... in Lean is notation for namespace Expr def typeCheck ... end Expr. The term .found .nat .nat is sugar for Maybe.found Ty.nat HasType.nat. Lean can infer the namespaces using the expected types.

def Expr.typeCheck (e : Expr) : {{ ty | HasType e ty }} := match e with | nat .. => .found .nat .nat | bool .. => .found .bool .bool | plus a b => match a.typeCheck, b.typeCheck with | .found .nat h₁, .found .nat h₂ => .found .nat (.plus h₁ h₂) | _, _ => .unknown | and a b => match a.typeCheck, b.typeCheck with | .found .bool h₁, .found .bool h₂ => .found .bool (.and h₁ h₂) | _, _ => .unknowntheorem Expr.typeCheck_correct (h₁ : HasType e ty) (h₂ : e.typeCheck ≠ .unknown) : e.typeCheck = .found ty h := bye:Exprty:Tyh:HasType e tyh₁:HasType e tyh₂:e.typeCheck ≠ Maybe.unknown⊢ e.typeCheck = Maybe.found ty h revert h₂e:Exprty:Tyh:HasType e tyh₁:HasType e ty⊢ e.typeCheck ≠ Maybe.unknown → e.typeCheck = Maybe.found ty h cases typeCheck e with | found ty' h' => introfounde:Exprty:Tyh:HasType e tyh₁:HasType e tyty':Tyh':HasType e ty'h₂✝:Maybe.found ty' h' ≠ Maybe.unknown⊢ Maybe.found ty' h' = Maybe.found ty h; have := HasType.det h₁ h'founde:Exprty:Tyh:HasType e tyh₁:HasType e tyty':Tyh':HasType e ty'h₂✝:Maybe.found ty' h' ≠ Maybe.unknownthis:ty = ty'⊢ Maybe.found ty' h' = Maybe.found ty h; subst thisfounde:Exprty:Tyh:HasType e tyh₁:HasType e tyh':HasType e tyh₂✝:Maybe.found ty h' ≠ Maybe.unknown⊢ Maybe.found ty h' = Maybe.found ty h; rflAll goals completed! 🐙 | unknown => introsunknowne:Exprty:Tyh:HasType e tyh₁:HasType e tyh₂✝:Maybe.unknown ≠ Maybe.unknown⊢ Maybe.unknown = Maybe.found ty h; contradictionAll goals completed! 🐙

Now, we prove that if Expr.typeCheck e returns Maybe.unknown, then forall ty, HasType e ty does not hold. The notation e.typeCheck is sugar for Expr.typeCheck e. Lean can infer this because we explicitly said that e has type Expr. The proof is by induction on e and case analysis. Note that the tactic simp [typeCheck] is applied to all goal generated by the induction tactic, and closes the cases corresponding to the constructors Expr.nat and Expr.bool.

theorem Expr.typeCheck_complete {e : Expr} : e.typeCheck = .unknown → ¬ HasType e ty := byty:Tye:Expr⊢ e.typeCheck = Maybe.unknown → ¬HasType e ty induction e with simp [typeCheck]All goals completed! 🐙 | plus a b iha ihb => splitplus.h_1ty:Tya:Exprb:Expriha:a.typeCheck = Maybe.unknown → ¬HasType a tyihb:b.typeCheck = Maybe.unknown → ¬HasType b tyx✝¹:{{ ty | HasType a ty }}x✝:{{ ty | HasType b ty }}h₁✝:HasType a Ty.nath₂✝:HasType b Ty.natheq✝¹:a.typeCheck = Maybe.found Ty.nat h₁✝heq✝:b.typeCheck = Maybe.found Ty.nat h₂✝⊢ Maybe.found Ty.nat ⋯ = Maybe.unknown → ¬HasType (a.plus b) typlus.h_2ty:Tya:Exprb:Expriha:a.typeCheck = Maybe.unknown → ¬HasType a tyihb:b.typeCheck = Maybe.unknown → ¬HasType b tyx✝²:{{ ty | HasType a ty }}x✝¹:{{ ty | HasType b ty }}x✝:∀ (h₁ : HasType a Ty.nat) (h₂ : HasType b Ty.nat), a.typeCheck = Maybe.found Ty.nat h₁ → b.typeCheck = Maybe.found Ty.nat h₂ → False⊢ Maybe.unknown = Maybe.unknown → ¬HasType (a.plus b) ty next =>ty:Tya:Exprb:Expriha:a.typeCheck = Maybe.unknown → ¬HasType a tyihb:b.typeCheck = Maybe.unknown → ¬HasType b tyx✝¹:{{ ty | HasType a ty }}x✝:{{ ty | HasType b ty }}h₁✝:HasType a Ty.nath₂✝:HasType b Ty.natheq✝¹:a.typeCheck = Maybe.found Ty.nat h₁✝heq✝:b.typeCheck = Maybe.found Ty.nat h₂✝⊢ Maybe.found Ty.nat ⋯ = Maybe.unknown → ¬HasType (a.plus b) ty introsty:Tya:Exprb:Expriha:a.typeCheck = Maybe.unknown → ¬HasType a tyihb:b.typeCheck = Maybe.unknown → ¬HasType b tyx✝¹:{{ ty | HasType a ty }}x✝:{{ ty | HasType b ty }}h₁✝:HasType a Ty.nath₂✝:HasType b Ty.natheq✝¹:a.typeCheck = Maybe.found Ty.nat h₁✝heq✝:b.typeCheck = Maybe.found Ty.nat h₂✝a✝:Maybe.found Ty.nat ⋯ = Maybe.unknown⊢ ¬HasType (a.plus b) ty; contradictionAll goals completed! 🐙 next ra rb hnp =>ty:Tya:Exprb:Expriha:a.typeCheck = Maybe.unknown → ¬HasType a tyihb:b.typeCheck = Maybe.unknown → ¬HasType b tyra:{{ ty | HasType a ty }}rb:{{ ty | HasType b ty }}hnp:∀ (h₁ : HasType a Ty.nat) (h₂ : HasType b Ty.nat), a.typeCheck = Maybe.found Ty.nat h₁ → b.typeCheck = Maybe.found Ty.nat h₂ → False⊢ Maybe.unknown = Maybe.unknown → ¬HasType (a.plus b) ty -- Recall that `hnp` is a hypothesis generated by the `split` tactic -- that asserts the previous case was not taken intro h htty:Tya:Exprb:Expriha:a.typeCheck = Maybe.unknown → ¬HasType a tyihb:b.typeCheck = Maybe.unknown → ¬HasType b tyra:{{ ty | HasType a ty }}rb:{{ ty | HasType b ty }}hnp:∀ (h₁ : HasType a Ty.nat) (h₂ : HasType b Ty.nat), a.typeCheck = Maybe.found Ty.nat h₁ → b.typeCheck = Maybe.found Ty.nat h₂ → Falseh:Maybe.unknown = Maybe.unknownht:HasType (a.plus b) ty⊢ False cases ht with | plus h₁ h₂ =>ty:Tya:Exprb:Expriha:a.typeCheck = Maybe.unknown → ¬HasType a tyihb:b.typeCheck = Maybe.unknown → ¬HasType b tyra:{{ ty | HasType a ty }}rb:{{ ty | HasType b ty }}hnp:∀ (h₁ : HasType a Ty.nat) (h₂ : HasType b Ty.nat), a.typeCheck = Maybe.found Ty.nat h₁ → b.typeCheck = Maybe.found Ty.nat h₂ → False⊢ Maybe.unknown = Maybe.unknown → ¬HasType (a.plus b) ty exact hnp h₁ h₂ (typeCheck_correct h₁ (iha · h₁)) (typeCheck_correct h₂ (ihb · h₂))All goals completed! 🐙 | and a b iha ihb => splitand.h_1ty:Tya:Exprb:Expriha:a.typeCheck = Maybe.unknown → ¬HasType a tyihb:b.typeCheck = Maybe.unknown → ¬HasType b tyx✝¹:{{ ty | HasType a ty }}x✝:{{ ty | HasType b ty }}h₁✝:HasType a Ty.boolh₂✝:HasType b Ty.boolheq✝¹:a.typeCheck = Maybe.found Ty.bool h₁✝heq✝:b.typeCheck = Maybe.found Ty.bool h₂✝⊢ Maybe.found Ty.bool ⋯ = Maybe.unknown → ¬HasType (a.and b) tyand.h_2ty:Tya:Exprb:Expriha:a.typeCheck = Maybe.unknown → ¬HasType a tyihb:b.typeCheck = Maybe.unknown → ¬HasType b tyx✝²:{{ ty | HasType a ty }}x✝¹:{{ ty | HasType b ty }}x✝:∀ (h₁ : HasType a Ty.bool) (h₂ : HasType b Ty.bool), a.typeCheck = Maybe.found Ty.bool h₁ → b.typeCheck = Maybe.found Ty.bool h₂ → False⊢ Maybe.unknown = Maybe.unknown → ¬HasType (a.and b) ty next =>ty:Tya:Exprb:Expriha:a.typeCheck = Maybe.unknown → ¬HasType a tyihb:b.typeCheck = Maybe.unknown → ¬HasType b tyx✝¹:{{ ty | HasType a ty }}x✝:{{ ty | HasType b ty }}h₁✝:HasType a Ty.boolh₂✝:HasType b Ty.boolheq✝¹:a.typeCheck = Maybe.found Ty.bool h₁✝heq✝:b.typeCheck = Maybe.found Ty.bool h₂✝⊢ Maybe.found Ty.bool ⋯ = Maybe.unknown → ¬HasType (a.and b) ty introsty:Tya:Exprb:Expriha:a.typeCheck = Maybe.unknown → ¬HasType a tyihb:b.typeCheck = Maybe.unknown → ¬HasType b tyx✝¹:{{ ty | HasType a ty }}x✝:{{ ty | HasType b ty }}h₁✝:HasType a Ty.boolh₂✝:HasType b Ty.boolheq✝¹:a.typeCheck = Maybe.found Ty.bool h₁✝heq✝:b.typeCheck = Maybe.found Ty.bool h₂✝a✝:Maybe.found Ty.bool ⋯ = Maybe.unknown⊢ ¬HasType (a.and b) ty; contradictionAll goals completed! 🐙 next ra rb hnp =>ty:Tya:Exprb:Expriha:a.typeCheck = Maybe.unknown → ¬HasType a tyihb:b.typeCheck = Maybe.unknown → ¬HasType b tyra:{{ ty | HasType a ty }}rb:{{ ty | HasType b ty }}hnp:∀ (h₁ : HasType a Ty.bool) (h₂ : HasType b Ty.bool), a.typeCheck = Maybe.found Ty.bool h₁ → b.typeCheck = Maybe.found Ty.bool h₂ → False⊢ Maybe.unknown = Maybe.unknown → ¬HasType (a.and b) ty intro h htty:Tya:Exprb:Expriha:a.typeCheck = Maybe.unknown → ¬HasType a tyihb:b.typeCheck = Maybe.unknown → ¬HasType b tyra:{{ ty | HasType a ty }}rb:{{ ty | HasType b ty }}hnp:∀ (h₁ : HasType a Ty.bool) (h₂ : HasType b Ty.bool), a.typeCheck = Maybe.found Ty.bool h₁ → b.typeCheck = Maybe.found Ty.bool h₂ → Falseh:Maybe.unknown = Maybe.unknownht:HasType (a.and b) ty⊢ False cases ht with | and h₁ h₂ =>ty:Tya:Exprb:Expriha:a.typeCheck = Maybe.unknown → ¬HasType a tyihb:b.typeCheck = Maybe.unknown → ¬HasType b tyra:{{ ty | HasType a ty }}rb:{{ ty | HasType b ty }}hnp:∀ (h₁ : HasType a Ty.bool) (h₂ : HasType b Ty.bool), a.typeCheck = Maybe.found Ty.bool h₁ → b.typeCheck = Maybe.found Ty.bool h₂ → False⊢ Maybe.unknown = Maybe.unknown → ¬HasType (a.and b) ty exact hnp h₁ h₂ (typeCheck_correct h₁ (iha · h₁)) (typeCheck_correct h₂ (ihb · h₂))All goals completed! 🐙

Finally, we show that type checking for e can be decided using Expr.typeCheck.

instance (e : Expr) (t : Ty) : Decidable (HasType e t) := match h' : e.typeCheck with | .found t' ht' => if heq : t = t' then isTrue (heq ▸ ht') else isFalse fun ht => heq (HasType.det ht ht') | .unknown => isFalse (Expr.typeCheck_complete h')