[m-dev.] Confused about existentially quantified types

[Ralph Becket]

The reference manual states that the following is wrong

:- some [T] pred foo(T).

foo(123).
foo('a').
foo("bar").

because the types on the RHS are not unifiable.  However,
existentially quantified types are used in the store
module

:- some [S] pred store_new(store(S)).

to ensure that stores cannot be confused (that is, there
is no guarantee that separate calls to store_new/1 will
generate stores of the same type).

These two things seem to be in opposition: the first requires
that whatever type foo/0 returns it must always be the same
whereas the second says that you can't rely upon this.

This means that I can't write

:- some [T] pred something(T) => a_thing(T).

something(thing1).
something(thing2).
something(thing3).

where thing[123] all have different types but satisfy the
typeclass constraint.  Instead I have to jump through a hoop:

:- type some_thing ---> some [T] s(T) => a_thing(T).

:- some [T] pred something(some_thing).

something('new s'(thing1)).
something('new s'(thing2)).
something('new s'(thing3)).

It seems I haven't grokked part of the existential types
story.  Can someone explain?

[BTW, if you accidentally omit the `new ' then the error messages
aren't very helpful...]

Ta,

Ralph

--
Ralph Becket      |      MSR Cambridge      |      rbeck at microsoft.com 
--------------------------------------------------------------------------
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
--------------------------------------------------------------------------