Title
Boxy type inference for higher-rank types and impredicativity
Abstract
However, higher-rank types are not enough! Consider the fol-Languages with rich type systems are beginning to employ a blend of type inference and type checking, so that the type inference en-gine is guided by programmer-supplied type annotations. In this paper we show, for the first time, how to combine the virtues of two well-established ideas: unification-based inference, and bidi-rectional propagation of type annotations. The result is a type sys-tem that conservatively extends Hindley-Milner, and yet supports both higher-rank types and impredicativity.
Year
DOI
Venue
2006
10.1145/1159803.1159838
International Conference on Functional Programming
Keywords
Field
DocType
type inference engine,type inference,type checking,rich type system,higher-rank type,unification-based inference,boxy type,bidi-rectional propagation,type annotation,type system,programmer-supplied type annotation,programming language,polymorphism,impredicativity,abstract data type
Programming language,Annotation,Type checking,Computer science,Unification,Inference,Type theory,Type erasure,Theoretical computer science,Type inference,Impredicativity
Conference
Volume
Issue
ISSN
41
9
0362-1340
ISBN
Citations 
PageRank 
1-59593-309-3
15
0.78
References 
Authors
15
3
Name
Order
Citations
PageRank
Dimitrios Vytiniotis166036.89
Stephanie Weirich2152.47
Simon L. Peyton Jones3150.78