namin + type-inference + paper   6

Flexible Types: Robust type inference for first-class polymorphism (Paper PDF)
We present HML, a type inference system that supports full firstclass
polymorphism where few annotations are needed: only function
parameters with a polymorphic type need to be annotated.
HML is a simplification of MLF where only flexibly quantified
types are used. This makes the types easier to work with from
a programmers perspective, and simplifies the implementation of
the type inference algorithm. Still, HML retains much of the expressiveness
of MLF, it is robust with respect to small program
transformations, and has a simple specification of the type rules
with an effective type inference algorithm that infers principal
types. A small reference implementation with many examples is
available at:
type-inference  paper  implementation  haskell  hindley-milner  filetype:pdf  media:document 
january 2009 by namin
HM(X) Type Inference is CLP(X) Solving (Paper PDF)
The HM(X) system is a generalization of the Hindley/Milner system parameterized in the
constraint domain X. Type inference is performed by generating constraints out of the
program text which are then solved by the domain specific constraint solver X. The solver
has to be invoked at the latest when type inference reaches a let node so that we can
build a polymorphic type. A typical example of such an inference approach is Milner’s
algorithm W.
We formalize an inference approach where the HM(X) type inference problem is first
mapped to a CLP(X) program. The actual type inference is achieved by executing the
CLP(X) program. Such an inference approach supports the uniform construction of type
inference algorithms and has important practical consequences when it comes to reporting
type errors. The CLP(X) style inference system where X is defined by Constraint Handling
Rules is implemented as part of the Chameleon system.
paper  pdf  type-inference  types  hindley-milner  filetype:pdf  media:document 
january 2009 by namin
Practical type inference for arbitrary-rank types (Paper PDF)
We take as our starting point a λ-calculus proposed by Odersky and Läufer. Their system supports arbitrary-rank polymorphism through the exploitation of type annotations
on λ-bound arguments and arbitrary sub-terms. Though elegant, and more convenient than some other proposals, Odersky and Läufer’s system requires many annotations. We show how to use local type inference (invented by Pierce and Turner) to greatly reduce the annotation burden, to the point where higher-rank types become eminently usable. Higher-rank types have a very modest impact on type inference. We substantiate this claim in a very concrete way, by presenting a complete type-inference engine, written in Haskell, for a traditional Damas-Milner type system, and then showing how to extend it for higher-rank types. We write the type-inference engine using a monadic framework: it turns out to be a particularly compelling example of monads in action. The paper is long, but is strongly tutorial in style.
types  type-inference  haskell  paper  pdf  hindley-milner  filetype:pdf  media:document  monads 
december 2008 by namin
Typing Haskell in Haskell
Haskell benefits from a sophisticated type system, but implementors, programmers, and researchers suffer because it has no formal description. To remedy this shortcoming, we present a Haskell program that implements a Haskell typechecker, thus providing a mathematically rigorous specification in a notation that is familiar to Haskell users. We expect this program to fill a serious gap in current descriptions of Haskell, both as a starting point for discussions about existing features of the type system, and as a platform from which to explore new proposals.
haskell  types  cs  paper  type-inference  hindley-milner 
december 2008 by namin
Local type inference
We study two partial type inference methods for a language combining subtyping and impredicative polymorphism. Both methods are local in the sense that missing annotations are recovered using only information from adjacent nodes in the syntax tree, without long-distance constraints such as unification variables. One method infers type arguments in polymorphic applications using a local constraint solver. The other infers annotations on bound variables in function abstractions by propagating type constraints downward from enclosing application nodes. We motivate our design choices by a statistical analysis of the uses of type inference in a sizable body of existing ML code.
type-inference  types  paper 
october 2008 by namin

Copy this bookmark: