DOC PREVIEW
CMU CS 15819 - Lecture

This preview shows page 1-2-3-4-5-6 out of 17 pages.

Save
View full document
View full document
Premium Document
Do you want full access? Go Premium and unlock all 17 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 17 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 17 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 17 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 17 pages.
Access to all documents
Download any document
Ad free experience
View full document
Premium Document
Do you want full access? Go Premium and unlock all 17 pages.
Access to all documents
Download any document
Ad free experience
Premium Document
Do you want full access? Go Premium and unlock all 17 pages.
Access to all documents
Download any document
Ad free experience

Unformatted text preview:

15-819K: Logic ProgrammingLecture 10PolymorphismFrank PfenningSeptember 28, 2006In this lecture we extend the system of simple types from the previous lec-ture to e n comp ass polymorphism. There are some technical pitfalls, andsome plausible systems do not satisfy type preservation. We discuss threeways to resto re type preservation.10.1 Heterogeneous and Homogeneous ListsTypes such as natural numbers, be it in binary or in unary notation, areeasy to specify and use in the system from the previous lecture. Genericdata structures such as lists, on the other hand, present difficulties. Recallthe type predicate for lists:list([]).list([X|Xs]) :- list(Xs).The difficult y is that for lists in general there is no restriction on X: it canhave arbitrary type. When we try to give the declarationslist : type.[] : list.’.’ : ?, list -> list.we realize that there is nothing sensible we can put as the type of the firstargument of cons.1Two solutions suggest themselves. One is to introduce a univer sal typ e“any” and ensure that t : any for all terms t. This destroys the property of1Recall that [X|Xs] is just alternate syntax for ’.’(X, Xs)LECTURE NOTES SEPTEMBER 28, 2006L10.2 Polymorphismsimple types that every well-typed term has a unique type and significantlycomplicates the type syste m. Following this direction it seems almost in-evitable that some types need to be carried at runtime. A second possibil-ity is to introduce type variables and think of the ty pe of cons tructors asschematic in their free type variables.list : type.[] : list.’.’ : A, list -> list.We will pursue this idea in this lecture. Although it is also not withoutproblems, it is quite general and leads to a rich and expressive types s ys-tem.Since the typing rules above are schematic, we ge t to choose a freshinstance for A every time we use the cons constructor. This means the ele-ments of a list can have arbitrarily different types (they are heterogeneous).For certain programs it is important to know t h at the elements of a listall have the same type. For example, we can sort a list of integers, but nota list mixing integers , booleans, and other lists . This requires that list isactually a type constructor: it takes a type as an argument and returns atype. Specifically:list : type -> typ e.[] : list(A).’.’ : A, list(A) -> list(A).With these declarations only homogeneous lists will type-check: a term oftype list(A) will be a list all of whose elemen ts are of type A.10.2 Polymorphic SignaturesWe n ow mo ve to a formal specification of typ ing . We start with signatures,which now have a more general form. We write α for type variables andα for a seq uences of type variables. As in the case of clauses and ordinaryvariables, the official s yntax quantifies over type variables in declarations.Signature Σ ::= · empty signature| Σ, a : typen→ type type const ructor declaration| Σ, f : ∀α. σ → τ function symbol declaration| Σ, p : ∀α. σ → o predicate s ymbol declarationHere, boldface “typen” stands for a se q uence type, . . . , type of lengthn. As usu al, if a sequence to the left of the arrow is empty, we may omitLECTURE NOTES SEPTEMBER 28, 2006Polymorphism L10.3the arrow altogether. Similarly, we may omit the quantifier if there are notype variables, and the argument to a type zero-ary types constructor a().Moreover, function and predicate declarations should not contain any freetype variables.The language of types is als o more elaborate, but still does not co n tainfunction types as first-class constructors.Types τ ::= α | a(τ1, . . . , τn)10.3 Polymorphic Typing for TermsThe only two rules in the system for simple types that are affected by poly-morphism are those for function and predicate symbols. We account forthe schematic nature of function and predicate declarations by allowing asubstitutionˆθ for the type variables α that occur in the declaration. Wesuppose a fixed signature Σ.dom(ˆθ) = αf : ∀α. σ → τ ∈ Σ ∆ ` t : σˆθ∆ ` f(t) : τˆθWe use the notationˆθ to indicate a substitution of types for type variablesrather ter ms for term variables.Looking ahead (or back) at the required prope r ty of type preservation,one critical lemma is t h at unification pro duces a well-type d substitution.Unfortunately, in the presence of polymorphic typing, this prop erty fails!You may want to spend a couple of minutes thinking about a poss ible coun-terexample before reading on. One way to try to find one (and also a goodstart on fixing the problem) is to attempt a proof and learn from its failure.False Claim 10.1 If ∆ ` t : τ and ∆ ` s : τ and ∆ ` t.= s | θ then ∆ ` θ substand similarly for sequences of terms.Proof attempt: We proceed by induction on the derivation D of the unifi-cation judg ment, applying inversion to t h e given typing judgments in eachcase. We focus on the proble matic one.Case: D =D0∆ ` t.= s | θ∆ ` f(t).= f(s) | θ.LECTURE NOTES SEPTEMBER 28, 2006L10.4 PolymorphismWe note that we could complete this case if we could appeal to t h e in-duction hypothesis on D0, since this would yield t h e well-typednessof θ. We can appeal to the induction hypothesis if we can show that tand s have the same sequence of types. Let’s see what we can gleanfro m applying inversion to the giving typing derivations. First, wenote that there must be a unique type declaration for f in the signa-ture, sayf : σ → τ0∈ Σ for some σ and τ0.Now we write out the inversions on t h e given typing derivations,using the uniqueness of the declaration for f.∆ ` f(t) : τ Assumptionτ = τ0ˆθ1and ∆ ` t : σˆθ1for someˆθ1By inversion∆ ` f(s) : τ Assumptionτ = τ0ˆθ2and ∆ ` s : σˆθ2for someˆθ2By inversionAt this point we would like to concludeσˆθ1= σˆθ2because then t and s would have the same sequence of types and wecould finish this case by the induction hypothesis.Unfortunately, this is not necessarily the case because all we k n ow isτ = τ0ˆθ1= τ0ˆθ2.From this we can only onclude that θ1and θ2agree on the typ e vari-ables free in τ0, but they could differ on variables that occur only in σbut not in τ0.3From this we can construct a counterexample. Consider het erogeneouslistsnil : listcons : ∀α. α, list → listThenx:nat ` cons(x, nil) : listx:nat ` cons(nil, nil) : listLECTURE NOTES SEPTEMBER 28, 2006Polymorphism L10.5andx:nat ` cons(x, nil).= cons(nil, nil) | (nil/x)but the returned


View Full Document

CMU CS 15819 - Lecture

Download Lecture
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 Lecture 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 Lecture 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?