[mercury-users] The Logic of Mercury

[Lee Naish]

In message <199909062253.KAA22465 at hermes.otago.ac.nz>you write:
>Fergus Henderson wrote:
>	For example, Lee advocates the use of type systems for higher-order code
>	but in that paper he does not make any attempt to say how apply/3 could
>	or should be typed.
>
>I note that the call/N family was invented by me as part of the work that
>led to the Mycroft/O'Keefe type system reported in AI Journal.  I invented
>it because we tried to figure out a straightforward way to type apply/3
>and failed.

I believe you were influenced by the (non-curried) ML type scheme.
If you had started with Haskell (a bit difficult since I think it hadn't
been invented back then) it might have worked out.  One of the unfortunate
things for the intuition of relational programmers (as opposed to
functional programmers) 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 have also tried (and failed) to construct a type system which avoids the
-> pred all over the place.

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.

	lee
--------------------------------------------------------------------------
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
--------------------------------------------------------------------------