existential types (was: univ and functor/arg)

[Fergus Henderson]

I wrote:

>Currently there is a big limit to what you can do with `univ', because
>although you can convert a value to type univ, and you can convert a
>univ back to any given ground type that you know at compile time, there
>is no way to convert a univ back to a type which is not fully known at
>compile time; that means that for example if you have a univ, then
>although you can pass the univ itself to a polymorphic predicate, you
>can't pass the value stored in the univ to a polymorphic predicate.

This limitation is in fact very bad.  I keep running into it.
I'm just writing hash/1 and I find that in order to avoid this
problem, I need to have a hash_univ/1.  Duplicating the interface
is bad enough already, but in this case I also need to duplicate the code. 
For efficiency I don't want to do

	hash(X) = hash_univ(univ(X)).

because that would require a memory allocation (to create the univ)
for every call to hash/1, so instead I'm forced to have two copies
of the same code, one for hash/1 and one for hash_univ/1.

In my previous mail I proposed extending explicit type qualifications
to handle this:

>	expand_univ(Univ, F, N, Args) :-
>		expand(univ_value(Univ) : { univ_type(Univ) }, F, N, Args).

However, I've realized there is a much nicer answer that solves the
problem perfectly: existential types.

The type declaration for `univ_value' should be changed to use an
existential qualifier: instead of

	:- func univ_value(univ) = T.	% T implicitly universally quantified
	:- mode univ_value(in) = out is semidet.

it would be declared as

	:- some [T] (func univ_value(univ) = T).
	:- mode univ_value(in) = out is det.	% NB det not semidet, because
						% it does not need a type test

Then you could just write

	expand_univ(Univ, F, N, Args) :-
		expand(univ_value(Univ), F, N, Args).

and indeed there'd be no need for a separate expand_univ.

Implementation-wise, the type_info argument for an existentially
qualified type variable would have mode `out' rather than the usual
`in' mode that is used for universally qualified type variables.
Type checking and mode analysis would both need changes to handle
existential types.

I think this is definitely the right solution, but unfortunately
implementing it will require quite a significant amount of work.

In the short term I guess we'll just have to have two versions
of everything that calls expand/4, functor/3, or argument/3.

--
Fergus Henderson <fjh at cs.mu.oz.au>   |  "I have always known that the pursuit
WWW: <http://www.cs.mu.oz.au/~fjh>   |  of excellence is a lethal habit"
PGP: finger fjh at 128.250.37.3         |     -- the last words of T. S. Garp.