[mercury-users] The Logic of Mercury

[Fergus Henderson]

On 08-Sep-1999, Lee Naish <lee at cs.mu.OZ.AU> wrote:
> 
> ... it that it seems best to treat predicates as
> functions returning some special type (which you can think of as rather
> like Boolean). eg:
> 
> append :: list(T) -> list(T) -> list(T) -> pred
> ',' :: pred -> pred -> pred
...
> I believe the details have been worked out for Lambda Prolog (they use 'o'
> instead of 'pred'), though I haven't actually seen a full type system
> described and there might still be some problems.

One important problem is integrating this with the mode system.
For example, consider the (out, in, in) mode of `append'.
The obvious way of giving a mode for that would be something like

	out -> in -> in -> predmode

The trouble is that partially applying `out' modes doesn't work.
Consider a goal such as `A = append(X)'.
The obvious way of interpreting that kind of mode declaration
would suggest that this goal was mode-correct, and would bind `X'.
But in fact `X' won't be bound until `A' has been called.
It's not clear how to resolve that problem.

-- 
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.
--------------------------------------------------------------------------
mercury-users mailing list
post:  mercury-users at cs.mu.oz.au
administrative address: owner-mercury-users at cs.mu.oz.au
unsubscribe: Address: mercury-users-request at cs.mu.oz.au Message: unsubscribe
subscribe:   Address: mercury-users-request at cs.mu.oz.au Message: subscribe
--------------------------------------------------------------------------