[mercury-users] accessing typeclass dictionaries

[Juergen Stuber]

Fergus Henderson <fjh at cs.mu.OZ.AU> writes:
>
> On 05-Nov-1999, Juergen Stuber <juergen at mpi-sb.mpg.de> wrote:
> > On a similar note, it would also be nice to get access to
> > the dictionaries for typeclasses by some kind of low-lewel
> > Mercury.  Then I could put values such as for example the N
> > for the type of integers modulo N there and access them
> > efficiently (there is already a rather inefficient way to do
> > it with existential types).  This allows to use the standard
> > infix notation as the N gets passed around in the type, and
> > the typechecker makes sure I only add two numbers with the
> > same modulus.
> 
> I don't really understand what you mean here.
> Perhaps you could elaborate, e.g. by showing the way to do
> it with existential types.

With existential types it is possible to encode any value
in a type that is created dynamically:
 
:- module et_test.
%------------------------------------------------------------
:- interface.
:- import_module io.

:- pred main( state, state).
:- mode main( di,    uo   ) is det.

%------------------------------------------------------------
:- implementation.
:- import_module int.
:- use_module require.

:- typeclass int_singleton(T) where [
       func value(T) = int
   ].

:- type zero ---> zero.

:- instance int_singleton(zero) where [
       func(value/1) is zero_value
   ].

:- type succ(N) ---> succ(N).

:- instance int_singleton(succ(N)) <= int_singleton(N) where [
       func(value/1) is succ_value
   ].

:- func zero_value(zero) = int.
zero_value(_) = 0.

:- func succ_value(succ(N)) = int <= int_singleton(N).
succ_value(succ(N)) = value(N)+1.

:- type natural_number ---> some [N] (nat(N) => int_singleton(N)).

:- some [T] func to_natural_number(int) = T => int_singleton(T).
to_natural_number(I) = Result :-
    ( I=0 ->
	N = 'new nat'(zero)
    ; I>0 ->
	N1 = to_natural_number(I-1),
	N = 'new nat'(succ(N1))
    ; % I<0,
	require__error("to_natural_number: cannot convert negative integer")
    ),
    N = nat(Result).

main -->
    { N = to_natural_number(3) },
    print(value(N)),
    nl.

%------------------------------------------------------------
:- end_module et_test.

If I would really use it I'd have a binary representation,
but it would still be inefficient.

> If you want to put an integer in the typeclass dictionary,
> you can use a zero-arity function method that returns an integer:
> 
> 	typeclass foo(T) where [
> 		func num(T::unused) = (int::out) is det
> 	].
> 
> This is not quite as efficient as putting an integer in the
> typeclass dictionary, since you may end up doing an indirect
> method call rather than merely doing a load.  But I find it hard
> to imagine this making a significant difference in real applications.

This is ok for me as an interface to access that value.
The problem is that I have to provide a fixed function `num'
in an instance declaration at compile time, at a time when
the number I want to return is not yet known.  In some
low-level Mercury I could assemble the dictionary as I like
it when I create the first value of that type, and put a
closure that returns my value as the function for `num'.

Unfortunately my integer_modulo module where I use this is
not ready for prime time.

Jürgen

-- 
Jürgen Stuber <juergen at mpi-sb.mpg.de>
http://www.mpi-sb.mpg.de/~juergen/
--------------------------------------------------------------------------
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
--------------------------------------------------------------------------