TypesType Systems

New topic: type systems
  • This chapter: a toy type system for a toy language
    • typing relation
    • progress and preservation theorems
  • Next chapter: simply typed lambda-calculus

Typed Arithmetic Expressions

  • A simple toy language where expressions may fail with dynamic type errors
    • numbers (and arithmetic)
    • booleans (and conditionals)
  • Unlike Imp, we use a single syntactic category for both booleans and numbers
  • This means we can write stuck terms like 5 + true and if 42 then 0 else 1.

Syntax

Here is the syntax, informally:
    t ::= true
        | false
        | if t then t else t
        | 0
        | succ t
        | pred t
        | iszero t

Values are true, false, and numeric values...
Inductive bvalue : tm → Prop :=
  | bv_true : bvalue <{ true }>
  | bv_false : bvalue <{ false }>.
Inductive nvalue : tm → Prop :=
  | nv_0 : nvalue <{ 0 }>
  | nv_succ : ∀ t, nvalue t → nvalue <{ succ t }>.
Definition value (t : tm) := bvalue t ∨ nvalue t.

Operational Semantics

   (ST_IfTrue)  
if true then t1 else t2 --> t1
   (ST_IfFalse)  
if false then t1 else t2 --> t2
t1 --> t1' (ST_If)  
if t1 then t2 else t3 --> if t1' then t2 else t3
t1 --> t1' (ST_Succ)  
succ t1 --> succ t1'
   (ST_Pred0)  
pred 0 --> 0
numeric value v (ST_PredSucc)  
pred (succ v) --> v
t1 --> t1' (ST_Pred)  
pred t1 --> pred t1'
   (ST_IsZero0)  
iszero 0 --> true
numeric value v (ST_IszeroSucc)  
iszero (succ v) --> false
t1 --> t1' (ST_Iszero)  
iszero t1 --> iszero t1'
Inductive step : tm → tm → Prop :=
  | ST_IfTrue : ∀ t1 t2,
      <{ if true then t1 else t2 }> --> t1
  | ST_IfFalse : ∀ t1 t2,
      <{ if false then t1 else t2 }> --> t2
  | ST_If : ∀ c c' t2 t3,
      c --> c' →
      <{ if c then t2 else t3 }> --> <{ if c' then t2 else t3 }>
  | ST_Succ : ∀ t1 t1',
      t1 --> t1' →
      <{ succ t1 }> --> <{ succ t1' }>
  | ST_Pred0 :
      <{ pred 0 }> --> <{ 0 }>
  | ST_PredSucc : ∀ v,
      nvalue v →
      <{ pred (succ v) }> --> v
  | ST_Pred : ∀ t1 t1',
      t1 --> t1' →
      <{ pred t1 }> --> <{ pred t1' }>
  | ST_Iszero0 :
      <{ iszero 0 }> --> <{ true }>
  | ST_IszeroSucc : ∀ v,
       nvalue v →
      <{ iszero (succ v) }> --> <{ false }>
  | ST_Iszero : ∀ t1 t1',
      t1 --> t1' →
      <{ iszero t1 }> --> <{ iszero t1' }>

where "t '-->' t'" := (step t t').
Hint Constructors step : core.
(* /HIDEFROMHTML *)

Normal Forms and Values

The first interesting thing to notice about this step relation is that the strong progress theorem from the Smallstep chapter fails here. That is, there are terms that are normal forms (they can't take a step) but not values (they are not included in our definition of possible "results of reduction").
Such terms are stuck.
Notation step_normal_form := (normal_form step).
Definition stuck (t : tm) : Prop :=
  step_normal_form t ∧ ¬value t.

However, although values and normal forms are not the same in this language, the set of values is a subset of the set of normal forms.
This is important because it shows we did not accidentally define things so that some value could still take a step.
Lemma value_is_nf : ∀ t,
  value t → step_normal_form t.
Proof.
  (* FILL IN HERE *) Admitted.

Is the following term stuck?
    iszero (if true then (succ 0) else 0)
(1) Yes
(2) No
What about this one?
    if (succ 0) then true else false
(1) Yes
(2) No
What about this one?
    succ (succ 0)
(1) Yes
(2) No
What about this one?
    succ (if true then true else true)
(1) Yes
(2) No
(Hint: Notice that the step relation doesn't care about whether the expression being stepped makes global sense -- it just checks that the operation in the next reduction step is being applied to the right kinds of operands.)

Typing

Types describe the possible shapes of values:
Inductive ty : Type :=
  | Bool : ty
  | Nat : ty.

Typing Relations

The typing relation |-- t ∈ T relates terms to the types of their results:
   (T_True)  
|-- true ∈ Bool
   (T_False)  
|-- false ∈ Bool
|-- t1 ∈ Bool    |-- t2 ∈ T    |-- t3 ∈ T (T_If)  
|-- if t1 then t2 else t3 ∈ T
   (T_0)  
|-- 0 ∈ Nat
|-- t1 ∈ Nat (T_Succ)  
|-- succ t1 ∈ Nat
|-- t1 ∈ Nat (T_Pred)  
|-- pred t1 ∈ Nat
|-- t1 ∈ Nat (T_Iszero)  
|-- iszero t1 ∈ Bool
Inductive has_type : tm → ty → Prop :=
  | T_True :
       |-- <{ true }> \in Bool
  | T_False :
       |-- <{ false }> \in Bool
  | T_If : ∀ t1 t2 t3 T,
       |-- t1 \in Bool →
       |-- t2 \in T →
       |-- t3 \in T →
       |-- <{ if t1 then t2 else t3 }> \in T
  | T_0 :
       |-- <{ 0 }> \in Nat
  | T_Succ : ∀ t1,
       |-- t1 \in Nat →
       |-- <{ succ t1 }> \in Nat
  | T_Pred : ∀ t1,
       |-- t1 \in Nat →
       |-- <{ pred t1 }> \in Nat
  | T_Iszero : ∀ t1,
       |-- t1 \in Nat →
       |-- <{ iszero t1 }> \in Bool

where "'|--' t '∈' T" := (has_type t T).
Hint Constructors has_type : core.
(* /HIDEFROMHTML *)

Example has_type_1 :
  |-- <{ if false then 0 else (succ 0) }> \in Nat.
Proof.
  apply T_If.
  - apply T_False.
  - apply T_0.
  - apply T_Succ. apply T_0.
Qed.

Typing is a conservative (static) approximation to behavior.
In particular, a term can be ill typed even though it steps to something well typed.
Example has_type_not :
  ¬( |-- <{ if false then 0 else true}> \in Bool ).
Proof.
  intros Contra. solve_by_inverts 2. Qed.

Canonical forms

The following two lemmas capture the fundamental fact that the definitions of boolean and numeric values agree with the typing relation.
Lemma bool_canonical : ∀ t,
  |-- t \in Bool → value t → bvalue t.
Proof.
  intros t HT [Hb | Hn].
  - assumption.
  - destruct Hn as [ | Hs].
    + inversion HT.
    + inversion HT.
Qed.

Lemma nat_canonical : ∀ t,
  |-- t \in Nat → value t → nvalue t.
Proof.
  intros t HT [Hb | Hn].
  - inversion Hb; subst; inversion HT.
  - assumption.
Qed.

Progress

The typing relation enjoys two critical properties.
The first is that well-typed normal forms are not stuck -- or conversely, if a term is well typed, then either it is a value or it can take at least one step. We call this progress.
Theorem progress : ∀ t T,
  |-- t \in T →
  value t ∨ ∃ t', t --> t'.
Proof.
  intros t T HT.
  induction HT; auto.
  (* The cases that were obviously values, like T_True and
     T_False, are eliminated immediately by auto *)
  - (* T_If *)
    right. destruct IHHT1.
    + (* t1 is a value *)
    apply (bool_canonical t1 HT1) in H.
    destruct H.
      × ∃ t2. auto.
      × ∃ t3. auto.
    + (* t1 can take a step *)
      destruct H as [t1' H1].
      ∃ (<{ if t1' then t2 else t3 }>). auto.
  (* FILL IN HERE *) Admitted.

What is the relation between the progress property defined here and the strong progress from SmallStep?
(1) No difference
(2) Progress implies strong progress
(3) Strong progress implies progress
(4) They are unrelated properties
(5) Dunno
Quick review:
In the language defined at the start of this chapter...
  • Every well-typed normal form is a value.
(1) True
(2) False
In this language...
  • Every value is a normal form.
(1) True
(2) False
In this language...
  • The single-step reduction relation is a partial function (i.e., it is deterministic).
(1) True
(2) False
In this language...
  • The single-step reduction relation is a total function.
(1) True
(2) False

Type Preservation

The second critical property of typing is that, when a well-typed term takes a step, the result is a well-typed term (of the same type).
Theorem preservation : ∀ t t' T,
  |-- t \in T →
  t --> t' →
  |-- t' \in T.

Type Soundness

Putting progress and preservation together, we see that a well-typed term can never reach a stuck state.
Definition multistep := (multi step).
Notation "t1 '-->*' t2" := (multistep t1 t2) (at level 40).
Corollary soundness : ∀ t t' T,
  |-- t \in T →
  t -->* t' →
  ~(stuck t').
Proof.
  intros t t' T HT P. induction P; intros [R S].
  - apply progress in HT. destruct HT; auto.
  - apply IHP.
    + apply preservation with (t := x); auto.
    + unfold stuck. split; auto.
Qed.

Suppose we add the following two new rules to the reduction relation:
      | ST_PredTrue :
           pred true --> pred false
      | ST_PredFalse :
           pred false --> pred true Which of the following properties remain true in the presence of these rules? (Choose 1 for yes, 2 for no.)
  • Determinism of step
  • Progress
  • Preservation
Suppose, instead, that we add this new rule to the typing relation:
      | T_IfFunny : ∀ t2 t3,
           |-- t2 \in Nat →
           |-- <{ if true then t2 else t3 }> \in Nat Which of the following properties remain true in the presence of these rules?
  • Determinism of step
  • Progress
  • Preservation