Already a member? Log in

Sign up with your...


Sign Up with your email address

Add Tags

Duplicate Tags

Rename Tags

Share It With Others!

Save Link

Sign in

Sign Up with your email address

Sign up

By clicking the button, you agree to the Terms & Conditions.

Forgot Password?

Please enter your username below and press the send button.
A password reset link will be sent to you.

If you are unable to access the email address originally associated with your Delicious account, we recommend creating a new account.


Links 1 through 6 of 6 by Nada Amin tagged type-inference+paper

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:

Share It With Others!

Share It With Others!

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.

Share It With Others!

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.

Share It With Others!

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.

Share It With Others!

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.

Share It With Others!