[mercury-users] some [T] ...

[Mark Brown]

On 18-Nov-2002, Michael Day <mikeday at yeslogic.com> wrote:
> > Another alternative is to pass around a func -- if the function has mode
> > func(in, in, ...) = out then in recent (ROTD) versions of Mercury you
> > can just use mode `in' or `out'.
> 
> Sadly, I need to thrash the io state with this thing :)
> 
> The function-considered-ground feature really seems like a bandaid applied
> to a sucking chest wound when it comes to making data structures
> containing higher order stuff.

Yes, it wasn't ever designed to be a complete solution.  We felt, though,
that the func(in, ..., in) = out mode was a special enough case to warrant
its special handling; we always intended to design and implement a more
general solution, IIRC.

As Ralph mentioned, I'm working on the new subtyping scheme (the idea itself
isn't new, the idea has been floating around for a number of years [1]).
Among other things, this should provide a more general solution to the
problem of using higher order insts.  We haven't fleshed out the full
specification, so there may prove to be a devil in the details, but here
is an example or two that should illustrate the general idea; any further
discussion about design details should probably be held on the
mercury-developers mailing list.

	:- type abc ---> a ; b ; c.

	:- subtype ab < abc ---> a ; b.

This says that ab is a subtype of abc which uses only the a and b functors.
Subtypes like ab can be used in the arguments of pred and func declarations
(including those inside typeclass declarations).  The effect on the program
is that subtype information from a pred/func declaration is propagated
into each of the corresponding mode declarations.  For example, the
declarations

	:- pred p(ab, ab).
	:- mode p(in, out) is nondet.

would be transformed into something like

	:- pred p(abc, abc).
	:- mode p(in(bound(a ; b)), out(bound(a ; b))) is nondet.

In other words, the inst 'ground' gets replaced by the inst 'bound(a ; b)',
which contains the subtype information for ab.

Here is an example of a data structure containing higher order stuff.

	:- type z_rep(T) ---> z(pred(T, io, io)).

	:- subtype z(T) < z_rep(T)
		---> z(pred(T, io, io) `with_inst` pred(in, di, uo) is det).

The LHS of the `with_inst` gives the subtype information for each
argument and the RHS gives any non-subtype information, such as
uniqueness of arguments, determinism, etc.  The meaning of an argument
qualified with `with_inst` is that the subtype information from the LHS
is propagated into the RHS the same way as it is propagated from a
pred/func declaration to its corresponding mode declaration.

So in the inst which contains the subtype information for the type z(ab),
the argument to the z functor would be the inst

	pred(in(bound(a ; b)), di, uo) is det,

where the bound(a ; b) comes from the type parameter T being bound to ab.
A predicate/function with an argument of type z(ab) would be treated
something like the following:

	:- pred q(z(ab), io, io).
	:- mode q(in, di, uo) is det.

becomes

	:- pred q(z_rep(abc), io, io) is det.
	:- mode q(in(bound(z(Z))), di, uo) is det.

where Z is the argument to the z functor mentioned above.  Of course, it is
completely up to the programmer to supply clauses for q which are consistent
with the transformed signature.

Cheers,
Mark.

[1] See, for example, http://www.cs.mu.oz.au/research/mercury/mailing-lists/mercury-developers/mercury-developers.0002/0093.html
--------------------------------------------------------------------------
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
--------------------------------------------------------------------------