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.

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 v1 (ST_PrdScc)  
prd (scc v1) --> v1
t1 --> t1' (ST_Prd)  
prd t1 --> prd t1'
   (ST_IszroZro)  
iszro zro --> tru
numeric value v1 (ST_IszroScc)  
iszro (scc v1) --> fls
t1 --> t1' (ST_Iszro)  
iszro t1 --> iszro t1'

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. For example, the term scc tru cannot take a step, but the almost as obviously nonsensical term
       scc (test tru then tru else tru)
can take a step (once, before becoming stuck).

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 (because we have not included them 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?
    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

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_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) ∈ 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 ∈ 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 ∈ Bool → value t → bvalue t.
Proof.
  intros t HT [Hb | Hn].
  - assumption.
  - induction Hn; inversion HT; auto.
Qed.

Lemma nat_canonical : ∀t,
  ⊢ t ∈ 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 ∈ T →
  value t ∨ ∃t', t --> t'.
Proof with auto.
  intros t T HT.
  induction HT...
  (* The cases that were obviously values, like T_Tru and
     T_Fls, were eliminated immediately by auto *)
  - (* T_Test *)
    right. inversion IHHT1; clear IHHT1.
    + (* t1 is a value *)
    apply (bool_canonical t1 HT1) in H.
    inversion H; subst; clear H.
      ∃t2...
      ∃t3...
    + (* t1 can take a step *)
      inversion H as [t1' H1].
      ∃(test t1' t2 t3)...
  (* 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

This theorem 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.
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 also a well-typed term.
Theorem preservation : ∀t t' T,
  ⊢ t ∈ T →
  t --> t' →
  ⊢ t' ∈ 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 ∈ 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.
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 ∈ Nat →
           ⊢ test tru t2 t3 ∈ Nat
Which of the following properties remain true in the presence of these rules?
  • Determinism of step
  • Progress
  • Preservation