Conjunctive polymorphic type checking with explicit types

dc.contributor.authorFlannery, Kevin E.en
dc.contributor.committeechairMartin, Johannes J.en
dc.contributor.committeecochairArthur, James D.en
dc.contributor.committeememberBixler, Patricken
dc.contributor.committeememberFarkas, Daniel R.en
dc.contributor.committeememberRoach, John W.en
dc.contributor.departmentComputer Science and Applicationsen
dc.date.accessioned2015-07-10T20:00:22Zen
dc.date.available2015-07-10T20:00:22Zen
dc.date.issued1989en
dc.description.abstractAn expressive type language and the ability to do compile-time type inference are desirable goals in language design, but the attainment of the former may preclude the possibility of the latter. Specifically, the type conjunction operator (type intersection) induces a rich type language at the expense of decidability of the typeable expressions. Two extreme alternatives to this dilemma are to abandon type inference (and force the programmer to, essentially, supply a derivation for his type claims) or to abandon (or restrict) type conjunction. This work presents a third alternative in which the programmer, at times, may be required to supply explicit types in order for type inference to succeed. In this way, the power of conjunctive types is preserved, yet compile-time type inference can be done for a large class of polymorphic functions, including those typeable with parametric types. To this end, we introduce a simple combinator based language with typing rules based on type conjunction and a subtype relation, of sorts, called "weaker." The validity of the type rules with respect to the usual interpretation of "type" is shown, along with the undecidability of the type relation. It is shown how the computational portion of the language can be modified to accommodate explicit type information which may direct an automatic type derivation. This new language has the principal type property with respect to a decidable relation, although deciding this relation is shown to be an NP-Complete problem. The language is extended to accommodate type fixed points, and extended further to allow all expressions with parametric types to be typed automatically, and to accommodate integers, pairs, sums, and abstract types in the form of type generators.en
dc.description.degreePh. D.en
dc.format.extentvi, 209 leavesen
dc.format.mimetypeapplication/pdfen
dc.identifier.urihttp://hdl.handle.net/10919/54527en
dc.language.isoen_USen
dc.publisherVirginia Polytechnic Institute and State Universityen
dc.relation.isformatofOCLC# 20316235en
dc.rightsIn Copyrighten
dc.rights.urihttp://rightsstatements.org/vocab/InC/1.0/en
dc.subject.lccLD5655.V856 1989.F637en
dc.subject.lcshProgramming languages (Electronic computers)en
dc.titleConjunctive polymorphic type checking with explicit typesen
dc.typeDissertationen
dc.type.dcmitypeTexten
thesis.degree.disciplineComputer Science and Applicationsen
thesis.degree.grantorVirginia Polytechnic Institute and State Universityen
thesis.degree.leveldoctoralen
thesis.degree.namePh. D.en

Files

Original bundle
Now showing 1 - 1 of 1
Loading...
Thumbnail Image
Name:
LD5655.V856_1989.F637.pdf
Size:
6.93 MB
Format:
Adobe Portable Document Format