[mercury-users] The Logic of Mercury

[Richard A. O'Keefe]

I explained briefly why call/N was invented for
the Mycroft/O'Keefe type system.  Lee Naish replied:
	
	I believe you were influenced by the (non-curried) ML type scheme.

Most certainly we were influenced by the ML type system.
I wanted a type system because Leon Sterling's Boyer-Moore-style
theorem prover failed to prove some obvious properties of Prolog
predicates, and the prover was *right* because the predicates
didn't *have* those properties, but typed versions did.
Alan Mycroft wanted a type system for Prolog because he had a
Hope-to-Prolog translator he wanted type-checking for (or was
it an ML subset to Prolog?  I don't remember any more).  I had
to twist his arm a bit to remove claims from the paper that
were true about ML but false about Prolog; those claims turn
out to be true about Mercury thanks to modes.

However, it is nonsense to call the ML type system "non-curried".
ML has always supported curried function definitions and the
Hindley/Milner type system has always handled them just fine.
ML *style* in the SML Basis Library tends to avoid curried functions,
but they are *there*, just as Haskell and Clean support uncurried
functions.

	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: [sic]
	
	append :: list(T) -> list(T) -> list(T) -> pred
	',' :: pred -> pred -> pred
	
This type is obvious and was equally obvious back in 1984.
Haskell may not have been around, but the pure lambda calculus _was_,
and Alan Mycroft and I were adequately informed about it.
I deny that it is "BEST to treat predicates" this way because I
deny that the asymmetry involved is appropriate.  I have frequently
used append/3 "backwards", for which the type (in an ad hoc notation)
	set(list(T) * list(T)) <- list(T)
is a better conceptual fit.  In a previous message I demonstrated
that splitting off the leftmost argument is not always the best fit
for functions either.

I note that the approach taken in most functional languages (Erlang is
a notable exception) means that the arity of a function is part of its
type, not its name, so you cannot have

    append([], []).
    append([X|Xs], Ys0) :-
        append(X, Ys1, Ys0),
        append(Xs, Ys1).

as well as the usual append/3.  Some imperative languages in which
routine names are simple identifiers have exploited this to allow
optional and/or keyword parameters.  There are good software engineering
reasons why Ada has optional and keyword parameters.  The lack of
keyword parameters has been a long-standing *practical* niggle in
Prolog.  I've thought about combining keyword parameters with currying,
but there are some nasty little inference problems.  One of the design
goals for Mercury is that you should be able to offer it to a software
engineer with a straight face.  I believe that keyword parameters would
be more practical use than currying, and would even do more to support
re-use than currying.
--------------------------------------------------------------------------
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
--------------------------------------------------------------------------