Re: [Caml-list] Type indexed types?

[brogoff <brogoff@speakeasy.net>]

You are close, I think, to related things that would probably interest you

Try googling these

"type indexed data types"
"guarded algebraic data types"

in particular, see Simonet and Pottier's work available from the project
Cristal web site.

I think the application of constraint solving to type systems is a popular
topic these days in the type theory community.

-- Brian

On Tue, 25 Jan 2005, Jim Farrand wrote:

> Hi,
>
> This is what I need to do:
>
> Given a type, u, and a collection of types, ts, find a type t such that:
>   * t is a member of ts
>   * t can be unified with u
>   * There is no type v in ts, which unifies with u and is more general
>     than t.
>
> (In other words, find the most specific type in ts that is still equal
> to or a generalisation of u.)
>
> For example:
>
> ts = list int, int, list 'a, 'a
>
> For u = list int, the result would be list int.  For u = list string,
> the result would be list 'a, and for u = string the result would be 'a.
>
> Note that I already have a function which can compute if type a is a
> specialisation of type b.
>
> I think that in theory, I could do a brute force approach:
>   * Grab all types in ts that are generalisations of u.
>   * Order the results according to how specific they are.
>   * Arbitrarily choose one of the most specific.
>
> But there must be a smarter way!  Eg, I think that I should be able to
> start with the type u, and incrementally generalise it until I find a
> match.  It is tricky to find a method of generalisation that will cover
> the entire search space, and find the most specific type first.
>
> I am sure there must be papers on this, but I am having trouble coming
> up with the right search terms - references appreciated! :)
>
> Thanks in advance,
> Jim
>
> --
> Jim Farrand
>
> _______________________________________________
> Caml-list mailing list. Subscription management:
> http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list
> Archives: http://caml.inria.fr
> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
> Bug reports: http://caml.inria.fr/bin/caml-bugs
>