Re: Decidable polymorphic recursion?

> Does anybody know of any work on type systems which are somewhere in
> between the Damas-Milner and the Milner-Mycroft calculus in
> strength? What I am looking for is a type system for which we can
> infer the types but still gives some kind of (but of course not
> full) polymorphic recursion.  Any pointers appreciated.

Hi. A paper on decidable type inference for polymorphic recursion is
available at


A shorter version of this paper has been presented at WFLP'2001 (Int'l
Workshop on Func'l & Logic Prog.). The abstract follows: 

This article presents a type system for polymorphic recursion that has
decidable type inference. The type system types exactly the same terms
as ML+(FIX-POLY). It is an extension of a type system also defined by
Damas that uses exactly the same syntax of types of ML, types exactly
the same terms, and has principal typings.

We provide also a corresponding extension of the type system and type
inference algorithm with a rule for typing mutually recursive

An implementation of the type inference algorithm (in Haskell) is
available at http://www.dcc.ufmg.br/~camarao/ml0/ml0.tar.gz, and a
paper describing it at http://www.dcc.ufmg.br/~camarao/ml0-impl.ps.