Abstract/Details

Practical type inference for first-class polymorphism


2008 2008

Other formats: Order a copy

Abstract (summary)

Type inference is a key component of modern statically typed programming languages. It allows programmers to omit many—and in some cases all—type annotations from programs. Type inference becomes particularly interesting theoretically and from an implementation standpoint in the presence of polymorphism. Hindley-Damas-Milner type inference, underlying modern functional programming languages with let-bound polymorphism, allows for full type reconstruction for programs with types that (i) only contain top-level quantifiers, and (ii) can only be instantiated with quantifier-free types. As soon as one attempts to overcome these barriers to allow higher-rank or impredicative polymorphism full type reconstruction becomes either undecidable or non-modular because many typeable programs no longer possess principal types. The only hope then for modular and decidable type inference for first-class polymorphism arises from exploiting type annotations to guide the type checker in a mixture of type reconstruction and type checking.

The first contribution of this dissertation is a formal study of various theoretical properties of annotation-guided inference for predicative higher-rank types. The second contribution is the presentation of a type system and inference algorithm that lift both Damas-Milner restrictions, allowing impredicative higher-rank types.

A central claim of this dissertation is that annotation-guided type inference for first-class polymorphism is compatible with intuitive specifications that do not have to be more complicated than the familiar Damas-Milner type system.

Indexing (details)


Subject
Computer science
Classification
0984: Computer science
Identifier / keyword
Applied sciences; Higher-rank polymorphisms; Polymorphisms; Type inference
Title
Practical type inference for first-class polymorphism
Author
Vytiniotis, Dimitrios
Number of pages
189
Publication year
2008
Degree date
2008
School code
0175
Source
DAI-B 69/09, Dissertation Abstracts International
Place of publication
Ann Arbor
Country of publication
United States
ISBN
9780549809791
Advisor
Weirich, Stephanie
University/institution
University of Pennsylvania
University location
United States -- Pennsylvania
Degree
Ph.D.
Source type
Dissertations & Theses
Language
English
Document type
Dissertation/Thesis
Dissertation/thesis number
3328671
ProQuest document ID
304494596
Copyright
Database copyright ProQuest LLC; ProQuest does not claim copyright in the individual underlying works.
Document URL
http://search.proquest.com/docview/304494596
Access the complete full text

You can get the full text of this document if it is part of your institution's ProQuest subscription.

Try one of the following:

  • Connect to ProQuest through your library network and search for the document from there.
  • Request the document from your library.
  • Go to the ProQuest login page and enter a ProQuest or My Research username / password.