Unformatted text preview:

AdministriviaMore on Evaluation ContextsThe Curry-Howard CorrespondenceUniversal TypesExamplesExistential TypesCIS 500Software FoundationsFall 2006December 4AdministriviaHomework 11Homework 11 is currently due on Friday.Should we make it due next Monday instead?More on Evaluation ContextsProgress for FJTheorem [Progress]: Suppose t is a closed, well-typed normalform. Then either1. t is a value, or2. t −→ t0for some t0, or3. for some evaluation context E, we can express t ast = E[(C)(new D(v))]with D 6<: C.Evaluation ContextsE ::= evaluation contexts[ ] holeE.f field accessE.m(t) method invocation (rcv)v.m(v,E,t) method invocation (arg)new C(v,E,t) object creation (arg)(C)E castE.g.,[].fst[].fst.sndnew C(new D(), [].fst.snd, new E())Evaluation ContextsE[t] denotes “the term obtained by filling the hole in E with t.”E.g., if E = (A)[], thenE[(new Pair(new A(), new B())).fst]=(A)((new Pair(new A(), new B())).fst)Evaluation ContextsEvaluation contexts capture the notion of the “next subterm to bereduced”:IBy ordinary evaluation relation:(A)((new Pair(new A(), new B())).fst) −→ (A)(new A())by E-Cast with subderivation E-ProjNew.IBy evaluation contexts:E = (A)[]r = (new Pair(new A(), new B())).fstr0= new A()r −→ r0by E-ProjNewE[r] = (A)((new Pair(new A(), new B())).fst)E[r0] = (A)(new A())Precisely...Claim 1: If r −→ r0by one of the computation rulesE-ProjNew, E-InvkNew, or E-CastNew and E is anarbitrary evaluation context, then E[r] −→ E[r0] by the ordinaryevaluation relation.Claim 2: If t −→ t0by the ordinary evaluation relation, then thereare unique E , r, and r0such that1. t = E[r],2. t0= E[r0], and3. r −→ r0by one of the computation rules E-ProjNew,E-InvkNew, or E-CastNew.Proofs: Homework 11.The Curry-HowardCorrespondenceIntro vs. elim formsAn introduction form for a given type gives us a way ofconstructing elements 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 ∨ ¬Pnot recognized.IA proof of P ∧ Q is a pair of evidence for P and evidence forQ.IA proof of P ⊃ Q is a procedure for transforming evidence forP into 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 term)???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 term)proof simplification evaluation(a.k.a. “cut elimination”)Universal TypesMotivationIn the simply typed lambda-calculus, we often have to write severalversions of the same code, differing only in type annotations.doubleNat = λf:Nat→Nat. λx:Nat. f (f x)doubleRcd = λf:{l:Bool}→{l:Bool}. λx:{l:Bool}. f (f x)doubleFun = λf:(Nat→Nat)→(Nat→Nat). λx:Nat→Nat. f (f x)Bad! Violates a basic principle of software engineering:Write each piece of functionality once... and parameterize iton the details that vary from one instance to another.Here, the details that vary are the types!MotivationIn the simply typed lambda-calculus, we often have to write severalversions of the same code, differing only in type annotations.doubleNat = λf:Nat→Nat. λx:Nat. f (f x)doubleRcd = λf:{l:Bool}→{l:Bool}. λx:{l:Bool}. f (f x)doubleFun = λf:(Nat→Nat)→(Nat→Nat). λx:Nat→Nat. f (f x)Bad! Violates a basic principle of software engineering:Write each piece of functionality once... and parameterize iton the details that vary from one instance to another.Here, the details that vary are the types!MotivationIn the simply typed lambda-calculus, we often have to write severalversions of the same code, differing only in type annotations.doubleNat = λf:Nat→Nat. λx:Nat. f (f x)doubleRcd = λf:{l:Bool}→{l:Bool}. λx:{l:Bool}. f (f x)doubleFun = λf:(Nat→Nat)→(Nat→Nat). λx:Nat→Nat. f (f x)Bad! Violates a basic principle of software engineering:Write each piece of functionality once... and parameterize iton the details that vary from one instance to another.Here, the details that vary are the types!IdeaWe’d like to be able to take a piece of code and “abstract out”some type annotations.We’ve already got a mechanism for doing this with terms:λ-abstraction. So let’s just re-use the notation.Abstraction:double = λX. λf:X→X. λx:X. f (f x)Application:double [Nat]double [Bool]Computation:double [Nat] −→ λf:Nat→Nat. λx:Nat. f (f x)(N.b.: Type application is commonly written t [T], though t Twould be more consistent.)IdeaWhat is the type of a term likeλX. λf:X→X. λx:X. f (f x) ?This term is a function that, when applied to a type X, yields aterm of type (X→X)→X→X.I.e., for all types X, it yields a result of type (X→X)→X→X.We’ll write it like this: ∀X. (X→X)→X→XIdeaWhat is the type of a term likeλX. λf:X→X. λx:X. f (f x) ?This term is a function that, when applied to a type X, yields aterm of type (X→X)→X→X.I.e., for all types X, it yields a result of type (X→X)→X→X.We’ll write it like this: ∀X. (X→X)→X→XIdeaWhat is the type of a term likeλX. λf:X→X. λx:X. f (f x) ?This term is a function that, when applied to a type X, yields aterm of type (X→X)→X→X.I.e., for all types X, it yields a result of type (X→X)→X→X.We’ll write it like this: ∀X. (X→X)→X→XSystem FSystem F (aka “the polymorphic lambda-calculus”) formalizes thisidea by extending the simply typed lambda-calculus with typeabstraction and type application.t ::= termsx variableλx:T.t abstractiont t applicationλX.t type abstractiont [T] type applicationv ::= valuesλx:T.t abstraction valueλX.t type abstraction valueSystem FSystem F (aka “the polymorphic lambda-calculus”) formalizes thisidea by extending the simply typed lambda-calculus with typeabstraction and type application.t ::= termsx variableλx:T.t abstractiont t applicationλX.t type abstractiont [T] type applicationv ::= valuesλx:T.t abstraction valueλX.t type abstraction valueSystem F: new evaluation rulest1−→ t01t1[T2] −→ t01[T2](E-TApp)(λX.t12) [T2] −→ [X 7→ T2]t12(E-TappTabs)System F: TypesTo talk


View Full Document

Penn CIS 500 - CIS 500 LECTURE NOTES

Download CIS 500 LECTURE NOTES
Our administrator received your request to download this document. We will send you the file to your email shortly.
Loading Unlocking...
Login

Join to view CIS 500 LECTURE NOTES and access 3M+ class-specific study document.

or
We will never post anything without your permission.
Don't have an account?
Sign Up

Join to view CIS 500 LECTURE NOTES 2 2 and access 3M+ class-specific study document.

or

By creating an account you agree to our Privacy Policy and Terms Of Use

Already a member?