[mercury-users] Superclasses and "solutions"

[Fergus Henderson]

On 27-Feb-2002, Kerry Raymond <kerry at dstc.edu.au> wrote:
> > > foo(_) :- solutions((pred(X::out) is nondet:- f_x(X)),_List).
> 
> > If you add an explicit type qualifier, e.g. change "X" to "X `with_type` a",
> > then the error will go away; the call to solutions will then
> > find all the solutions to f_x(X) where X has type `a'.
> 
> If I wanted to find all the solutions where X has type 'a', then I could have
> just called the predicate f_a to begin with.
> 
> What I am wanting to do is to get all the solutions for both types 'a' and 'b'
> (i.e. all instance classes of the type class super). How do I do that?

Since Mercury supports dynamic loading, the concept "all types which are an
instance of a given type class" is not well-defined -- it depends on which
modules are loaded.

Even if you ignore the possibility of dynamic loading, the meaning of
this concept would change depending on what modules happen to get linked
into the program.  This goes against the idea of separate compilation --
the semantics of a goal should not depend on the contents of other modules
which are not referred to (directly or indirectly) by the module containing
that goal.  (Or at very least, not unless the goal makes explicit use of
reflection.)

In other words, Mercury supports an "open-world" semantics for type class
instances, for separate compilation and in order to allow dynamic loading,
whereas finding all solutions requires a "closed-world" semantics.

If you do need to find all solutions, then you can mirror (part of)
the type class hierarchy as Mercury predicates.  E.g. you can define
an `instance_super' predicate, which succeeds for any value of a type
which is a known instance of the `super' type class.

Here's an (incorrect) first attempt:

	:- some [T] pred instance_super(T :: unused) => super(T).
	instance_super(_ `with_type` a).
	instance_super(_ `with_type` b).

	foo(_) :- solutions((pred(X::out) is nondet:-
				instance_super(X),
				f_x(X)
			_List).

Note that the type parameter `T' to instance_super must be existentially
quantified, since it has different values for different clauses.
This parameter also has mode `unused' -- the predicate doesn't really
return a value, it just returns a type.

Unfortunately using an existential quantifier on the type is not quite
sufficient, however; the type checker will still complain because the
argument has different types in different places.  To make it work,
you need to use an existentially quantified data type:

	:- type super ---> some [T] wrap(T) <= super(T).

	:- some [T] pred instance_super(T :: unused) is multi => super(T).
	instance_super(X) :-
		( WrappedX = 'new wrap'(_ `with_type` a)
		; WrappedX = 'new wrap'(_ `with_type` b)
		),
		WrappedX = wrap(X).

With this change, `instance_super' type checks fine.
But you'll still get a type error in `foo'.
The problem is that in Mercury, lists are homogenous: all
elements of a given list have to have the same type.
But in the code for `foo', the list returned from `solutions'
would have elements of both type `a' and type `b'.

The way to solve that is to use the same existentially quantified
data type that we used before:

	foo(_) :- solutions((pred('new wrap'(X)::out) is nondet:-
				instance_super(X),
				f_x(X)
			_List).

Now all elements of the list have type `super'.

-- 
Fergus Henderson <fjh at cs.mu.oz.au>  |  "I have always known that the pursuit
The University of Melbourne         |  of excellence is a lethal habit"
WWW: <http://www.cs.mu.oz.au/~fjh>  |     -- the last words of T. S. Garp.
--------------------------------------------------------------------------
mercury-users mailing list
post:  mercury-users at cs.mu.oz.au
administrative address: owner-mercury-users at cs.mu.oz.au
unsubscribe: Address: mercury-users-request at cs.mu.oz.au Message: unsubscribe
subscribe:   Address: mercury-users-request at cs.mu.oz.au Message: subscribe
--------------------------------------------------------------------------