Sum and product types

Product types

Read TAPL 11.6-8.

Pierce shows how to add pairs, tuples (which are an easy generalization of pairs), and records (which are basically tuples with named members).

Scheme cons cells, Python tuple, and C struct are real-world examples of product types.

The i ∈ 1..n notation that the book uses is a bit hard to read; here’s a less rigorous notation that also uses evaluation contexts.

t ::= ...
      {t, t, ...}
      t.i             (i≥1)

v ::= ...
      {v, v, ...}

T ::= ...
      {T, T, ...}

E ::= ...
      E.i
      {v, v, ..., E, t, t, ...}

{v1, v2, ...}.j ⟶ vj             E-ProjTuple

  Γ ⊢ t1 : T1  Γ ⊢ t2 : T2  ...
―――――――――――――――――――――――――――――――――  T-Tuple
Γ ⊢ {t1, t2, ...} : {T1, T2, ...}

Γ ⊢ t : {T1, T2, ...}
―――――――――――――――――――――              T-Proj
     Γ ⊢ t.j : Tj

Sum types

Read TAPL 11.9-10.

Pierce presents two kinds of sum types: sums and variants, which are an easy generalization of sums.

C union is not quite the same as a sum type, because a C union variable doesn’t “know” which of the two unioned types it belongs to. Sum types are often called tagged unions to distinguish from C-style untagged unions.

Question: Why don’t untyped languages (Scheme, Python) typically have sum types?

In order to preserve uniqueness of types, TAPL adds as clauses in many places. For variants, these are actually not necessary if we require that every label uniquely determines a variant type. This is, in fact, the case in many languages, like ML and Haskell (p. 141). We will adopt this convention.

Again, the notation gets a bit hard to read; here’s a less rigorous version.

t ::= ...
      <l=t>
      case t of <l=x> ⇒ t, <l=x> ⇒ t, ...

T ::= ...
      <l:T, l:T, ...>

E ::= ...
      case E of <l=x> ⇒ t, <l=x> ⇒ t, ...
      <l=E>

case <lj=vj> of <l1=x1> ⇒ t1, <l2=x2> ⇒ t2, ... ⟶ [xj↦vj]tj      E-CaseVariant

           Γ ⊢ tj:Tj
―――――――――――――――――――――――――――――――                                       T-Variant
Γ ⊢ <lj=tj>:<l1:T1, l2:T2, ...>

Γ ⊢ t:<l1:T1, l2:T2, ...>   Γ, x1:T1 ⊢ t1:T   Γ, x2:T2 ⊢ t2:T   ...
―――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――   T-Case
        Γ ⊢ case t of <l1=x1> ⇒ t1, <l2=x2> ⇒ t2 : T

Assuming that we have a Unit type, we can define variants like

Color ≡ <red:Unit, green:Unit, blue:Unit>

which are analogous to C/C++/Java enum. In particular, we no longer need Bool to be built in; we can define it ourselves:

Bool ≡ <false:Unit, true:Unit>

Exercise. Show how to simulate if if Bool is defined as above.

Propositions as types (graduate only)

Now would be a good time to bring up the Curry-Howard isomorphism (pages 108-109). Forget about type systems for a moment and think about propositional logic.

We define a syntax of formulas:

φ ::= x
      true
      false
      φ → φ
      φ ∧ φ
      φ ∨ φ

And inference rules for Γ ⊢ φ (“under the assumptions in Γ, φ is provable”):

――――――――
Γ ⊢ true

――――――――
Γ, φ ⊢ φ

 Γ, φ1 ⊢ φ2
――――――――――――                              (→ introduction)
Γ ⊢ φ1 → φ2                              
                                          
Γ ⊢ φ1 → φ2  Γ ⊢ φ1                      
――――――――――――――――――――                      (→ elimination, or modus ponens)
       Γ ⊢ φ2                             
                                          
Γ ⊢ φ1  Γ ⊢ φ2                            
――――――――――――――                            (∧ introduction)
 Γ ⊢ φ1 ∧ φ2                              
                                          
Γ ⊢ φ1 ∧ φ2                               
―――――――――――   i ∈ {1,2}                   (∧ elimination)
  Γ ⊢ φi                                  
                                          
   Γ ⊢ φi                                 
―――――――――――   i ∈ {1,2}                   (∨ introduction)
Γ ⊢ φ1 ∨ φ2

Γ ⊢ φ1 ∨ φ2   Γ ⊢ φ1 → φ   Γ ⊢ φ1 → φ
―――――――――――――――――――――――――――――――――――――――   (∨ elimination)
                Γ ⊢ φ

This is a restriction of propositional logic called intuitionistic propositional logic that doesn’t have negation.

The Curry-Howard isomorphism is a correspondence between proof systems in logic and type systems in programming language theory. Notice the similarity between these rules and the typing rules we’ve built up so far.

proof systems	type systems
formulas φ	types T
assumptions Γ	contexts Γ
Γ ⊢ φ	Γ ⊢ t:T for some t
→	→
∧	×
∨	+
true	unit

This naturally leads to a number of questions, like:

• What does false correspond to? The empty type, usually written ⊥.
• What do ∀ and ∃ correspond to?
• What does negation correspond to?