[mercury-users] Re: your mail

[Fergus Henderson]

On 05-Sep-2001, Peter Ross <peter.ross at miscrit.be> wrote:
> I want to write some code which mimics places in coloured petri nets.
> A place in a coloured petri net has two attributes.  It contains the name
> of the place and the set of tokens of some arbitary type, T, at that place.
> I have modelled this by the two typeclasses below.
> 
> A petri net will consist of many different places where each place will have
> a different type, T.  So I want some sort of generic container which can hold
> any place, that is the existential_place type below.
> 
> Finally given an existential_place, I want to get a T out of that place,
> apply some function which will map the T to an environment.  That is
> the function f, below.
...
> The code below produces the following error:
> 
> $ mmc -e place.m
> place.m:027: In clause for predicate `place:f/3':
> place.m:027:   unsatisfiable typeclass constraint(s):
> place.m:027:   `place:place(P, U)'.
> For more information, try recompiling with `-E'.
> 
> I actually suspect what I am trying to do isn't possible with Mercurys
> current type system, and that I need constructor classes as well, but I
> would appreciated the confirmation.

One error here is that the variable T has type T,
which is extracted from the existential_place structure,
whereas the function F has type func(U) = env,
where U is determined by the caller to f/3,
and there is no guarantee that U = T.
This can be fixed by making F a typeclass member rather than passing it
as a parameter to f.

The other error, which is the one that the compiler is complaining about, is
that you call get/2 without constraining the second argument to have a type
that is a member of the appropriate type class.  Type classes with
functional dependencies would help heree.  But it is possible to achieve the
same effect by adding explicit type qualifications, e.g. via calls to
same_type/2.

See the attached code.
-- 
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.
-------------- next part --------------
:- module place.

:- interface.

	% A place has a name.
:- typeclass place(P) where [
	func name(P) = string
].

:- typeclass env(T) where [
	func get_env(T) = env
].

	% A place contains some objects of type T.
:- typeclass place(P, T) <= (place(P),env(T)) where [
		% Get one of the T's stored in P.
	pred get(P::in, T::out) is nondet
].

:- type existential_place
	--->	some [P, T] (p(P, T) => place(P, T)).

:- type env == int.

:- implementation.

	% Given an arbitary place determine it's environment.
:- pred f(existential_place::in, (func(U) = env)::in, env::out) is nondet.

f(p(Place, Dummy), F, Int) :-
	same_type(T, Dummy),
	get(Place, T),
	Int = get_env(T).

:- pred same_type(T,T).
same_type(_,_).