[Prev][Next][Index][Thread]
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
http://www.linc.dcc.ufmg.br/~lucilia/research/ml0-toplas.ps.gz.
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
definitions.
====================================================================
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.
Carlos