Mercury (?advanced?)

[Fergus Henderson]

On 22-Feb-1999, Serge Varennes <serge.varennes at detexis.thomson-csf.com> wrote:
> Hello, 
> I'm having a new walk through LRM (Language Reference Manual) and I got
> some questions about features I did not use up to now : 
> 	some, all, 
> and 	inst/modes (non trivial ones)
> 
> all : 
> The intuition I had appears in the following example :  
> :- module all1.
> :- interface.
> :- import_module io.
> :- pred main(io__state, io__state) is det.
> :- mode main(di, uo) is det.
> :- implementation.
> :- pred data(int, int).
> :- mode data(in, out) is nondet.
> :- import_module int.
> data(1,11).
> data(1, 111).
> data(2, 22).
> data(3, 30).
> 
> main(In, Out) :-
> 	((all [X] (data(X, Y), Y > 10))
> 		-> write(" really all", In, Int)
> 		; write("some are not", In, Int)),
> 	nl(Int, Out).
> 
> leading to the fact that X is unbound in data ... 

Yes.  Because of your mode declarations for data/2,
it is a mode error: data/2 requires its first argument
to have mode `in', but there is no producer for X,
i.e. no subgoal which can bind X.

If you simply add `:- mode data(out, out) is multi.'
then your program will work fine.

> What are the intended meaning for all and some ?

`all Vars Goal' is just the same as `not (some Vars not Goal)'.

`some Vars Goal' means existential quantification;
it introduces a new scope, and the variables in Vars
are local to that scope.  Apart from
its effects on lexical scoping, `some Vars Goal'
is operationally just the same as `Goal'.

> (could some kind of
> mode declaration be attached to their description in the documentation ?
> or even a simple example)

I don't think it would be appropriate to discuss modes at the point
where `all' and `some' are described, since the description of modes
comes several chapters later on.

I have however added a more complete description of the semantics of
existential quantification.

Index: reference_manual.texi
===================================================================
RCS file: /home/mercury1/repository/mercury/doc/reference_manual.texi,v
retrieving revision 1.128
diff -u -u -r1.128 reference_manual.texi
--- reference_manual.texi	1999/02/22 17:20:27	1.128
+++ reference_manual.texi	1999/02/22 18:17:32
@@ -409,6 +409,23 @@
 @var{Vars} must be a list of variables.
 @var{Goal} must be a valid goal.
 
+Each existential quantification introduces a new scope.
+The variables in @var{Vars} are local to the goal @var{Goal}:
+for each variable named in @var{Vars},
+any occurrences of variables with that name in @var{Goal}
+are considered to name a different variable than any
+variables with the same name that occur outside of the
+existential quantification.
+
+Operationally, existential quantification has no effect,
+so apart from its effect on variable scoping,
+ at samp{some @var{Vars} @var{Goal}} is the
+same as @samp{@var{Goal}}.
+
+Mercury's rules for implicit quantification (@pxref{Implicit quantification})
+mean that variables are often implicitly existentially quantified.
+There is usually no need to write existential quantifiers explicitly.
+
 @item @code{all @var{Vars} @var{Goal}}
 A universal quantification.
 @var{Vars} must be a list of variables.

> For inst/modes; I tried to define a length predicate with two modes (as
> suggested in the manual): 
> 	The first one length(in, out) is det. The second one looking like
> length(free->listskel(free), in) is det.

Firstly, I should point out that, as documented in the LIMITATIONS file,
the current implementation does not fully support partially instantiated
modes.  If you use modes like the second one, you may get some spurious
mode errors.

> But all attempts I had to
> implement it led to the problem How should I state the halt condition of
> the recursion (in prolog I would have used var/1 to decide in which mode
> the predicate was used and hence compare either list to nil or integer
> to 0...) What is the solution with Mercury (to avoid defining two
> different predicates). 
>
> source code (bad one)
> :- module taille.
> :- interface.
> :- import_module list.
> :- pred lg(list(T), int).
> :- inst listskel(I) = bound([];[I|listskel(I)]).
> :- mode lg(in, out) is det.
> :- mode tagada :: free->listskel(free).
> :- mode lg(tagada, in) is det.
> :- implementation.
> :- import_module int.
> 
> lg(L, T1) :-
> 	L = [] 
> 	-> T1 = 0
> 	; (L = [_|L1], T1 = T+1, lg(L, T)).

One potential solution is

	lg([], 0).
	lg([_|L], N) :- N > 0, lg(L, N - 1).

Unfortunately, however, the compiler will not be able to infer
the desired determinisms for this solution.

Here's another solution:

	:- pragma import(lg(tagada, in), "lg_backward").
	:- pragma export(lg_backward(tagada, in), "lg_backward").
	:- pragma import(lg(in, out), "lg_forward").
	:- pragma export(lg_forward(in, out), "lg_forward").

	lg_forward([], 0).
	lg_forward([_|L], N+1) :- lg_forward(L, N).

	lg_backward(L, N) :-
		(if N = 0 then L = [] else L = [_|L1], lg_backward(L1, N-1)).

I don't claim that this is a particularly elegant or efficient one, though.

I would like to allow something along the lines of

	:- pragma promise_pure(lg/2).
	lg(L::tagada, N::in) :- lg_forward(L, N).
	lg(L::out, N::in) :- lg_backward(L, N).

or (avoiding lg_forward and lg_backward)

	:- pragma promise_pure(lg/2).
	lg(L::tagada, N::in) :-
		( L = [], N = 0
		; L = [_|L1], lg_forward(L1, N-1)
		).
	lg(L::out, N::in) :-
		(if N = 0 then L = [] else L = [_|L1], lg_backward(L1, N-1)).
		
as a more elegant and more efficient alternative to the use of
`pragma import' and `pragma export', but the current implementation
doesn't support that.

-- 
Fergus Henderson <fjh at cs.mu.oz.au>  |  "Binaries may die
WWW: <http://www.cs.mu.oz.au/~fjh>  |   but source code lives forever"
PGP: finger fjh at 128.250.37.3        |     -- leaked Microsoft memo.