[mercury-users] Existential Types: Passing over typeclass of enclosed types

[Mark Brown]

Hi Nick,

On 29-Apr-2007, Jrg Roman Rudnick <joerg.rudnick at t-online.de> wrote:
> Dear all,
> 
> in his Ph.D. thesis,
> 
> David Jeffery:
>    Expressive Type Systems for Logic Programming Languages
>    University of Melbourne; February, 2002,
> 
> David Jeffery in p. 82 ff. sheds an impression a typeclass of an 
> enclosed type may be passed over to its existential type wrapper, i.e.
> 
> ---------------------------------
> :-typeclass x_y_point(T) where [
>    pred get_x(T::in, float::out) is det,
>    pred get_y(T::in, float::out) is det,
>    pred set_x(T::in, float::in, T::out) is det,
>    pred set_y(T::in, float::in, T::out) is det
> ].
> 
> :-type x_y_point --->
>    some [T] x_y_point(T) => x_y_point(T).
> 
> :-instance x_y_point(x_y_point).
> 
> :-instance x_y_point(x_y_point) where [
>    ( get_x(x_y_point(P), X) :-
>            get_x(P, X)
>    ),
>    ( get_y(x_y_point(P), Y) :-
>            get_y(P, Y)
>    ),
>    ( set_x(x_y_point(P0), X, 'new x_y_point'(P)) :-
>            set_x(P0, X, P)
>    ),
>    ( set_y(x_y_point(P0), Y, 'new x_y_point'(P)) :-
>            set_y(P0, Y, P)
>    )
> ].
> ---------------------------------
> 
> In consideration inhowfar to apply existential types, I discovered this 
> does not seem so for
> 
>    pred add(T::in, T::in, T::out) is det,
> ...
>    ( add(x_y_point(P1), x_y_point(P2), 'new x_y_point'(P)) :-
>            add(P1, P2, P)
>    ),
> 
> with the consequence that one can't use more than a single parameter in 
> in-mode - otherwise, a type clash is reported, as the compiler expects 
> the exact type instances to be different.

Yes, this is correct.  The existential quantifiers effectively hide the
types from the type checker, so it no longer has any way of knowing
they are the same.

> 
> Now my question:
> 
> As
> 
> (1) it seems the very common case that such params actually do share the 
> same type_desc, and
> 
> (2) being able to use several existentially typed in-mode params is most 
> useful (or even critical) for application,
> 
> is it possible to add an explicit assertion that identical types are used?
> 

Since it is not statically checked that the types are the same, there are
two choices:

1) Perform the check dynamically, and throw an exception (for example) if
the check fails.

2) Don't perform the check at all.  Just rely on the "very common case"
actually occurring.

The first can be done using det_univ_to_type.  For example:

	( add(x_y_point(P1), x_y_point(P2), 'new x_y_point'(P)) :-
		det_univ_to_type(univ(P2), CastP2),
		add(P1, CastP2, P)
	).

The second can be done with an "unsafe type cast", which is trivial
to write using foreign code.

Cheers,
Mark.

--------------------------------------------------------------------------
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
--------------------------------------------------------------------------