[mercury-users] Maths and contexts.

[Julien Fischer]

On Sat, 21 Apr 2012, Julien Fischer wrote:

> The other limitation of this approach is that you are limited to the
> set of context types that are defined in your program.  You cannot
> construct new contexts at runtime.

You can support construction of contexts at runtime and get compile-time
checking of contexts mismatches (at the cost of adding an extra word to
the representation of a number) using existential types.  The modified
decimal module below demonstrates this -- I left most of the fields out
of the context to save space.  The following test program attempts
to add two decimals that have different contexts associated with them:

    :- module test.
    :- interface.
    :- import_module io.
    :- pred main(io::di, io::uo) is det.
    :- implementation.
    :- import_module decimal2.
    :- import_module bool, integer.

    main(!IO) :-
       Context1 = make_context(integer(30), round_floor, signal(no, no)),
       Context2 = make_context(integer(40), round_up, signal(no, no)),
       X = to_number(Context1, "1000000"),
       Y = to_number(Context2, "2900000"),
       Z = X `add` Y,
       io.write_string(to_scientific_string(Z), !IO),
       io.nl(!IO).

Attempting to compile the above will result in the following compilation
error:

    Making Mercury/cs/test.c
    test.m:013: In clause for predicate `main'/2:
    test.m:013:   in unification of variable `Z'
    test.m:013:   and term `add(X, Y)':
    test.m:013:   type error in argument(s) of functor `add/2'.
    test.m:013:   Argument 1 (X) has type `(some [C] decimal2.decimal(C))',
    test.m:013:   expected type was `decimal2.decimal(C)';
    test.m:013:   argument 2 (Y) has type `(some [C] decimal2.decimal(C))',
    test.m:013:   expected type was `decimal2.decimal(C)'.
    ** Error making `Mercury/cs/test.c'.

The modified code for decimals is:


 	:- module decimal2.
 	:- interface.

 	:- import_module bool.
 	:- import_module integer.
 	:- import_module string.

 	:- type rounding_strategy
 	    --->    round_down       % mandatory strategies
 	    ;       round_half_up
 	    ;       round_half_even
 	    ;       round_ceiling
 	    ;       round_floor
 	    ;       round_half_down  % optional strategies
 	    ;       round_up
 	    ;       round_05up.

 	:- type signal
 	    --->    signal(
 		       flag         :: bool,
 		       trap_enabler :: bool
 		    ).

 	:- typeclass context(C) where [
 		func precision(decimal(C)) = integer,
 		func rounding(decimal(C))  = rounding_strategy,
 		func clamped(decimal(C))   = signal
 	].

 	:- some [C] func make_context(integer, rounding_strategy, signal)
 	    = C => context(C).

 	:- type sign
 	    --->    positive
 	    ;       negative.

 	:- type decimal(C).

 	:- func to_scientific_string(decimal(C)) = string <= context(C).
 	:- func to_engineering_string(decimal(C)) = string <= context(C).

 	:- func to_number(C, string) = decimal(C) <= context(C).
 	:- func abs(decimal(C)) = decimal(C) <= context(C).
 	:- func add(decimal(C), decimal(C)) = decimal(C) <= context(C).

 	:- implementation.

 	:- type decimal(C)
 	    --->    number(
 			sign        :: sign,
 			coefficient :: integer,
 			exponent    :: integer,
 			context     :: C
 		    )

 	       ;    infinity(sign, C)

 	       ;    quiet_nan(sign, C)

 	       ;    signalling_nan(sign, C).


 	:- func get_context(decimal(C)) = C.

 	get_context(number(_, _, _, C)) = C.
 	get_context(infinity(_, C)) = C.
 	get_context(quiet_nan(_, C)) = C.
 	get_context(signalling_nan(_, C)) = C.

 	:- type rt_context
 	    --->    rt_context(
 			rtc_prec      :: integer,
 			rtc_round     :: rounding_strategy,
 			rtc_clamped   :: signal
 		    ).

 	:- instance context(rt_context) where [
 	    precision(D) = D ^ get_context ^ rtc_prec,
 	    rounding(D) = D ^ get_context ^ rtc_round,
 	    clamped(D) = D ^ get_context ^ rtc_clamped
 	].

 	make_context(Prec, Round, Clamp) = rt_context(Prec, Round, Clamp).

 	:- end_module decimal2.

Julien.
--------------------------------------------------------------------------
mercury-users mailing list
Post messages to:       mercury-users at csse.unimelb.edu.au
Administrative Queries: owner-mercury-users at csse.unimelb.edu.au
Subscriptions:          mercury-users-request at csse.unimelb.edu.au
--------------------------------------------------------------------------