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.
Here is one interesting instance of this idea. Imagine a
program-analysis-oriented type system where types carry (atomic) decorations.
(I'm thinking of data flow, information flow, binding time, etc. analysis
systems.) Then, it is possible to first infer the structure of types within
the usual ML type system, then infer the decorations using polymorphic
recursion. Since decorations are atomic, the semi-unification problem that
arises is (I believe) decidable.
I don't know if this idea is developed in the literature. It was inspired
to me by reading Fähndrich, Rehof and Das's paper in PLDI'00, although I
am not sure that their paper actually employs this technique.