We study an extension of Hindley/Milner with
a user-programmable constraint domain and a general form of algebraic data types
which unifies common forms
such as existential types, the combination of type classes and existential types
and the more recent extension of guarded recursive data types.
We can furthermore express some novel variants such as a limited form of
dependent types.
Type inference is reduced to solving of implication constraints.
We identify sufficient conditions in terms of solutions of implication
constraints under which inference is sound and complete.
One of our main technical achievements is
a generic implication solver which is parameterized in the solver
of the underlying constraint domain.
Our results show that our system is practical and
greatly extends the expressive power of languages such as Haskell.
Slides, Haskell examples,
Chameleon examples
We give a type-driven translation from XDuce to ML
based on a structured representation of XDuce values.
XDuce type inference guides the insertion of appropriate
coercion functions such that the resulting ML program is type correct
and reflects the meaning of the original XDuce program.
Our approach is simple and represents an important step
to integrate XDuce features into
main stream functional languages such as ML.
Slides
Extending XDuce with Parametric Polymorphism
presented by Kenny.
Slides
An Overview of the new Chameleon Features
presented by Jeremy.
Slides