Case Study: Building a Typed Mini Language

Write a grammar, typing rules, and an evaluator, run programs written as text, and prove type safety.

19a.1 The language, and what you write

In this chapter we build a small typed expression language with only numbers, booleans, +, ==, and if.

1 + 2 + 3                        -- 6 : Nat
if 1 + 1 == 2 then 10 else 20    -- 10 : Nat
1 + true                         -- type error

Of the parts of an interpreter, Tauto's macros make the lexer, the parser, and the type checker. A person writes three things.

What you write	Feature	What it gives	Section
The grammar	`inductive_syntax!`	the parser `tl::parse` and a syntax tree that proofs can see	19a.2
The typing rules	an `inductive` relation and `@mode!`	the type checker `check`	19a.3
A proof of type safety	`theorem`	the guarantee that a well-typed program does not fail at run time	19a.7

The rest, the evaluator (19a.4) and the function that turns the syntax tree into the core language (19a.5), are ordinary functions. The whole flow is:

text --tl::parse--> tl::Expr --to_i--> tl::Expr::I --lower_expr--> Term --check_ty--> Option(Ty)
                                                                   Term --eval------> Option(Val)

The code is a tote (chapter 12) with its files in src/, connected by import. The repository's examples/typed-lang/ is a complete example with the same structure (with a REPL that reads one expression per line).

19a.2 Writing the grammar

The grammar goes in inductive_syntax!. It is written the same way as the syntax! grammar of chapter 17a.

src/syntax.taut

import std::Text { Text }

// One grammar gives the reader `tl::parse` and the tree `tl::Expr::I` that proofs can see.
inductive_syntax!(tl, ```par
%start Expr
%title "typed-lang"
%%
Expr: IfExpr | Cmp;
IfExpr: KwIf Expr KwThen Expr KwElse Expr;
Cmp: Sum [ EqEq Sum ];
Sum: Atom { Plus Atom };
Atom: Num | KwTrue | KwFalse | Paren;
Paren: LParen Expr RParen;
Num: /[0-9]+/;
Plus: '+';
EqEq: '==';
KwIf: 'if';
KwThen: 'then';
KwElse: 'else';
KwTrue: 'true';
KwFalse: 'false';
LParen: '(';
RParen: ')';
```) =>
  enum Atom, struct Cmp, struct Cmp_Opt1, enum Expr, struct IfExpr, struct Paren, struct Sum,
  struct Sum_Rep1, fn parse, inductive Atom::I, inductive Cmp::I, inductive Cmp_Opt1::I,
  inductive Expr::I, inductive IfExpr::I, inductive Paren::I, inductive Sum::I,
  inductive Sum_Rep1::I, fn Atom::to_i, fn Cmp::to_i, fn Cmp_Opt1::to_i, fn Expr::to_i,
  fn IfExpr::to_i, fn Paren::to_i, fn Sum::to_i, fn Sum_Rep1::to_i, fn Cmp_Opt1_opt::to_i,
  fn Sum_Rep1_list::to_i

✓ Check passed

The rules come after %%. Strings such as '+' and regular expressions such as /[0-9]+/ become tokens, and spaces are skipped. In Sum: Atom { Plus Atom };, { … } repeats zero or more times; in Cmp: Sum [ EqEq Sum ];, [ … ] is optional. Both sides of + are Atoms, so 1 + 1 == 2 reads as (1 + 1) == 2.

This declaration makes two sets of types and functions.

tl::Expr, tl::Sum, and so on: the syntax tree that tl::parse builds from text. Text that does not fit the grammar is an Err that says what was expected.
tl::Expr::I, tl::Sum::I, and so on: the inductive version of the same tree. The kernel can read these types, so proofs can use them. tl::Expr::to_i turns the first into the second.

=> … is the complete list of the declarations it makes; a missing or extra name is an error. After changing the grammar, tauto syntax gen regenerates the parser's tables.

19a.3 Write the typing rules, get a checker

The syntax tree has the shape of the grammar, with the repetitions of Sum and the parentheses. Type checking and evaluation use a smaller core language, Term.

src/core.taut

import std::Mode { mode }

// The core of the typed language: the form the type checker and the evaluator read, not the tree.

pub(open) inductive Ty: Type {
  TNat: Ty
  TBool: Ty
}

pub(open) inductive Term: Type {
  TmNum(n: Nat): Term
  TmBool(b: Bool): Term
  TmAdd(a: Term, b: Term): Term
  TmEq(a: Term, b: Term): Term
  TmIf(c: Term, t: Term, e: Term): Term
}

pub(open) inductive TyDecision(a: Ty, b: Ty): Type {
  TySame(e: a = b): TyDecision(a, b)
  TyDifferent(refute: (a = b) -> False): TyDecision(a, b)
}

pub fn ty_dec(a: Ty, b: Ty): TyDecision(a, b) {
  match a: TyDecision(a, b) {
    TNat => match b: TyDecision(TNat, b) {
      TNat => TySame(Refl)
      TBool => TyDifferent(e => match e: False {})
    }
    TBool => match b: TyDecision(TBool, b) {
      TNat => TyDifferent(e => match e: False {})
      TBool => TySame(Refl)
    }
  }
}

// The relation below is the only specification a person reads. `mode!` makes the checker from its rules.
@mode!(`check(rec term, out ty) -> Check { Accepted | Rejected } eq Ty: ty_dec { TySame | TyDifferent }`) => inductive Check, fn check
pub(open) inductive HasTy: (Term, Ty) -> Prop {
  TyNum<n: Nat>: HasTy(TmNum(n), TNat)
  TyBool<b: Bool>: HasTy(TmBool(b), TBool)
  TyAdd<a: Term, b: Term>(ha: HasTy(a, TNat), hb: HasTy(b, TNat)): HasTy(TmAdd(a, b), TNat)
  TyEq<a: Term, b: Term>(ha: HasTy(a, TNat), hb: HasTy(b, TNat)): HasTy(TmEq(a, b), TBool)
  TyIf<c: Term, t: Term, e: Term, ty: Ty>(
    hc: HasTy(c, TBool),
    ht: HasTy(t, ty),
    he: HasTy(e, ty)
  ): HasTy(TmIf(c, t, e), ty)
}

Execution result

✓ def ty_dec : ∀ a: Ty. ∀ b: Ty. TyDecision(a, b)

Ty is a type and Term an expression of the core language. HasTy(t, ty) is the relation "the expression t has the type ty", and each constructor is a typing rule. TyAdd, for example, reads "if a and b are Nat, TmAdd(a, b) is Nat". TyIf asks for a Bool condition and two branches of the same type ty.

@mode! makes the type checker check from these rules.

check(rec term, out ty) says: recurse on the first argument of HasTy (the expression) as the input, and find the second (the type) as the output.
Whether the two branches of TyIf have the same type is decided with eq Ty: ty_dec. ty_dec returns a proof that they are equal (TySame) or a proof that they are not (TyDifferent).
The answer of check(t), a Check(t), carries the type, the derivation of HasTy, and the uniqueness of the type when it accepts (Accepted), and a refutation that no type fits when it rejects (Rejected).

You do not write a checker by hand and prove afterwards that it agrees with the rules. The rules give a checker that comes with the evidence that it is right.

19a.4 The evaluator

Values are Val. The evaluator eval, in its own file src/eval.taut, is a recursion that follows the shape of Term.

src/eval.taut

import "core.taut" { Term }
import std::Base { Nat }

pub(open) inductive Val: Type {
  VNat(n: Nat): Val
  VBool(b: Bool): Val
}

// The evaluator. An operation on values of the wrong type is `None` (a type error at run time).
pub fn add_val(x: Option(Val), y: Option(Val)): Option(Val) {
  match x: Option(Val) {
    None => None
    Some(vx) => match vx: Option(Val) {
      VBool(xb) => None
      VNat(nx) => match y: Option(Val) {
        None => None
        Some(vy) => match vy: Option(Val) {
          VBool(yb) => None
          VNat(ny) => Some(VNat(Nat::add(nx, ny)))
        }
      }
    }
  }
}

pub fn eq_val(x: Option(Val), y: Option(Val)): Option(Val) {
  match x: Option(Val) {
    None => None
    Some(vx) => match vx: Option(Val) {
      VBool(xb) => None
      VNat(nx) => match y: Option(Val) {
        None => None
        Some(vy) => match vy: Option(Val) {
          VBool(yb) => None
          VNat(ny) => Some(VBool(Nat::eq(nx, ny)))
        }
      }
    }
  }
}

pub fn if_val(c: Option(Val), t: Option(Val), e: Option(Val)): Option(Val) {
  match c: Option(Val) {
    None => None
    Some(vc) => match vc: Option(Val) {
      VNat(n) => None
      VBool(b) => match b: Option(Val) {
        true => t
        false => e
      }
    }
  }
}

pub fn eval(t: Term): Option(Val) {
  match t: Option(Val) {
    TmNum(n) => Some(VNat(n))
    TmBool(b) => Some(VBool(b))
    TmAdd(a, b) => add_val(eval(a), eval(b))
    TmEq(a, b) => eq_val(eval(a), eval(b))
    TmIf(c, t1, e) => if_val(eval(c), eval(t1), eval(e))
  }
}

Execution result

✓ def add_val : (Option(Val)) -> (Option(Val)) -> Option(Val)
✓ def eq_val : (Option(Val)) -> (Option(Val)) -> Option(Val)
✓ def if_val : (Option(Val)) -> (Option(Val)) -> (Option(Val)) -> Option(Val)
✓ def eval : (Term) -> Option(Val)

The evaluator does not look at types. For an expression such as TmAdd(TmNum(1), TmBool(true)), add_val returns None (a type error at run time). eval is structurally recursive, so it is a total function with no Div.

19a.5 From the syntax tree to the core language

lower_expr turns the inductive syntax tree tl::Expr::I into a Term.

src/lower.taut

import "core.taut" { Term }
import "syntax.taut" { tl }
import std::Base { Nat }
import std::Text { Text }

// Turn the tree (`tl::Expr::I`) into the core `Term`. These are ordinary total functions; they do not look at types.

pub fn num_of(t: Text): Nat {
  digits(Text::bytes(t), 0)
}

pub fn digits(bs: List(Nat), acc: Nat): Nat {
  match bs: Nat {
    Nil => acc
    Cons(b, rest) => digits(rest, Nat::add(Nat::mul(acc, 10), Nat::sub(b, 48)))
  }
}

mutual {
  pub fn lower_expr(e: tl::Expr::I): Term {
    match e: Term {
      IfExpr_I(i) => lower_if(i)
      Cmp_I(c) => lower_cmp(c)
    }
  }
  pub fn lower_if(i: tl::IfExpr::I): Term {
    match i: Term {
      Mk(k1, c, k2, t, k3, e) => TmIf(lower_expr(c), lower_expr(t), lower_expr(e))
    }
  }
  pub fn lower_cmp(c: tl::Cmp::I): Term {
    match c: Term {
      Mk(sum, opt) => lower_cmp_opt(lower_sum(sum), opt)
    }
  }
  pub fn lower_cmp_opt(lhs: Term, o: Option(tl::Cmp_Opt1::I)): Term {
    match o: Term {
      None => lhs
      Some(r) => lower_cmp_rhs(lhs, r)
    }
  }
  pub fn lower_cmp_rhs(lhs: Term, r: tl::Cmp_Opt1::I): Term {
    match r: Term {
      Mk(op, rhs) => TmEq(lhs, lower_sum(rhs))
    }
  }
  pub fn lower_sum(s: tl::Sum::I): Term {
    match s: Term {
      Mk(atom, rep) => lower_rep(lower_atom(atom), rep)
    }
  }
  pub fn lower_rep(acc: Term, rep: List(tl::Sum_Rep1::I)): Term {
    match rep: Term {
      Nil => acc
      Cons(r, more) => lower_rep(lower_rep_step(acc, r), more)
    }
  }
  pub fn lower_rep_step(acc: Term, r: tl::Sum_Rep1::I): Term {
    match r: Term {
      Mk(op, atom) => TmAdd(acc, lower_atom(atom))
    }
  }
  pub fn lower_atom(a: tl::Atom::I): Term {
    match a: Term {
      Num_I(t) => TmNum(num_of(t))
      KwTrue_I(t) => TmBool(true)
      KwFalse_I(t) => TmBool(false)
      Paren_I(p) => lower_paren(p)
    }
  }
  pub fn lower_paren(p: tl::Paren::I): Term {
    match p: Term {
      Mk(l, e, r) => lower_expr(e)
    }
  }
}

✓ Check passed

✓ def digits : (List(Nat)) -> (Nat) -> Nat
✓ def num_of : (Text) -> Nat
✓ def lower_expr : (tl::Expr::I) -> Term
✓ def lower_if : (tl::IfExpr::I) -> Term
✓ def lower_cmp : (tl::Cmp::I) -> Term
✓ def lower_cmp_opt : (Term) -> (Option(tl::Cmp_Opt1::I)) -> Term
✓ def lower_cmp_rhs : (Term) -> (tl::Cmp_Opt1::I) -> Term
✓ def lower_sum : (tl::Sum::I) -> Term
✓ def lower_rep : (Term) -> (List(tl::Sum_Rep1::I)) -> Term
✓ def lower_rep_step : (Term) -> (tl::Sum_Rep1::I) -> Term
✓ def lower_atom : (tl::Atom::I) -> Term
✓ def lower_paren : (tl::Paren::I) -> Term

The repetition in tl::Sum::I (Atom { Plus Atom }) is folded into TmAdd from the left by lower_rep. Functions that call each other go in mutual { … }. A run of digits becomes a Nat from the bytes that Text::bytes reads.

19a.6 Putting it together

We write check_ty, which turns the answer of check into an Option(Ty), and run_term, which evaluates only what passed the checker.

src/pipeline.taut

import "core.taut" { Check, Term, Ty, check }
import "eval.taut" { Val, eval }
import "lower.taut" { lower_expr }
import "syntax.taut" { tl }

pub fn decision_ty(t: Term, d: Check(t)): Option(Ty) {
  match d: Option(Ty) {
    Accepted(ty, derivation, unique) => Some(ty)
    Rejected(refute) => None
  }
}

// The type checker: the answer of `check`, made by `mode!`, as an `Option` of a type.
pub fn check_ty(t: Term): Option(Ty) {
  decision_ty(t, check(t))
}

// Evaluate only what passed the checker.
pub fn run_if_typed(r: Option(Ty), t: Term): Option(Val) {
  match r: Option(Val) {
    None => None
    Some(ty) => eval(t)
  }
}

pub fn run_term(t: Term): Option(Val) {
  run_if_typed(check_ty(t), t)
}

pub fn run_tree(e: tl::Expr::I): Option(Val) {
  run_term(lower_expr(e))
}

✓ Check passed

✓ def decision_ty : ∀ t: Term. (Check(t)) -> Option(Ty)
✓ def check_ty : (Term) -> Option(Ty)
✓ def run_if_typed : (Option(Ty)) -> (Term) -> Option(Val)
✓ def run_term : (Term) -> Option(Val)
✓ def run_tree : (tl::Expr::I) -> Option(Val)

Check(t) is a type that depends on the expression t. decision_ty takes the type out when it accepts, and returns None when it rejects.

Now connect text to results, and run it.

src/main.taut

import "core.taut" { Ty }
import "eval.taut" { Val, eval }
import "lower.taut" { lower_expr }
import "pipeline.taut" { check_ty }
import "syntax.taut" { tl }
import std::prelude::Shared { concat }

fn show_ty(ty: Ty): Text {
  match ty {
    TNat => "Nat"
    TBool => "Bool"
  }
}

fn show_val(v: Option(Val)): Text {
  match v {
    None => "stuck"
    Some(x) => match x {
      VNat(n) => Text::of_nat(n)
      VBool(b) => if b { "true" } else { "false" }
    }
  }
}

fn run_text(src: Text): Text ! {Div} {
  match tl::parse(src) {
    Err(d) => concat("syntax error: ", d.message)
    Ok(tree) => {
      let t := lower_expr(tl::Expr::to_i(tree))
      match check_ty(t) {
        None => "type error"
        Some(ty) => concat(show_val(eval(t)), concat(" : ", show_ty(ty)))
      }
    }
  }
}

perform show("a", run_text("1 + 2 + 3"))
perform show("b", run_text("if 1 + 1 == 2 then 10 else 20"))
perform show("c", run_text("1 + true"))
perform show("d", run_text("if true then 1 else false"))
perform show("e", run_text("1 + * 2"))

Execution result

✓ def show_ty : (Ty) -> Text
・ show_val
・ run_text

a = "6 : Nat"
b = "10 : Nat"
c = "type error"
d = "type error"
e = "syntax error: macro.syntax_error: in tl: expected Num or KwTrue or KwFalse or LParen, found Error"

a = "6 : Nat"
b = "10 : Nat"
c = "type error"
d = "type error"
e = "syntax error: macro.syntax_error: in tl: expected Num or KwTrue or KwFalse or LParen, found Error"

The type checker stops 1 + true and if true then 1 else false, so they never reach the evaluator. For 1 + * 2, the parser made from the grammar reports the tokens it expected.

19a.7 Proving type safety

We prove that an expression that passed the type checker never hits a type error at run time. First, a relation that says the result of evaluation fits a type.

src/safety.taut

import "core.taut" { HasTy, Term, Ty }
import "eval.taut" { Val, add_val, eq_val, eval, if_val }

// The relation "a value has a type".
pub(open) inductive ValHas: (Val, Ty) -> Prop {
  HNat<n: Nat>: ValHas(VNat(n), TNat)
  HBool<b: Bool>: ValHas(VBool(b), TBool)
}

// Evidence that evaluation succeeded and returned a value of the promised type. No such evidence exists for `None`.
pub(open) inductive ResultHas: (Option(Val), Ty) -> Prop {
  Returned<v: Val, ty: Ty>(h: ValHas(v, ty)): ResultHas(Some(v), ty)
}

pub theorem add_safe<x: Option(
  Val
), y: Option(Val)>(hx: ResultHas(x, TNat), hy: ResultHas(y, TNat)): ResultHas(add_val(x, y), TNat) {
  match hx: ResultHas(add_val(x, y), TNat) {
    Returned(vx, tx, hvx) => ⊢ ResultHas(add_val(Some(vx), y), TNat) from match hvx: ResultHas(add_val(Some(vx), y), TNat) {
      HNat(nx) => ⊢ ResultHas(add_val(Some(VNat(nx)), y), TNat) from match hy: ResultHas(add_val(Some(VNat(nx)), y), TNat) {
        Returned(vy, ty, hvy) => ⊢ ResultHas(add_val(Some(VNat(nx)), Some(vy)), TNat) from match hvy: ResultHas(add_val(Some(VNat(nx)), Some(vy)), TNat) {
          HNat(ny) => ⊢ ResultHas(add_val(Some(VNat(nx)), Some(VNat(ny))), TNat) from Returned(HNat)
        }
      }
    }
  }
}

pub theorem eq_safe<x: Option(
  Val
), y: Option(Val)>(hx: ResultHas(x, TNat), hy: ResultHas(y, TNat)): ResultHas(eq_val(x, y), TBool) {
  match hx: ResultHas(eq_val(x, y), TBool) {
    Returned(vx, tx, hvx) => ⊢ ResultHas(eq_val(Some(vx), y), TBool) from match hvx: ResultHas(eq_val(Some(vx), y), TBool) {
      HNat(nx) => ⊢ ResultHas(eq_val(Some(VNat(nx)), y), TBool) from match hy: ResultHas(eq_val(Some(VNat(nx)), y), TBool) {
        Returned(vy, ty, hvy) => ⊢ ResultHas(eq_val(Some(VNat(nx)), Some(vy)), TBool) from match hvy: ResultHas(eq_val(Some(VNat(nx)), Some(vy)), TBool) {
          HNat(ny) => ⊢ ResultHas(eq_val(Some(VNat(nx)), Some(VNat(ny))), TBool) from Returned(HBool)
        }
      }
    }
  }
}

pub theorem if_safe<c: Option(
  Val
), t: Option(
  Val
), e: Option(
  Val
), ty: Ty>(
  hc: ResultHas(c, TBool),
  ht: ResultHas(t, ty),
  he: ResultHas(e, ty)
): ResultHas(if_val(c, t, e), ty) {
  match hc: ResultHas(if_val(c, t, e), ty) {
    Returned(vc, tc, hvc) => ⊢ ResultHas(if_val(Some(vc), t, e), ty) from match hvc: ResultHas(if_val(Some(vc), t, e), ty) {
      HBool(b) => ⊢ ResultHas(if_val(Some(VBool(b)), t, e), ty) from match b: ResultHas(if_val(Some(VBool(b)), t, e), ty) {
        true => ht
        false => he
      }
    }
  }
}

// Type safety: evaluating a well-typed expression always returns a value, and the value has the expression's type.
pub theorem eval_safe<t: Term, ty: Ty>(h: HasTy(t, ty)): ResultHas(eval(t), ty) {
  match h: ResultHas(eval(t), ty) {
    TyNum(n) => Returned(HNat)
    TyBool(b) => Returned(HBool)
    TyAdd(a, b, ha, hb) => add_safe(eval_safe(ha), eval_safe(hb))
    TyEq(a, b, ha, hb) => eq_safe(eval_safe(ha), eval_safe(hb))
    TyIf(c, t1, e, ty1, hc, ht, he) => if_safe(eval_safe(hc), eval_safe(ht), eval_safe(he))
  }
}

Execution result

✓ theorem add_safe : ∀ x: Option(Val). ∀ y: Option(Val). (ResultHas(x, Ty::TNat)) -> (ResultHas(y, Ty::TNat)) -> ResultHas(add_val(x, y), Ty::TNat)
✓ theorem eq_safe : ∀ x: Option(Val). ∀ y: Option(Val). (ResultHas(x, Ty::TNat)) -> (ResultHas(y, Ty::TNat)) -> ResultHas(eq_val(x, y), Ty::TBool)
✓ theorem if_safe : ∀ c: Option(Val). ∀ t: Option(Val). ∀ e: Option(Val). ∀ ty: Ty. (ResultHas(c, Ty::TBool)) -> (ResultHas(t, ty)) -> (ResultHas(e, ty)) -> ResultHas(if_val(c, t, e), ty)
✓ theorem eval_safe : ∀ t: Term. ∀ ty: Ty. (HasTy(t, ty)) -> ResultHas(eval(t), ty)

Returned is the only constructor of ResultHas(r, ty), so there is no such evidence for None. add_safe, eq_safe, and if_safe show, one operation at a time, that results fit the type when the arguments do. eval_safe is induction on the derivation of HasTy: each typing rule is closed with the matching lemma (chapter 15).

Next, we show that the checker agrees with the rules.

src/checker.taut

import "core.taut" { Check, HasTy, Term, Ty, check }
import "pipeline.taut" { check_ty, decision_ty, run_if_typed, run_term }
import "safety.taut" { ResultHas, eval_safe }

// Soundness of the checker: when it answers `Some(ty)`, `t : ty` holds.
pub theorem decision_sound<t: Term, ty: Ty>(
  d: Check(t),
  said: Eq(Option(Ty), decision_ty(t, d), Some(ty))
): HasTy(t, ty) {
  match d: HasTy(t, ty) {
    Accepted(out, derivation, unique) => match said: HasTy(t, ty) {
      Refl => derivation
    }
    Rejected(refute) => match said: HasTy(t, ty) {}
  }
}

pub theorem check_sound<t: Term, ty: Ty>(
  said: Eq(Option(Ty), check_ty(t), Some(ty))
): HasTy(t, ty) {
  decision_sound(check(t), said)
}

// Completeness of the checker: when `t : ty` holds, it answers `Some(ty)`.
pub theorem decision_complete<t: Term, ty: Ty>(
  d: Check(t),
  h: HasTy(t, ty)
): Eq(Option(Ty), decision_ty(t, d), Some(ty)) {
  match d: Eq(Option(Ty), decision_ty(t, d), Some(ty)) {
    Accepted(out, derivation, unique) => Eq::congr(Some, Eq::sym(unique(ty, h)))
    Rejected(refute) => False::elim(refute(ty, h))
  }
}

pub theorem check_complete<t: Term, ty: Ty>(
  h: HasTy(t, ty)
): Eq(Option(Ty), check_ty(t), Some(ty)) {
  decision_complete(check(t), h)
}

// Running after the checker returns a value of the right type.
pub theorem run_term_safe<t: Term, ty: Ty>(h: HasTy(t, ty)): ResultHas(run_term(t), ty) {
  Eq::subst(
    (r: Option(Ty)) => ResultHas(run_if_typed(r, t), ty),
    Eq::sym(check_complete(h)),
    eval_safe(h)
  )
}

✓ Check passed

✓ theorem decision_sound : ∀ t: Term. ∀ ty: Ty. ∀ d: Check(t). (decision_ty(t, d) = Option::Some(Ty, ty)) -> HasTy(t, ty)
✓ theorem check_sound : ∀ t: Term. ∀ ty: Ty. (check_ty(t) = Option::Some(Ty, ty)) -> HasTy(t, ty)
✓ theorem decision_complete : ∀ t: Term. ∀ ty: Ty. ∀ d: Check(t). (HasTy(t, ty)) -> decision_ty(t, d) = Option::Some(Ty, ty)
✓ theorem check_complete : ∀ t: Term. ∀ ty: Ty. (HasTy(t, ty)) -> check_ty(t) = Option::Some(Ty, ty)
✓ theorem run_term_safe : ∀ t: Term. ∀ ty: Ty. (HasTy(t, ty)) -> ResultHas(run_term(t), ty)

check_sound says "when the checker answers Some(ty), t : ty", and check_complete says the converse. Both only take out the derivation, the uniqueness, or the refutation that @mode! put in Check; the case analysis of the rules is not written again. run_term_safe combines them: running a well-typed expression with run_term returns a value that fits its type.

Finally, we check concrete expressions by computation.

src/examples.taut

import "core.taut" { Term }
import "eval.taut" { Val }
import "pipeline.taut" { check_ty, run_term }

// Concrete expressions are checked by computation (`Refl`).
theorem sum3_runs(): run_term(TmAdd(TmAdd(TmNum(1), TmNum(2)), TmNum(3))) = Some(VNat(6)) { Refl }
theorem add_bool_rejected(): check_ty(TmAdd(TmNum(1), TmBool(true))) = None { Refl }

✓ Check passed

✓ theorem sum3_runs : run_term(Term::TmAdd(Term::TmAdd(Term::TmNum(1), Term::TmNum(2)), Term::TmNum(3))) = Option::Some(Val, Val::VNat(6))
✓ theorem add_bool_rejected : check_ty(Term::TmAdd(Term::TmNum(1), Term::TmBool(true))) = Option::None(Ty)

These proofs use no axioms.

19a.8 What is not guaranteed

tl::parse and tl::Expr::to_i are code generated from tables to run, and they are outside the proofs. So it is not proved that a text means a given tree. run_term_safe holds for every Term that lower_expr makes. The evaluator treats Nat as the mathematical natural numbers and does not deal with the limits of how numbers are represented at run time (chapter 20).

Exercise 19a.1: To add *, what must change in the grammar, Term, HasTy, eval, lower_expr, and the proofs?

Exercise 19a.2: If TyIf no longer required the two branches to have the same type, where in eval_safe would the proof stop going through?