[Prev][Next][Index][Thread]
RE: Decidable polymorphic recursion?

To: <types@cis.upenn.edu>

Subject: RE: Decidable polymorphic recursion?

From: "Jakob Rehof" <rehof@microsoft.com>

Date: Fri, 11 Jan 2002 14:25:50 0800

ThreadIndex: AcGZjcg2CgNfaH0nS3uY3FDqiIj+mQBU4Tcg

ThreadTopic: 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 "TypeBased
Flow Analysis: From Polymorphic Subtyping to CFLReachability" 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 CFLreachability, 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 flowpolymorphic 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 graphbased techniques lend themselves to largescale
engineering quite easily.
Links to our papers:
Manuel Fahndrich, Jakob Rehof and Manhuvir Das: "Scalable
ContextSensitive Flow Analysis Using Instantiation Constraints", PLDI
2000 http://research.microsoft.com/~rehof/pldi00.ps
Jakob Rehof and Manuel Fahndrich: "TypeBased Flow Analysis: From
Polymorphic Subtyping to CFLReachability", 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 DamasMilner and the MilnerMycroft 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
> programanalysisoriented 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 semiunification 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/