CIS 500Software FoundationsFall 2006October 16Any Questions?Plan“We have the technology...”IIn this lecture and the next, we’re going to cover some simpleextensions of the typed-lambda calculus (TAPL Chapter 11).1. Products, records2. Sums, variants3. RecursionIWe’re skipping Chapters 10 and 12.Erasure and TypabilityErasureWe can transform terms in λ→to terms of the untypedlambda-calculus simply by erasing type annotations onlambda-abstractions.erase(x) = xerase(λx:T1. t2)= λx. erase(t2)erase(t1t2) = erase(t1) erase(t2)TypabilityConversely, an untyped λ-term m is said to be typable if there issome term t in the s imply typed lambda-calculus, some type T,and some context Γ such that erase(t) = m and Γ ` t : T.This process is called type reconstruction or type inference.Example: Is the termλx. x xtypable?TypabilityConversely, an untyped λ-term m is said to be typable if there issome term t in the s imply typed lambda-calculus, some type T,and some context Γ such that erase(t) = m and Γ ` t : T.This process is called type reconstruction or type inference.Example: Is the termλx. x xtypable?The Curry-HowardCorrespondenceIntro vs. elim formsAn introduction form for a given type gives us a way ofconstructing eleme nts of this type.An elimination form for a type gives us a way of using elements ofthis type.The Curry-Howard CorrespondenceIn constructive logics, a proof of P must provide evidence for P.I“law of the excluded middle” — P ∨ ¬P — not recognized.A proof of P ∧ Q is a pair of evidence for P and evidence for Q.A proof of P ⊃ Q is a procedure for transforming evidence for Pinto evidence for Q.Propositions as TypesLogic Programming languagespropositions typesproposition P ⊃ Q type P→Qproposition P ∧ Q type P × Qproof of proposition P term t of type Pproposition P is provable type P is inhabited (by some te rm)proof simplificationevaluation(a.k.a. “cut elimination”)Propositions as TypesLogic Programming languagespropositions typesproposition P ⊃ Q type P→Qproposition P ∧ Q type P × Qproof of proposition P term t of type Pproposition P is provable type P is inhabited (by some te rm)proof simplificationevaluation(a.k.a. “cut elimination”)On to real programminglanguages...Base typesUp to now, we’ve formulated “base types” (e.g. Nat) by addingthem to the syntax of types, extending the syntax of terms withassociated constants (zero) and operators (succ, etc.) andadding appropriate typing and evaluation rules. We can do this foras many base types as we like.For more theoretical discussions (as opposed to programming) wecan often ignore the term-level inhabitants of base types, and justtreat these types as uninterpreted constants.E.g., suppose B and C are some base types. Then we can ask(without knowing anything more about B or C) whether there areany types S and T such that the term(λf:S. λg:T. f g) (λx:B. x)is well typed.The Unit typet ::= ... termsunit constant unitv ::= ... valuesunit constant unitT ::= ... typesUnit unit typeNew typing rules Γ ` t : TΓ ` unit : Unit(T-Unit)Sequencingt ::= ... termst1;t2t1−→ t01t1;t2−→ t01;t2(E-Seq)unit;t2−→ t2(E-SeqNext)Γ ` t1: Unit Γ ` t2: T2Γ ` t1;t2: T2(T-Seq)Sequencingt ::= ... termst1;t2t1−→ t01t1;t2−→ t01;t2(E-Seq)unit;t2−→ t2(E-SeqNext)Γ ` t1: Unit Γ ` t2: T2Γ ` t1;t2: T2(T-Seq)Derived formsISyntatic sugarIInternal language vs. external (surface) languageSequencing as a derived formt1;t2def= (λx:Unit.t2) t1where x /∈ FV(t2)Equivalence of the two definitions[board]AscriptionNew s yntactic formst ::= ... termst as T ascriptionNew e valuation rules t −→ t0v1as T −→ v1(E-Ascribe)t1−→ t01t1as T −→ t01as T(E-Ascribe1)New typing rules Γ ` t : TΓ ` t1: TΓ ` t1as T : T(T-Ascribe)Ascription as a derived formt as Tdef= (λx:T. x) tLet-bindingsNew s yntactic formst ::= ... termslet x=t in t let bindingNew e valuation rules t −→ t0let x=v1in t2−→ [x 7→ v1]t2(E-LetV)t1−→ t01let x=t1in t2−→ let x=t01in t2(E-Let)New typing rules Γ ` t : TΓ ` t1: T1Γ, x:T1` t2: T2Γ ` let x=t1in t2: T2(T-Let)Pairs , tuples, and recordsPairst ::= ... terms{t,t} pairt.1 first projectiont.2 second projectionv ::= ... values{v,v} pair valueT ::= ... typesT1× T2product typeEvaluation rules for pairs{v1,v2}.1 −→ v1(E-PairBeta1){v1,v2}.2 −→ v2(E-PairBeta2)t1−→ t01t1.1 −→ t01.1(E-Proj1)t1−→ t01t1.2 −→ t01.2(E-Proj2)t1−→ t01{t1,t2} −→ {t01,t2}(E-Pair1)t2−→ t02{v1,t2} −→ {v1,t02}(E-Pair2)Typing rules for pairsΓ ` t1: T1Γ ` t2: T2Γ ` {t1,t2} : T1× T2(T-Pair)Γ ` t1: T11× T12Γ ` t1.1 : T11(T-Proj1)Γ ` t1: T11× T12Γ ` t1.2 : T12(T-Proj2)Tuplest ::= ... terms{tii∈1 ..n} tuplet.i projectionv ::= ... values{vii∈1 ..n} tuple valueT ::= ... types{Tii∈1 ..n} tuple typeEvaluation rules for tuples{vii∈1 ..n}.j −→ vj(E-ProjTuple)t1−→ t01t1.i−→ t01.i(E-Proj)tj−→ t0j{vii∈1 ..j−1,tj,tkk∈j+1 ..n}−→ {vii∈1 ..j−1,t0j,tkk∈j+1 ..n}(E-Tuple)Typing rules for tuplesfor each i Γ ` ti: TiΓ ` {tii∈1 ..n} : {Tii∈1 ..n}(T-Tuple)Γ ` t1: {Tii∈1 ..n}Γ ` t1.j : Tj(T-Proj)Recordst ::= ... terms{li=tii∈1 ..n} recordt.l projectionv ::= ... values{li=vii∈1 ..n} record valueT ::= ... types{li:Tii∈1 ..n} type of recordsEvaluation rules for records{li=vii∈1 ..n}.lj−→ vj(E-ProjRcd )t1−→ t01t1.l−→ t01.l(E-Proj)tj−→ t0j{li=vii∈1 ..j−1,lj=tj,lk=tkk∈j+1 ..n}−→ {li=vii∈1 ..j−1,lj=t0j,lk=tkk∈j+1 ..n}(E-Rcd)Typing rules for recordsfor each i Γ ` ti: TiΓ ` {li=tii∈1 ..n} : {li:Tii∈1 ..n}(T-Rcd)Γ ` t1: {li:Tii∈1 ..n}Γ ` t1.lj: Tj(T-Proj)Sums and variantsSums – motivating examplePhysicalAddr = {firstlast:String, addr:String}VirtualAddr = {name:String, email:String}Addr = PhysicalAddr + VirtualAddrinl : “PhysicalAddr → PhysicalAddr+VirtualAddr”inr : “VirtualAddr → PhysicalAddr+VirtualAddr”getName = λa:Addr.case a ofinl x ⇒ x.firstlast| inr y ⇒ y.name;New s yntactic formst ::= ... termsinl t tagging (left)inr t tagging (right)case t of inl x⇒t | inr x⇒t casev ::= ... valuesinl v tagged value (left)inr v tagged value (right)T ::= ... typesT+T sum typeT1+T2is a disjoint union of T1and T2(the tags inl and inrensure disjointness)New evaluation rules t −→ t0case (inl v0)of inl x1⇒t1| inr x2⇒t2−→ [x17→ v0]t1(E-CaseInl)case (inr v0)of inl x1⇒t1| inr x2⇒t2−→ [x27→ v0]t2(E-CaseInr)t0−→ t00case t0of inl