CS611 Lecture 25 Products, Sums, and Other Datatypes 27 October 2006Lecturer: Dexter Kozen1 IntroductionIn this lecture, we add constructs to the typed λ-calculus that allow working with more complicated datastructures, such as pairs, tuples, records, sums and recursive functions. We also provide denotational seman-tics for these new constructs.2 Recap – The Typed λ-Calculus λ→2.1 Syntaxterms e ::= n | true | false | null | x | e1e2| λx:τ. etypes τ ::= int | bool | unit | τ1→ τ2values v ::= n | true | false | null | λx:τ. e closed2.2 Typing RulesΓ ` n:int Γ ` true:b ool Γ ` false : bool Γ ` null :unit Γ, x:τ ` x:τΓ ` e0:σ → τ Γ ` e1:σΓ ` e0e1:τΓ, x:σ ` e:τΓ ` (λx:σ. e):σ → τ3 Simple Data StructuresEach data structure can be added by extending the syntax of expressions (e), types (τ) and values (v). Theevaluation contexts (E) will also need to be extended, and evaluation and type derivation rules added towork with the new syntax.3.1 PairsSyntax:e ::= · · · | (e1, e2) | #1 e | #2 eτ ::= · · · | τ1∗ τ2v ::= · · · | (v1, v2)E ::= · · · | ([•], e) | (v, [•]) | #1 [•] | #2 [•]For every added syntactic form, we observe that we have expressions that introduce the form, and expressionsthat eliminate the form. In the case of pairs, the introduction expression is (e1, e2), and the eliminationexpressions are #1 e and #2 e.Evaluation rules:#1 (v1, v2) → v1#2 (v1, v2) → v2Note that these rules define eager evaluation, because we only select from a pair when both elements arealready evaluated to a value.Typing rules:Γ ` e1:τ1Γ ` e2:τ2Γ ` (e1, e2):τ1∗ τ2Γ ` e:τ1∗ τ2Γ ` #1 e:τ1Γ ` e:τ1∗ τ2Γ ` #2 e:τ213.2 TuplesSyntax:e ::= · · · | (e1, . . . , en) | #n eτ ::= · · · | τ1∗ · · · ∗ τnv ::= · · · | (v1, . . . , vn)E ::= · · · | (v1, . . . , vi−1, [•], ei+1, . . . , en) | #n [•]Evaluation rule:#m (v1, . . . , vn) → vm(1 ≤ m ≤ n)Typing rules:Γ ` ei:τii ∈ {1, . . . , n}Γ ` (e1, . . . , en):τ1∗ · · · ∗ τnΓ ` e:τ1∗ · · · ∗ τnΓ ` #m e:τm(1 ≤ m ≤ n)3.3 RecordsSyntax:e ::= · · · | {x1= e1, . . . , xn= en} | e.xτ ::= · · · | {x1: τ1, . . . , xn: τn}v ::= · · · | {x1= v1, . . . , xn= vn}E ::= · · · | {x1= v1, . . . , xi−1= vi−1, xi= [•], xi+1= ei+1, . . . , xn= en) | [•].xEvaluation rule:{x1= v1, . . . , xn= vn}.xi→ vi(1 ≤ i ≤ n)Typing rules:Γ ` ei:τi, 1 ≤ i ≤ nΓ ` {x1= e1, . . . , xn= en):{x1: τ1, . . . , xn: τn}Γ ` e:{x1: τ1, . . . , xn: τn}Γ ` e.xi:τi(1 ≤ i ≤ n)3.4 SumsSums are useful for representing datatypes that can have multiple forms. For example, a tail of a list caneither b e another nonempty list or null.Syntax:e ::= · · · | inLτ1+τ2e | inRτ1+τ2e | case e0of e1| e2τ ::= · · · | τ1+ τ2v ::= · · · | inLτ1+τ2v | inRτ1+τ2vE ::= · · · | inL [•] | inR [•] | case [•] of e1| e2The inL and inR constructs are called left injection and right injection, respectively.Evaluation rules:case (inLτ1+τ2v) of e1| e2→ e1v case (inRτ1+τ2v) of e1| e2→ e2v2Here e1and e2are functions and must have the same codomain type in order for the whole case expressionto have a type.Typing rules:Γ ` e:τ1Γ ` inLτ1+τ2e:τ1+ τ2Γ ` e:τ2Γ ` inRτ1+τ2e:τ1+ τ2Γ ` e0:τ1+ τ2Γ ` e1:τ1→ τ3Γ ` e2:τ2→ τ3Γ ` case e0of e1| e2:τ3To give an example of the sum type, consider the sum of two unit types, unit + unit. This type hasexactly two elements, namely inL null and inR null. We could take this as a definition of the type bool withelements true4= inL null and false4= inR null. The statement if b then e1else e2could then be written ascase b of λz. e1| λz. e2.SML has a construct that is a generalization of the sum type:e ::= · · · | xi(e)τ ::= · · · | [x1: τ1, . . . , xn: τn]The SML syntax isdatatype t = x1 of t1 | ... | xn of tn.Such datatypes are also called variants. The xi are constructors, and must b e globally (across all types)unique to avoid confusion as to which type a particular constructor is referring to (in our sum type, theconfusion is alleviated by using τ1+ τ2subscripts in inLand inR).4 Denotational SemanticsWe now give the denotational semantics for type domains of λ→+∗, the strongly-typed λ-calculus with sumand product types.T [[τ → τ0]]4= T [[τ ]] → T [[τ0]]T [[τ ∗ τ0]]4= T [[τ ]] × T [[τ0]]T [[τ + τ0]]4= T [[τ ]] + T [[τ0]]As before, our contract for this language is:ρ |= Γ ∧ Γ ` e:τ ⇒ C[[e]]Γρ ∈ T [[τ ]].The remaining semantic rules are:C[[(e1, e2)]]Γρ4= hC[[e1]]Γρ, C[[e2]]ΓρiC[[#1 e]]Γρ4= π1(C[[e]]Γρ)C[[#2 e]]Γρ4= π2(C[[e]]Γρ)C[[inLτ1+τ2e]]Γρ4= in1(C[[e]]Γρ)C[[inRτ1+τ2e]]Γρ4= in2(C[[e]]Γρ)C[[case e0of e1| e2]]Γρ4= case C[[e0]]Γρ of inL v → (C[[e1]]Γρ) v | inR v → (C[[e2]]Γρ) v,where πnis the (mathematical) projection operator that selects the nth element of a product and innis theinjection ope rator that injects an element into a coproduct.35 Adding RecursionSo far this language is not Turing-complete, because there is no way to do unbounded recursion. This is truebecause there is no possibility of nontermination. The easiest way to add this capability to the language isto add support for recursive functions.To do this, we first extend the definition of an expression:e ::= · · · | rec f :σ → τ .λx : σ. eThe new keyword rec defines a recursive function named f such that both x and f are in scope inside e.Intuitively, the meaning of rec f :σ → τ .λx :σ. e is the least fixpoint of the map f 7→ λx :σ. e, where both fand λx: σ. e are of type σ → τ .For example, we would write the recursive functionf(x) = if x > 0 then 1 else f(x + 1)asrec f :int → int .λx: int. if x > 0 then 1 else f(x + 1).The small-step operational semantics evaluation rule for rec is:rec f :σ → τ .λx : σ. e → λx:σ. e{(rec f : σ → τ .λx : σ. e)/f}and the typing rule for rec isΓ, f :σ → τ, x : σ ` e:τΓ ` (rec f :σ → τ .λx : σ. e):σ → τ.The denotational semantics is defined in terms of the fix operator on domains:C[[rec f :σ → τ .λx : σ. e]]Γρ4= fix λg ∈ T [[σ → τ ]]. λv ∈ T [[σ ]]. C[[e]] Γ[(σ → τ )/f, σ/x] ρ[v/x, g/f]Of course, whenever we take a …