[Prev][Next][Index][Thread]
Re: Decidable polymorphic recursion?
Francois,
On Wed, 9 Jan 2002, Francois Pottier wrote:
> > 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.
>
You're quite right about this. Polymorphic recursion in the annotations is
decidable, at least for some program analyses. One example is flow
analysis. Christian Mossin developed such an analysis in his PhD thesis.
He used a fixed point to compute the annotation for fix expressions and
then proved that it terminates.
<advertisment>
In out paper "Constraint abstractions" we show how to compute the flow
information from Mossins analysis in O(n^3) time. However, we don't use
semi-unification as you suggested but an equivalent framework called
constraint abstractions. The paper can be found at:
http://www.cs.chalmers.se/~josefs/publications/ca.ps
</advertisment>
"Annotation polymorphic recursion" was introduced for the first time (I
believe, someone will surely correct me if I'm wrong) in the context of
binding time analysis in the following paper:
@inproceedings{dussart:polymorphic-recursion,
author = {D. Dussart and F. Henglein and C. Mossin},
title = {Polymorphic Recursion and Subtype Qualifications: Polymorphic
Binding-Time Analysis in Polynomial Time},
booktitle = {proceedings of 2nd Static Analysis Symposium},
month = {September},
year = 1995
}
Cheers,
/Josef
References: