univ and functor/arg

[Fergus Henderson]

Hi,

I think the current behaviour of expand/4, functor/3, and argument/3
for arguments of type `univ' is wrong.  There is a distinction between
the univ itself and the value stored in it (e.g. the univ itself
always has type `univ', whereas the value stored in the univ may
have any type).  However, those predicates currently ignore this
distinction.  This can lead to incorrect behaviour, e.g. output by
`io__write' that isn't type-correct.

One possible solution would be to create new predicates expand_univ/4,
univ_functor/3, and univ_argument/3 that take arguments of type `univ'
rather than of type `T', and perform their actions of the value stored
in the univ.  The existing ones could then be defined to call the
new ones:

	functor(Term, F, N) :-
		type_to_univ(Term, Univ),
		univ_functor(Univ, F, N).

	argument(Term, N, Arg) :-
		type_to_univ(Term, Univ),
		univ_argument(Univ, N, Arg).

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

Now that all works fine, the only problem is that it increases
the size of the library interface.

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.

That's why `expand' must be written in terms of `expand_univ',
and not vice versa.

It would be easy enough to write a higher-order predicate `call_with_univ'

	:- pred call_with_univ(univ, pred(T, In, Out, Di, Uo), In, Out, Di, Uo).
	:- mode call_with_univ(in, pred(in, in, out, di, uo), in, out, di, uo).

which called the polymorphic predicate with the unwrapped univ value,
and you could use such a predicate to implement `expand_univ' in terms
of `expand', but this would not be very elegant (and probably quite
inefficient, too).

More attractive would be some way of specifying to the typechecker that
the type of a variable will be determined at runtime by the value of
an expression of type `type_info'; perhaps something like
	
	expand_univ(Univ, F, N, Args) :-
		expand(univ_value(Univ) : { univ_type(Univ) }, F, N, Args).

Here `univ_value/1' and `univ_type/1' are functions that return the
value and the type_info stored in a univ;
`Value : Type' is an explicit type qualification; and
`{ TypeInfo }' denotes the type represented by `TypeInfo', which
must be an expression of type `type_info'.

Note that without the explicit type qualification, this won't work,
because univ_value returns a polymorphic type, and this type is
unbound, so the typechecker binds it to `void', which is not what
you want; it just causes the call to univ_value to fail.
(My version of typecheck.m issues warnings about such cases;
I'll commit that soon, and eventually we should probably upgrade
such warnings to errors.)

I'm not quite sure how hard it would be to extend the type checker
(and mode checker, etc.) to allow these new

	`Expression : { TypeInfoExpression }'
	
type qualifiers.

Comments?

-- 
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.