[mercury-users] Better syntax for currying and functions (was Re: Mercury syntax?

[Fergus Henderson]

Peter Moulder wrote:

> This article describes a number of syntactic conveniences.  I don't
> actually expect the mercury developers to implement any of these soon,
> as I'd prefer that more work be put into the back end than the front.
> But maybe others think differently, and different developers prefer
> working on different things.

In general I think these are interesting proposals and they all have
some merit.  For the moment I have just a few comments.

> Function syntax is indeed very sweet, and I'd like to be able to use
> it more often.  Therefore I suggest introducing another symbol, say
> `_@', such that `p(a, _@, c, d)' is a "function" returning Y such that
> p(a,Y,c,d). 

If p/4 is det, you can already write this as `(func = Y :- p(a, Y, c, d))',
so in that case the `_@' notation doesn't save you that much.

> (I place `function' in inverted commas because it needn't
> be deterministic.)

It needs to be either `det' or `semidet'.
It must not have more than one possible solution.
Otherwise, that would violate referential transparency.
For example `X = p(_@), q(X, X)' might be true even though
`q(p(_@), p(_@))' is false.  This would violates the standard
axiom of substitutivity.

In general Mercury differs from most other logic programming
languages in that Mercury takes logic seriously; we don't
want to allow people to write programs in which the basic
laws of logic are violated.

> 2b. An equivalence between functions and predicates.
> 
> As regards mapping predicates onto functions returning a bool: Mercury
> "functions" can be nondeterministic, so can already encode true/false
> information.

Mercury functions can only be `det' or `semidet' in the forwards mode.
(Mercury 0.6 didn't check this, I'm afraid, but Mercury 0.7 does.)
This is necessary to avoid violating referential transparency, just as
above.  For example `X = f(Y), q(X, X)' might be false even though
`q(p(f(X)), p(f(X)))' is true.

Yes, in the semidet case, functions do already encode true/false information.
But if you are mapping a predicate which is nondet in the
`p(in, in, ..., in, out)' mode, then you can't map it to a function,
unless you add an additional bool parameter, or map it to
a function returning a set, or something like that.

> Funny this should come up.  I just happened to be thinking today that
> data constructors are conceptually functions, so that
> 
>   :- type tree(T) ---> empty ; tree(tree(T), T, tree(T)).
> 
> is the same as declaring functions `tree__empty()' and
> `tree__tree(tree(T), T, tree(T))' and that
> 
>   (all [X,T]
>     (X is of type tree(T)) 
>     <=>
>     (
>       X = tree__empty()
>     ; 
>       X = tree__tree(_L, _V, _R),
>     )
>   ),
>   (all [L,V,R]
>     tree__empty() \= tree__tree(L,V,R)
>   ).
...
> If anything were done with type declarations ...

Well, actually we _have_ done something more with type declarations --
though it addresses a slightly different issue to the one you were
considering.  The latest development version includes support for
user-defined equality, for use in types such as maps represented
as trees.   For cases like those, where standard equality is not quite
what you want, since it compares the representations, rather than the values
they are supposed to represent; for example the map { 1 -> "foo", 2 -> "bar" }
may be represented differently depending on the order in which the
elements were inserted.  This extension allows the user to
relax the 

>   (all [L,V,R]
>     tree__empty() \= tree__tree(L,V,R)
>   ).

part of the type definition axioms.

P.S.	The latest development snapshot is available from
	ftp://turiel.cs.mu.oz.au/pub/beta-releases in the file
	mercury-rotd-*.tar.gz.

-- 
Fergus Henderson <fjh at cs.mu.oz.au>   |  "I have always known that the pursuit
WWW: <http://www.cs.mu.oz.au/~fjh>   |  of excellence is a lethal habit"
PGP: finger fjh at 128.250.37.3         |     -- the last words of T. S. Garp.