[mercury-users] type (class?) parameters

[Fergus Henderson]

On 13-Oct-2000, Michael Day <mcda at students.cs.mu.oz.au> wrote:
> 
> Something that has been bugging me is how the following use of templates
> in C++ would translate into Mercury or any other language with equivalent
> type system:
> 
> template <typename T, int size>
> struct
> {
> 	T buffer[size];
> 
> 	void do_something()
> 	{
> 		for (int i = 0; i < size; ++i)
> 		{
> 			buffer[i] = foo(buffer[i]);
> 		}
> 	}
> };
>
> Kind of like a type constructor that takes values as well as types? Eh?
> It's useful sometimes in C++ for making functions that will take the dot
> product of vectors and cleanly catch mismatched lengths. Can anyone offer
> any guidance on what this would look like in Mercury?

There's two ways.

(a) Simply don't include the non-type parameters in the type.
Instead pass them around as ordinary value parameters if needed.

	:- type blah(T) ---> blah(
		buffer :: array(T)  % note: an array(T) knows its size
	).
	:- inst uniq_blah == unique(blah(uniq_array)).

	:- pred do_something(foo(T)::di(uniq_blah), foo(T)::uo(uniq_blah))
		is det.
	do_something(X, Y) :- Y = array__map(foo, X).

(b) Represent numbers as types, e.g. using unary notation.

	:- type zero ---> zero.
	:- type succ(T) ---> succ(T).

	:- typeclass nat(T) where [func val(T) = int].
	:- instance nat(zero) where [val(_) = 0].
	:- instance nat(succ(T)) <= instance nat(T) where
			[val(succ(X)) = val(X) + 1].

	:- some [T] func int_to_nat(int) = T => nat(T).
	int_to_nat(N) = (if N = 0 then zero else succ(int_to_nat(N-1))).

    Then you can put the dimensions in as type parameters:

	:- type blah(T, N) ---> blah(
		buffer :: my_array(T, N)
	).

	:- pred do_something(foo(T, N)::di(uniq_blah), foo(T, N)::uo(uniq_blah))
		is det.
	do_something(X, Y) :- Y = my_array_map(foo, X).

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