[mercury-users] Dynamic typecasts to polymorphic types

[Fergus Henderson]

On 20-Sep-2000, Ralph Becket <rbeck at microsoft.com> wrote:
> I has looking at the pprint code and thought it would be nice if the
> generic to_doc/2 function spotted lists and generated [x, y, z] style
> output rather than '.'(x, '.'(y, '.'(z, []))) as it currently does.
> 
> My attempt at this went along the following lines:
...
> :- func my_to_doc(T) = doc.
> 
> my_to_doc(X) = ( if cast(X, Xs) then to_list_doc(Xs) else to_doc(X) ).
> 
> :- pred cast(X::in, Y::out) is semidet.
> 
> cast(X, Y) :- univ_to_type(univ(X), Y).
> 
> :- func to_list_doc(list(T)) = doc.
...
> This results in a warning:
> 
> foo.m:013: In function `foo:my_to_doc/1':
> foo.m:013:   warning: unresolved polymorphism.
> foo.m:013:   The variable with an unbound type was:
> foo.m:013:       Xs :: (list:list(T))
> foo.m:013:   The unbound type variable(s) will be implicitly
> foo.m:013:   bound to the builtin type `void'.
> 
> and to_list_doc/1 never gets called.

We should probably change that to an error rather than a warning.

> If I change its signature to
> 
> :- func to_list_doc(list(int)) = doc.
> 
> then at least [1, 2, 3, 4] gets printed as required.  The problem is
> obviously that univ_to_type(X, Y) only works if the type of Y is
> identical to that of X, rather than just subsuming it.  Is this a
> bug?

No.

In Mercury (unlike in TEL and HAL) all the types that are passed
around at runtime are ground types.  This simplifies the implementation
considerably, and improves efficiency a little.  It might also make
interoperability with other languages that support parametric
polymorphism easier.

As a result, a predicate like your cast/2 always gets passed
two ground types, and so it can only ever do a groundness check,
not a subsumption check.

> If not, I suspect we need another predicate that does as required.

You can achieve the effect that you're looking for using
the following technique:

	:- some [T2]
	   pred cast_to_list(T1::in, list(T2)::out) is semidet.

	cast_to_list(Object, List) :-
		% figure out the list element type
		type_ctor_and_args(type_of(Object), _, [ElemType]),

		% constrain the type of `List' to be list(ElemType)
		has_type(Elem, ElemType),
		same_type(List, [Elem]),

		% now the type of `List' is ground, so we can just
		% perform an ordinary cast
		cast(Object, List).

	% This could/should go in a library...
	:- pred same_type(T::unused, T::unused) is det.
	same_type(_, _).

Another way that could be used would be by calling std_util__construct/3
with an existentially quantified constructor:

	:- type t ---> some [T] t(list(T)).

	cast_to_list(Object, List) :-
		simple_construct(Object) = t(List).
	
	% This could/should go in a library...
	:- func simple_construct(ArgT) = T is semidet.
	simple_construct(Object) = Result :-
		univ_to_type(construct(type_of(Result), 0, [univ(Object)]),
			Result).

This method would be nicer, since it is simpler, and it extends more
easily to arbitrary pattern matching.  For example, if you want to
check that a type has the form `map(K, V)' or `map(T, T)', or that a
type has the form `list(T)' where T is an instance of the printable/1
type class, you could do the same thing as above, only using one of
these types instead of `t':

	:- type t2 ---> some [K, V] t2(map(K,V)).
	:- type t3 ---> some [T]    t3(map(T,T)).
	:- type t4 ---> some [T]   (t4(list(T)) => printable(T)).

However, currently we don't support std_util__construct/3 for
existentially quantified constructors, so you need to stick with
the technique I mentioned first.

-- 
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.
--------------------------------------------------------------------------
mercury-users mailing list
post:  mercury-users at cs.mu.oz.au
administrative address: owner-mercury-users at cs.mu.oz.au
unsubscribe: Address: mercury-users-request at cs.mu.oz.au Message: unsubscribe
subscribe:   Address: mercury-users-request at cs.mu.oz.au Message: subscribe
--------------------------------------------------------------------------