TypesType Systems


Require Export Smallstep.

Hint Constructors multi.

Next topic: type systems
  • This chapter: a toy type system
    • 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)
  • Terms like 5 + true and if 42 then 0 else 1 are stuck.

Syntax

Informally:
    t ::= true
        | false
        | if t then t else t
        | 0
        | succ t
        | pred t
        | iszero t
Formally:

Inductive tm : Type :=
  | ttrue : tm
  | tfalse : tm
  | tif : tm → tm → tm → tm
  | tzero : tm
  | tsucc : tm → tm
  | tpred : tm → tm
  | tiszero : tm → tm.

Values are true, false, and numeric values...

Inductive bvalue : tm → Prop :=
  | bv_true : bvalue ttrue
  | bv_false : bvalue tfalse.

Inductive nvalue : tm → Prop :=
  | nv_zero : nvalue tzero
  | nv_succ : ∀t, nvalue t → nvalue (tsucc t).

Definition value (t:tm) := bvalue t ∨ nvalue t.

Hint Constructors bvalue nvalue.
Hint Unfold value.
Hint Unfold extend.

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_PredZero)  
pred 0 ⇒ 0
numeric value v1 (ST_PredSucc)  
pred (succ v1) ⇒ v1
t1 ⇒ t1' (ST_Pred)  
pred t1 ⇒ pred t1'
   (ST_IszeroZero)  
iszero 0 ⇒ true
numeric value v1 (ST_IszeroSucc)  
iszero (succ v1) ⇒ false
t1 ⇒ t1' (ST_Iszero)  
iszero t1 ⇒ iszero t1'


Notice that the step relation doesn't care about whether expressions make global sense — it just checks that the operation in the next reduction step is being applied to the right kinds of operands.
For example, the term succ true (i.e., tsucc ttrue in the formal syntax) cannot take a step, but the almost as obviously nonsensical term
       succ (if true then true else true) 
can take a step (once, before becoming stuck).

Normal Forms and Values

The first interesting thing about the step relation in this language is that the strong progress theorem from the Smallstep chapter fails! That is, there are terms that are normal forms (they can't take a step) but not values (because we have not included them in our definition of possible "results of evaluation"). 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 former set is included in the latter. 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?
    tiszero (tif ttrue (tsucc tzero) tzero)
(1) Yes
(2) No

What about this one?
    tif (tsucc tzero) ttrue tfalse
(1) Yes
(2) No

What about this one?
    tsucc (tsucc tzero)
(1) Yes
(2) No

Typing

Types describe the possible shapes of values:

Inductive ty : Type :=
  | TBool : ty
  | TNat : ty.

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_Zero)  
⊢ 0 ∈ Nat
⊢ t1 ∈ Nat (T_Succ)  
⊢ succ t1 ∈ Nat
⊢ t1 ∈ Nat (T_Pred)  
⊢ pred t1 ∈ Nat
⊢ t1 ∈ Nat (T_IsZero)  
⊢ iszero t1 ∈ Bool


Examples

Typing is a conservative (static) approximation to behavior.

Example has_type_1 :
  ⊢ tif tfalse tzero (tsucc tzero) ∈ TNat.
Proof.
  apply T_If.
    apply T_False.
    apply T_Zero.
    apply T_Succ.
      apply T_Zero.
Qed.

Example has_type_not :
  ¬ (⊢ tif tfalse tzero ttrue ∈ TBool).
Proof.
  intros Contra. solve by inversion 2. Qed.

Progress

The typing relation enjoys two critical properties. The first is that well-typed normal forms are values (i.e., not stuck).

Theorem progress : ∀t T,
  ⊢ t ∈ T →
  value t ∨ ∃t', t ⇒ t'.

This is more interesting than the strong progress theorem that we saw in the Smallstep chapter, where all normal forms were values. Here, a term can be stuck, but only if it is ill typed.

Type Preservation

The second critical property of typing is that, when a well-typed term takes a step, the result is also a well-typed term.
This theorem is often called the subject reduction property, because it tells us what happens when the "subject" of the typing relation is reduced. This terminology comes from thinking of typing statements as sentences, where the term is the subject and the type is the predicate.

Theorem preservation : ∀t t' T,
  ⊢ t ∈ T →
  t ⇒ t' →
  ⊢ t' ∈ T.

Aside: the normalize Tactic

Proofs that one expression multisteps to another can be tedious...


Example astep_example1 :
  (APlus (ANum 3) (AMult (ANum 3) (ANum 4))) / empty_state
  ⇒a× (ANum 15).
Proof.
  apply multi_step with (APlus (ANum 3) (ANum 12)).
    apply AS_Plus2.
      apply av_num.
      apply AS_Mult.
  apply multi_step with (ANum 15).
    apply AS_Plus.
  apply multi_refl.
Qed.

We repeatedly apply multi_step until we get to a normal form. The proofs that the intermediate steps are possible are simple enough that auto, with appropriate hints, can solve them.

Hint Constructors astep aval.
Example astep_example1' :
  (APlus (ANum 3) (AMult (ANum 3) (ANum 4))) / empty_state
  ⇒a× (ANum 15).
Proof.
  eapply multi_step. auto. simpl.
  eapply multi_step. auto. simpl.
  apply multi_refl.
Qed.

The following custom Tactic Notation definition captures this pattern. In addition, before each multi_step we print out the current goal, so that the user can follow how the term is being evaluated.

Tactic Notation "print_goal" := match goal with ⊢ ?x ⇒ idtac x end.
Tactic Notation "normalize" :=
   repeat (print_goal; eapply multi_step ;
             [ (eauto 10; fail) | (instantiate; simpl)]);
   apply multi_refl.

Example astep_example1'' :
  (APlus (ANum 3) (AMult (ANum 3) (ANum 4))) / empty_state
  ⇒a× (ANum 15).
Proof.
  normalize.
  (* At this point in the proof script, the Coq response shows 
     a trace of how the expression evaluated. 

   (APlus (ANum 3) (AMult (ANum 3) (ANum 4)) / empty_state ==>a* ANum 15)
   (multi (astep empty_state) (APlus (ANum 3) (ANum 12)) (ANum 15))
   (multi (astep empty_state) (ANum 15) (ANum 15))
*)
Qed.

The normalize tactic also provides a simple way to calculate what the normal form of a term is, by proving a goal with an existential variable in it.

Example astep_example1''' : ∃e',
  (APlus (ANum 3) (AMult (ANum 3) (ANum 4))) / empty_state
  ⇒a× e'.
Proof.
  eapply ex_intro. normalize.

(* This time, the trace will be:

    (APlus (ANum 3) (AMult (ANum 3) (ANum 4)) / empty_state ==>a* ??)
    (multi (astep empty_state) (APlus (ANum 3) (ANum 12)) ??)
    (multi (astep empty_state) (ANum 15) ??)

   where ?? is the variable ``guessed'' by eapply.
*)
Qed.

Type Soundness

Putting progress and preservation together, we can 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 ∈ T →
  t ⇒* t' →
  ~(stuck t').
Proof.
  intros t t' T HT P. induction P; intros [R S].
  destruct (progress x T HT); auto.
  apply IHP. apply (preservation x y T HT H).
  unfold stuck. split; auto. Qed.

Additional Exercises


Suppose we add the following two new rules to the reduction relation:
      | ST_PredTrue : 
           (tpred ttrue) ⇒ (tpred tfalse)
      | ST_PredFalse : 
           (tpred tfalse) ⇒ (tpred ttrue)
Which of the following properties remain true in the presence of these rules? (Press 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 ∈ TNat →
           ⊢ tif ttrue t2 t3 ∈ TNat
Which of the following properties remain true in the presence of these rules?
  • Determinism of step
  • Progress
  • Preservation