[mercury-users] Circular lists

[Warwick HARVEY]

Fergus Henderson <fjh at cs.mu.OZ.AU> writes:
> Thomas Charles CONWAY wrote:
> > :- type chain(T)
> > 	--->	chain(
> > 			store(some_store_type),
> > 			mutvar(elem(T), some_store_type)
> > 		).
>
> That should be
>
> 	:- type chain(T, S)
> 		--->	chain(
> 				store(S),
> 				mutvar(elem(T), S)
> 			).
>
> and similarly elsewhere.
>
> As explained in the documentation for store.m, the idea is that the
> `some_store_type' type used in the definition of store__init will
> eventually (when Mercury's type system supports existential types)
> be replaced by a proper existential type `some [S] S'.  If you
> use `some_store_type' explicitly, then your code will break when
> that happens.

Please let me check my understanding here.  I think it may spell trouble for
me and the program I'm writing.  :-)  (Well, at the very least, my data may
need restructuring).

When existential types are implemented, will each store be *required* to
have a distinct type?  What I'm currently trying to implement involves
(essentially) a store of stores.  If each store is forced to have a
different type, there is no way I can form a collection of them.  I can get
around this by reorganising my data structures, but I'd rather avoid this at
this stage if I can.

At the moment I'm running afoul of the type system, because when I started
I didn't really understand what the parameter S for stores was, or what it
was for.  Everything I've written has stores parameterised in this way.  The
problem I have is that when I create a new store to insert into the main
store, store__init/1 says the type is store(some_store_type), while my
predicate advertises itself as working on general store(S).  To fix this, I
will basically have to replace all occurrences of S with some_store_type
throughout my code, and it will all break when existential types are added.
But I suspect it wouldn't work now even if existential types were already
implemented (I had been wondering how there was going to be compile-time
checking that I wasn't going to use a reference to one of these stores to
access another; now I think I know: by making my data structures illegal :-(
).

There seem to be two choices available to me to fix this problem.  The
"wrong" way is to just hard-code everything to "some_store_type".  This is
easy and will work now and I can get my program running sooner.  The "right"
way seems to be to restructure things so that all the low-level "stores" are
actually just pointers into one shared store (so they all have the same
type, and there's no checking that I'm not using a reference from one of
these "logical" stores to access another, because they're actually all the
same store).

Of course, I may have just demonstrated that I have completely no idea what
I'm talking about.  If this is the case, can somebody please explain to me
how stores and types and existential types all relate to each other.  :-)

Thanks,
	Warwick

----------------------------------------------------------------------------
Warwick Harvey                                    email: warwick at cs.mu.OZ.AU
Department of Computer Science                        phone: +61-3-9344-9171
University of Melbourne                                 fax: +61-3-9348-1184
Parkville, Victoria, AUSTRALIA 3052     web: http://www.cs.mu.OZ.AU/~warwick