[mercury-users] Existential types and if-then-else

[Peter Ross]

Hi,

Here is an existential type problem that I encountered today.

Basically if you have some semidet predicate which returns an
existential type, T, you want to store that type in a maybe-like type 
that has T in it if the predicate is succesful or indicates
that the predicate has failed.

exist1.m uses maybe(T) with the existential quantification on the
predicates.

exist2.m works by getting rid of the if_then_else

exist3.m uses maybe which has an existentially typed data constructor.

Pete
-------------- next part --------------
%------------------------------------------------------------------------------%

:- module exist.

:- interface.

:- typeclass tc(TC) where [
	pred r(TC),
	mode r(in) is semidet
].

:- type maybe(T)
	--->	no
	;	yes(T).

:- some [T1] pred p(maybe(T1)) => tc(T1).
:- mode p(out) is det.

%------------------------------------------------------------------------------%

:- implementation.

:- import_module int.

p(X) :-
	(
		q(1, Y)
	->
		X = yes(Y)
	;
		X = no
	).

:- some [T2] pred q(int::in, T2::out) is semidet => tc(T2).

q(1, 2).

%------------------------------------------------------------------------------%

:- instance tc(int) where [
	pred(r/1) is s
].

:- pred s(int::in) is semidet.

s(1).

%------------------------------------------------------------------------------%
-------------- next part --------------
%------------------------------------------------------------------------------%

:- module exist2.

:- interface.

:- typeclass tc(TC) where [
	pred r(TC),
	mode r(in) is semidet
].

:- some [T1] pred p(T1) => tc(T1).
:- mode p(out) is semidet.

%------------------------------------------------------------------------------%

:- implementation.

:- import_module int.

p(X) :-
	q(1, X).

:- some [T2] pred q(int::in, T2::out) is semidet => tc(T2).

q(1, 2).

%------------------------------------------------------------------------------%

:- instance tc(int) where [
	pred(r/1) is s
].

:- pred s(int::in) is semidet.

s(1).

%------------------------------------------------------------------------------%
-------------- next part --------------
%------------------------------------------------------------------------------%

:- module exist3.

:- interface.

:- typeclass tc(TC) where [
	pred r(TC),
	mode r(in) is semidet
].

:- type maybe
	--->	no
	;	some [T] (yes(T) => tc(T)).

:- pred p(maybe).
:- mode p(out) is det.

%------------------------------------------------------------------------------%

:- implementation.

:- import_module int.

p(X) :-
	(
		q(1, Y)
	->
		X = 'new yes'(Y)
	;
		X = no
	).

:- some [T2] pred q(int::in, T2::out) is semidet => tc(T2).

q(1, 2).

%------------------------------------------------------------------------------%

:- instance tc(int) where [
	pred(r/1) is s
].

:- pred s(int::in) is semidet.

s(1).

%------------------------------------------------------------------------------%