[Prev][Next][Index][Thread]

RE: Decidable polymorphic recursion?

As has been pointed out by others, the idea of exploiting bounded
polymorphic recursion in flow analysis over a fixed type structure is
not new -- the idea has been exploited in previous work on flow
analysis by Henglein and Mossin and also in work on polymorphic region
analysis.

The main point of our PLDI 00 paper and our POPL 01 paper "Type-Based
Flow Analysis: From Polymorphic Subtyping to CFL-Reachability" is that
such analyses can be understood and implemented via context free
language reachability (CFL)-techniques. In the PLDI paper (without
subtyping) the reachability specializes to regular graph reachability
and answers a flow query in linear time. In the POPL paper we
incorporate polymorphic subtyping via full CFL-reachability, leading
to cubic time flow computation (all complexity measures are in the
size of an underlying type graph which may be exponential in program
size). The techniques directly incorporate flow-polymorphic recursion,
because a bounded type structure is "underneath" the flow
information. Our algorithm for polymorphic subtyping improved over the
complexity of previous such algorithms by abandoning the idea of
implementing polymorphism via subtype constraint duplication, and in
the case of polymorphic recursion it computes the fixpoint more
efficiently. The graph-based techniques lend themselves to large-scale
engineering quite easily.

Links to our papers:

Manuel Fahndrich, Jakob Rehof and Manhuvir Das: "Scalable
Context-Sensitive Flow Analysis Using Instantiation Constraints", PLDI
2000 http://research.microsoft.com/~rehof/pldi00.ps

Jakob Rehof and Manuel Fahndrich: "Type-Based Flow Analysis: From
Polymorphic Subtyping to CFL-Reachability", POPL 2001
http://research.microsoft.com/~rehof/popl01.ps
  
Cheers,

   --Jakob and Manuel


> -----Original Message-----
> From: Francois Pottier [mailto:francois.pottier@inria.fr]
> Sent: Wednesday, January 09, 2002 1:16 AM
> To: types@cis.upenn.edu
> Cc: Josef Svenningsson
> Subject: Re: Decidable polymorphic recursion?
> 
> [----- The Types Forum, http://www.cis.upenn.edu/~bcpierce/types -----]
> 
> 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/