[m-dev.] Confused about existentially quantified types

[Fergus Henderson]

On 16-Nov-2000, Ralph Becket <rbeck at microsoft.com> wrote:
> 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.

Right.  Each variable or head argument must have a single type.
However, that type can be a non-ground type (e.g. a type variable)
which at run-time gets bound to different types.
So the following is allowed, for example:

	:- some [T] pred foo(T).
	foo(univ_value(X)) :-
		( X = univ(123)
		; X = univ('a')
		; X = univ("bar")
		).

And this code has essentially the same effect as your original example.
This is documented in the section "Some idioms for using existentially
quantified types".

It would be possible to allow the first example, if we supported
undiscriminated union types, but that would be quite a bit of work
to implement.  Prohibiting cases like the first example also makes it
easier to issue good error messages for programs that don't involve
the use of existential types.

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

The first of these is wrong: you have to return the same type variable
in each clause, but that type variable can be bound to different
things, as in my example above.

However, the *determinism* declaration for `store__new',
together with the fact that it has no input arguments,
does mean that it must always return the same thing.
And this is indeed in seeming contradiction with the
existential type declaration, which says that it may
return different things.

There's no actual contradiction, since it's always OK for the type
declaration to be more restrictive than necessary.

The reason that we use a more restrictive declaration is that
the safety of the store implementation relies on it.  This is
mildly dissatisfying, since safety of the store implementation
is essentially relying on the type checker being dumb, i.e.
not taking determinism information into account.  However, it works:
it's safe, and efficient, and it doesn't require any new language
extensions.  These qualities make it better than any of the
alternative ways of implementing stores.

> 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:

That's right.  See above for the rationale (supporting undiscriminated
unions would be lots of work and would make good error messages harder).

> :- 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)).

The `some [T]' there on the declaration for something/1
is superfluous, since there's no other occurrence of T.
(The compiler ought to issue a warning or error for that.)

The right way to write this is

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

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

	something(X) :-
		( S = 'new s'(thing1)
		; S = 'new s'(thing2)
		; S = 'new s'(thing3)
		),
		S = s(X).

-- 
Fergus Henderson <fjh at cs.mu.oz.au>  |  "I have always known that the pursuit
                                    |  of excellence is a lethal habit"
WWW: <http://www.cs.mu.oz.au/~fjh>  |     -- 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
--------------------------------------------------------------------------