[m-dev.] existential types

[Ralph Becket]

> From: Thomas Conway [mailto:conway at cs.mu.OZ.AU]
> 
> :- 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'.

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

Now we need to do some sordid runtime type checking:

unify(X, Y, ...) :-
    ( if univ_to_type(univ(Y), YY) then
        unify_same(X, YY, ...)
      else
        unify_other(X, Y, ...)
    ).

and we fill in...

:- pred unify_same(term, term, map(var, term), map(var, term)).
:- mode unify_same(in, in, in, out) is semidet.

unify_same(int(A), int(A), Bindings, Bindings).

unify_same(ext(A), ext(B), Bindings0, Bindings) :-
    unify(A, B, Bindings0, Bindings).

% etc...

:- pred unify_other(term, X, map(var, term), map(var, term)) <=
unifiable(X).
:- mode unify_other(in, in, in, out) is semidet.

unify_other(var(A), Y, Bindings0, Bindings) :-
    ( if map__search(Bindings0, A, X) then
        unify(X, Y, Bindings0, Bindings)
      else
        map__insert(Bindings0, A, 'new ext'(Y), Bindings)
    ).

Does that do the trick?  I've attached a module that compiles.

Ralph

--
Ralph Becket      |      MSR Cambridge      |      rbeck at microsoft.com 


begin 600 tc.m
M.BT@;6]D=6QE('1C+ at HZ+2!I;G1E<F9A8V4N"CHM(&EM<&]R=%]M;V1U;&4@
M:6YT+"!S=')I;F<L(&UA<"P@;&ES="X*"CHM('1Y<&4@=F%R(#T](&EN="X*
M"CHM('1Y<&5C;&%S<R!U;FEF:6%B;&4H5"D@=VAE<F4 at 6PH@("`@<')E9"!U
M;FEF>2A4+"!5+"!M87`H=F%R+"!T97)M*2P@;6%P*'9A<BP@=&5R;2DI(#P]
M('5N:69I86)L92A5*2P*("`@(&UO9&4@=6YI9GDH:6XL(&EN+"!I;BP@;W5T
M*2!I<R!S96UI9&5T"ETN"@HZ+2!T>7!E('1E<FT*("`@("TM+3X@("`@=F%R
M*'9A<BD*("`@(#L@("`@("`@:6YT*&EN="D*("`@(#L@("`@("`@=&5R;2AS
M=')I;F<L(&QI<W0H=&5R;2DI"B`@("`[("`@("`@('-O;64 at 6U9=("AE>'0H
M5BD@/3X@=6YI9FEA8FQE*%8I*2X*"CHM(&EN<W1A;F-E('5N:69I86)L92AT
M97)M*2X*"B4 at +2TM+2TM+2TM+2TM+2TM+2TM+2TM+2TM+2TM+2TM+2TM+2TM
M+2TM+2TM+2TM+2TM+2TM+2TM+2TM+2TM+2TM+2TM+2TM+2TM+2TM+2`E"@HZ
M+2!I;7!L96UE;G1A=&EO;BX*"CHM(&EM<&]R=%]M;V1U;&4@<W1D7W5T:6PN
M"@HZ+2!I;G-T86YC92!U;FEF:6%B;&4H=&5R;2D@=VAE<F4 at 6PH@("`@<')E
M9"AU;FEF>2\T*2!I<R!T97)M7W5N:69Y"ETN"@HE("TM+2TM+2TM+2TM+2TM
M+2TM+2TM+2TM+2TM+2TM+2TM+2TM+2TM+2TM+2TM+2TM+2TM+2TM+2TM+2TM
M+2TM+2TM+2TM+2TM+2TM+2T@)0H*.BT@<')E9"!T97)M7W5N:69Y*'1E<FTL
M(%<L(&UA<"AV87(L('1E<FTI+"!M87`H=F%R+"!T97)M*2D@/#T@=6YI9FEA
M8FQE*%<I+ at HZ+2!M;V1E('1E<FU?=6YI9GDH:6XL(&EN+"!I;BP@;W5T*2!I
M<R!S96UI9&5T+ at H*=&5R;5]U;FEF>2A8+"!9+"!":6YD:6YG<S`L($)I;F1I
M;F=S*2`Z+0H@("`@*"!I9B!U;FEV7W1O7W1Y<&4H=6YI=BA9*2P at 65DI('1H
M96X*("`@("`@("!U;FEF>5]S86UE*%@L(%E9+"!":6YD:6YG<S`L($)I;F1I
M;F=S*0H@("`@("!E;'-E"B`@("`@("`@=6YI9GE?;W1H97(H6"P at 62P@0FEN
M9&EN9W,P+"!":6YD:6YG<RD*("`@("DN"@HE("TM+2TM+2TM+2TM+2TM+2TM
M+2TM+2TM+2TM+2TM+2TM+2TM+2TM+2TM+2TM+2TM+2TM+2TM+2TM+2TM+2TM
M+2TM+2TM+2TM+2TM+2T@)0H*.BT@<')E9"!U;FEF>5]S86UE*'1E<FTL('1E
M<FTL(&UA<"AV87(L('1E<FTI+"!M87`H=F%R+"!T97)M*2DN"CHM(&UO9&4@
M=6YI9GE?<V%M92AI;BP@:6XL(&EN+"!O=70I(&ES('-E;6ED970N"@IU;FEF
M>5]S86UE*&EN="A!*2P@:6YT*$$I+"!":6YD:6YG<RP at 0FEN9&EN9W,I+ at H*
M=6YI9GE?<V%M92AE>'0H02DL(&5X="A"*2P at 0FEN9&EN9W,P+"!":6YD:6YG
M<RD at .BT*("`@('5N:69Y*$$L($(L($)I;F1I;F=S,"P at 0FEN9&EN9W,I+ at H*
M)2!E=&,N+BX*"B4 at +2TM+2TM+2TM+2TM+2TM+2TM+2TM+2TM+2TM+2TM+2TM
M+2TM+2TM+2TM+2TM+2TM+2TM+2TM+2TM+2TM+2TM+2TM+2TM+2TM+2TM+2`E
M"@HZ+2!P<F5D('5N:69Y7V]T:&5R*'1E<FTL(%@L(&UA<"AV87(L('1E<FTI
M+"!M87`H=F%R+"!T97)M*2D@/#T@=6YI9FEA8FQE*%@I+ at HZ+2!M;V1E('5N
M:69Y7V]T:&5R*&EN+"!I;BP@:6XL(&]U="D@:7,@<V5M:61E="X*"G5N:69Y
M7V]T:&5R*'9A<BA!*2P at 62P@0FEN9&EN9W,P+"!":6YD:6YG<RD at .BT*("`@
M("@@:68@;6%P7U]S96%R8V at H0FEN9&EN9W,P+"!!+"!8*2!T:&5N"B`@("`@
M("`@=6YI9GDH6"P at 62P@0FEN9&EN9W,P+"!":6YD:6YG<RD*("`@("`@96QS
M90H@("`@("`@(&UA<%]?:6YS97)T*$)I;F1I;F=S,"P at 02P@)VYE=R!E>'0G
7*%DI+"!":6YD:6YG<RD*("`@("DN"@H=
`
end
--------------------------------------------------------------------------
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
--------------------------------------------------------------------------