[mercury-users] Pred defns

[Richard A. O'Keefe]

	I've got the Prolog for a syntactic expansion that I find *very*
	helpful indeed, and much easier to read.
	
	The idea is that X` denotes the `next state' of X and X`` expands to
	the extra pair of arguments X, X`.

This is EXTREMELY confusing.  If X` denotes the `next state' of X,
then X`` should denote the `next state` of X`.  This is how ticks
are used in SML, for example:

    fun f X =
      let X' = g X in
        let X'' = h X' in
          let X''' = k X''' in
            X'''
          end
        end
      end;

	For example:
	
		io__write(..., IO``),		io__write(..., IO0, IO1),
		io__write(..., IO``),	 |->	io__write(..., IO1, IO2),
		io__write(..., IO``),		io__write(..., IO2, IO3),
	
This has me *completely* baffled.  The one thing I can rely on in Prolog
is that the same variable name stands for the same variable throughout
a clause.  Is it intended in this example that

	/* here IO means IO0, IO` means IO1 */
	io__write(..., IO``),
	/* here IO means IO1, IO` means IO2 */
	io__write(..., IO``),
	/* here IO means IO2, IO` means IO3 */
	io__write(..., IO``),
	/* here IO means IO3, IO` means IO4 */

or what?  If that _isn't_ intended, what _do_ IO and IO` stand for?


	and
	
		X` = X + 1		 |->	X1 = X0 + 1
	
Why does X mean X0 and not X?   Does it _always_ mean that even if I
don't use tick notation?  Would
		Y = X + 1		 |->	Y = X0 + 1
or would it not?  If I added a tick reference to X later, would that
change the meaning of the program?

	and
	
		map__init(M),			map__init(M0),
		map__insert(M, K0, V0, M`),	map__insert(M0, K0, V0, M1),
		map__insert(M, K1, V1, M`), |->	map__insert(M1, K1, V1, M2),
		map__insert(M, K2, V2, M`),	map__insert(M2, K2, V2, M3),
	
This is of course contrived.  Let me point out the obvious, that the
*syntactically* identical calls

		map__insert(M, K0, V0, M`),
		map__insert(M, K0, V0, M`)

would mean different things and affect different logical variables.
This is NOT the kind of thing I want in a declarative language.

	I'm so taken with this I'd like to see it adopted somewhere (hint
	hint!)

This notation makes _me_ begin to think well of monads.

	The only mildly tricky bit is that you sometimes have to add
	unifications to balance things up:
	
		( foo(X) ->			( foo(X0) ->	
			bar(X``)			bar(X0, X1), Y1 = Y0
		;			 |->	;		
			baz(Y``)			baz(Y0, Y1), X1 = X0
		),				),		
		quux(X, Y)			quux(X1, Y1)	
	
	But that really isn't hard to arrange at all.

Oh?  Nothing in your message preceding this example would lead anyone to
expect these extra unifications.  What happens if you have
	(   foo(Z) ->
	    bar(X``)
	;/* not foo(X) */
	    baz(Y``)
	),
	(   yoo(Z) ->
	    tick(X``)
	;/* not yoo(Z) */
	    tock(Y``)
	),
	hoo(X, Y, Z).
Just where do you undisclosed rules for cases like this put the extra
unifications?  Do they have the _same_ effect when they are applied to
the if-expansion

	(   foo(Z) ->
	    bar(X``)
	    (   yoo(Z) ->
		tick(X``),
		hoo(X, Y, Z)
	    ;/* not yoo(Z) */
		tock(Y``),
		hoo(X, Y, Z)
	    )
	;/* not foo(X) */
	    baz(Y``)
	    (   yoo(Z) ->
		tick(X``),
		hoo(X, Y, Z)
	    ;/* not yoo(Z) */
		tock(Y``),
		hoo(X, Y, Z)
	    )
	).

The intuition that underlies this proposal is that _real_ variables are
boxes whose contents can be changed, and that logical variables ought to
be syntactically bodged to behave in much the same way.

No thanks.  We didn't need it in Prolog (does ISO Prolog even _have_ DCGs?)
and we don't need it in Haskell or Clean.  The way out is to go *UP* to
higher level constructs, not to revert to the filth of the past.