[m-dev.] existential types

Thomas Conway conway at cs.mu.OZ.AU
Thu Aug 24 09:45:44 AEST 2000


On Wed, Aug 23, 2000 at 11:59:30PM EST, Ralph Becket wrote:

Thanks for your response Ralph. I don't think I acutually
used your ideas, but you debugged my brain enough that I
could get it right.... :-)

> There are two cases here:
> (1) either we're unifying a term with a term or
> (2) we're unifying a term with some other unifiable,
> but we can't know which ahead of time.  Therefore we need to change
> the typeclass definition to
> 
> :- typeclass unifiable(T) where [
>     pred unify(T, U, map(var, term), map(var, term)) <= unifiable(U),
>     mode unify(in, in, in, out) is semidet
> ].

Hang on. You've lost part of the specification. The whole point was that
there was an implicit type check that both the extension (ext/1) things
had the same type. For my intended semantics of my unifyTerms predicate
attempts to unify two extension terms that have different types should
fail.

You could almost do it with univs:

:- type term ....
    ;		ext(univ)
    .

unifyTerms(ext(LUniv), RHS, Bind0, Bind) :-
    (
    	RHS = ext(RUniv),
	LThing = univ_value(LUniv),
	( RUniv = univ(RThing) ->
	    unify(LThing, RThing, Bind0, Bind)
	;
	    % Types were different
	    fail
	)
    ;
    	RHS = var(_),
	...
    ).

This gets the types right, but it doesn't work because we then don't
have the typeclass constraint that LThing and RThing should be members
of unifiable. Hmm. How about this hack (assuming the original definition
of the term type):

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

[Goes away and tries this...]

Well, it compiles, and I don't see why it shouldn't work.
Question: Is there a nicer way to do it?

-- 
 Thomas Conway              Unicode for terrorists: U+0001 300C
 <conway at cs.mu.oz.au>         "Tie his hands behind his back"
 Mercurian )O+  
--------------------------------------------------------------------------
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
--------------------------------------------------------------------------



More information about the developers mailing list