**namin + type-inference + paper**
6

Flexible Types: Robust type inference for first-class polymorphism (Paper PDF)

january 2009 by namin

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: http://research.microsoft.com/users/daan/

pubs.html.

type-inference
paper
implementation
haskell
hindley-milner
filetype:pdf
media:document
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: http://research.microsoft.com/users/daan/

pubs.html.

january 2009 by namin

HM(X) Type Inference is CLP(X) Solving (Paper PDF)

january 2009 by namin

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
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.

january 2009 by namin

Practical type inference for arbitrary-rank types (Paper PDF)

december 2008 by namin

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
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.

december 2008 by namin

Typing Haskell in Haskell

december 2008 by namin

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

october 2008 by namin

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

**related tags**

Copy this bookmark: