TypesType Systems

New 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

Here is the syntax, informally:
    t ::= tru
        | fls
        | test t then t else t
        | zro
        | scc t
        | prd t
        | iszro t And here it is formally:
Inductive tm : Type :=
  | tru : tm
  | fls : tm
  | test : tm → tm → tm → tm
  | zro : tm
  | scc : tm → tm
  | prd : tm → tm
  | iszro : tm → tm.
(Since it is so simple, we will not bother introducing custom concrete syntax for this language.)

Values are tru, fls, and numeric values...
Inductive bvalue : tm → Prop :=
  | bv_tru : bvalue tru
  | bv_fls : bvalue fls.
Inductive nvalue : tm → Prop :=
  | nv_zro : nvalue zro
  | nv_scc : ∀ t, nvalue t → nvalue (scc t).
Definition value (t : tm) := bvalue t ∨ nvalue t.

Operational Semantics

   (ST_TestTru)  
test tru then t1 else t2 --> t1
   (ST_TestFls)  
test fls then t1 else t2 --> t2
t1 --> t1' (ST_Test)  
test t1 then t2 else t3 --> test t1' then t2 else t3
t1 --> t1' (ST_Scc)  
scc t1 --> scc t1'
   (ST_PrdZro)  
prd zro --> zro
numeric value v (ST_PrdScc)  
prd (scc v) --> v
t1 --> t1' (ST_Prd)  
prd t1 --> prd t1'
   (ST_IszroZro)  
iszro zro --> tru
numeric value v (ST_IszroScc)  
iszro (scc v) --> fls
t1 --> t1' (ST_Iszro)  
iszro t1 --> iszro t1'

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 said to be 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?

    iszro (test tru (scc zro) zro)
(1) Yes
(2) No
What about this one?

    test (scc zro) tru fls
(1) Yes
(2) No
What about this one?

    scc (scc zro)
(1) Yes
(2) No
What about this one?

    scc (test tru then tru else tru)
(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 \in T relates terms to the types of their results:
   (T_Tru)  
⊢ tru ∈ Bool
   (T_Fls)  
⊢ fls ∈ Bool
⊢ t1 ∈ Bool    ⊢ t2 ∈ T    ⊢ t3 ∈ T (T_Test)  
⊢ test t1 then t2 else t3 ∈ T
   (T_Zro)  
⊢ zro ∈ Nat
⊢ t1 ∈ Nat (T_Scc)  
⊢ scc t1 ∈ Nat
⊢ t1 ∈ Nat (T_Prd)  
⊢ prd t1 ∈ Nat
⊢ t1 ∈ Nat (T_IsZro)  
⊢ iszro t1 ∈ Bool

Example has_type_1 :
  ⊢ test fls zro (scc zro) \in Nat.
Proof.
  apply T_Test.
  - apply T_Fls.
  - apply T_Zro.
  - apply T_Scc. apply T_Zro.
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 :
  ¬( ⊢ test fls zro tru \in Bool ).
Proof.
  intros Contra. solve_by_inverts 2. Qed.

Canonical forms

The following two lemmas capture the fundamental property 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_Tru and
     T_Fls, are eliminated immediately by auto *)
  - (* T_Test *)
    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].
      ∃ (test t1' t2 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_PrdTru :
           (prd tru) --> (prd fls)
      | ST_PrdFls :
           (prd fls) --> (prd tru) 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_TestFunny : ∀ t2 t3,
           ⊢ t2 \in Nat →
           ⊢ test tru t2 t3 \in Nat Which of the following properties remain true in the presence of these rules?
  • Determinism of step
  • Progress
  • Preservation