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). Here, we’ll just focus on tuples. Note that the book uses the same syntax for pair and 2-tuple terms ({t1,t2}), but different syntax for their types (T1×T2 vs. {T1,T2}). We’ll consider these to be equivalent.

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.

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

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

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

                                ti ⟶ ti'
――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――   E-Tuple
{v1, ..., vi-1, ti, ti+1, ..., tn} ⟶ {v1, ..., vi-1, ti', ti+1, ..., tn}

  t ⟶ t'
――――――――――――                         E-Proj
t.i ⟶ t'.i

――――――――――――――――――――――               E-ProjTuple
{v1, ..., vn}.i ⟶ vi

  Γ ⊢ t1 : T1  ...  Γ ⊢ tn : Tn
―――――――――――――――――――――――――――――――――    T-Tuple
Γ ⊢ {t1, ..., tn} : {T1, ..., Tn}

Γ ⊢ t : {T1, ..., Tn}
―――――――――――――――――――――                T-Proj
     Γ ⊢ t.i : Ti

As a special case, the type of 0-tuples is written as Unit, and it is inhabited by exactly one value, written as unit.

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>

    t ⟶ t'
――――――――――――――――                                                      E-Variant
<l=t> ⟶ <l=t'>

                                               t ⟶ t'
――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――   E-Case
case <li=t> of <l1=x1> ⇒ t1, ..., <ln=xn> ⇒ tn ⟶ case <li=t'> of <l1=x1> ⇒ t1, ..., <ln=xn> ⇒ tn

――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――
case <li=v> of <l1=x1> ⇒ t1, ..., <ln=xn> ⇒ tn ⟶ [xi↦v]ti        E-CaseVariant

           Γ ⊢ ti:Ti
―――――――――――――――――――――――――――――――                                       T-Variant
Γ ⊢ <lj=tj>:<l1:T1, ..., ln:Tn>

Γ ⊢ t:<l1:T1, l2:T2, ...>   Γ, x1:T1 ⊢ t1:T   ...   Γ, xn:Tn ⊢ tn:T
―――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――――   T-Case
       Γ ⊢ case t of <l1=x1> ⇒ t1, ..., <ln=xn> ⇒ tn : T

Now 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

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 ⊢ φ   Γ, φ2 ⊢ φ
―――――――――――――――――――――――――――――――――――   (∨ elimination)
                Γ ⊢ φ

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

Exercise. Prove that

• true ∨ false
• false → false
• false → true

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

What does false correspond to? The empty type, usually written ⊥ (bottom) or Zero. It can be thought of as the special case of a variant type with 0 variants. In TypeScript, it’s called never; in Rust, it’s called ! (which is pronounced “never”).

Exercise. Which of the following types are inhabited? For the ones that are inhabited, give a term of that type.

• Unit + Zero
• Unit × Zero
• Zero → Zero
• Unit → Zero
• Zero → Unit

But we’ve left a number of questions unanswered, like:

• What do ∀ and ∃ correspond to?
• What does negation correspond to?