[m-dev.] existential types

[Fergus Henderson]

On 23-Aug-2000, Thomas Conway <conway at cs.mu.OZ.AU> wrote:
> I have a type which is for extendable terms:
> 
> :- type term
>     --->	var(var)
>     ;		int(int)
>     ;		term(string, list(term))
>     ; some [T]	(ext(T) => unifiable(T))
>     .
> 
> :- typeclass unifiable(T) where [
>     (pred unify(T, T, map(var, term), map(var, term)),
>     (mode unify(in, in, in, out) is semidet)
> ].
> 
> In my unifyTerms pred I'd like to write:
> 
> unifyTerms(LHS, RHS, Bind0, Bind) :-
>     LHS = ext(LData),
>     (
>     	RHS = ext(RData),
> 	unify(LData, RData, Bind0, Bind)
>     ;
>     	RHS = var(_),
> 	unifyTerms(RHS, LHS, Bind0, Bind)
>     ).
> 
> But this gives the following error message:
> script.m:236: In clause for predicate `script:unifyTerms/4':
> script.m:236:   in argument 2 of call to predicate `unify/4':
> script.m:236:   type error: variable `RData' has type `T',
> script.m:236:   expected type was `T'.
> 
> Which apart from the fact that it calls both extistentially
> quantified variables the same name, is more or less what I
> expected, though of course not what I wanted. What I wanted
> was for the implied type unification to happen, and if it
> succeeds then to call the unify method on the two data items.

So write this as

	unifyTerms(LHS, RHS, Bind0, Bind) :-
	     LHS = ext(LData),
	     (
		RHS = ext(RData0),
		dynamic_type_cast(RData0, RData),
		unify(LData, RData, Bind0, Bind)
	     ;
		RHS = var(_),
		unifyTerms(RHS, LHS, Bind0, Bind)
	     ).

	:- pred dynamic_type_cast(T1::in, T2::out) is semidet.
	dynamic_type_cast(X, Y) :-
		univ_to_type(univ(X), Y).

Alternatively you can write it with the dynamic_type_cast/2 inlined,
i.e.

	unifyTerms(LHS, RHS, Bind0, Bind) :-
	     LHS = ext(LData),
	     (
		RHS = ext(RData0),
		univ_to_type(univ(RData0), RData),
		unify(LData, RData, Bind0, Bind)
	     ;
		RHS = var(_),
		unifyTerms(RHS, LHS, Bind0, Bind)
	     ).

but IMHO the former is clearer.

> If I was using univs this would work, except that I couldn't
> then constrain the value to be 'unifiable/1'.
>
> So, how do I get the behaviour I want?

The trick is to only use univs to do the type cast, not in the data
structure.

-- 
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-developers mailing list
Post messages to:       mercury-developers at cs.mu.oz.au
Administrative Queries: owner-mercury-developers at cs.mu.oz.au
Subscriptions:          mercury-developers-request at cs.mu.oz.au
--------------------------------------------------------------------------