Re: Decidable polymorphic recursion?

• To: types@cis.upenn.edu
• Subject: Re: Decidable polymorphic recursion?
• From: Francois Pottier <francois.pottier@inria.fr>
• Date: Wed, 9 Jan 2002 10:16:22 +0100
• Cc: Josef Svenningsson <josefs@cs.chalmers.se>
• In-Reply-To: <200201081938.g08JcTJ25322@saul.cis.upenn.edu>; from josefs@cs.chalmers.se on Tue, Jan 08, 2002 at 07:41:06PM +0100
• References: <200201081938.g08JcTJ25322@saul.cis.upenn.edu>
• Reply-To: Francois.Pottier@inria.fr

Hi Josef,

> 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.

Cheers,

-- 
François Pottier
Francois.Pottier@inria.fr
http://pauillac.inria.fr/~fpottier/

• Re: Decidable polymorphic recursion?
• From: Josef Svenningsson <josefs@cs.chalmers.se>

• Prev: Re: Decidable polymorphic recursion?
• Next: Re: Formal Semantics for C
• Index(es):
  • Main
  • Thread