I just started learning a functional/logic language called Mercury, which has features that make it feel (at least to my initial impressions) like a mix between Prolog and Haskell. It has all the features that make it a viable Prolog, but it also adds static typing (with full type inference) and purity (all side effects are dealt with by passing around the state of the world). Since I recently was interested in learning Prolog, but had no desire to give up static typing or purity, Mercury seemed like a neat thing to learn.

While it is not very well known, the language has been around for over 15 years, and has a high quality self-hosting compiler.

Getting to play around with logic/declarative programming is interesting (and indeed the main reason why I’m interested in learning it), but what seems even more interesting with Mercury is how they have incorporated typing to the logic programming (which, unless I’m mistaken, is a new thing). As a tiny code example:

:- pred head(list(T), T). 
:- mode head(in,    out) is semidet. 
:- mode head(in(non_empty_list), out) is det.
head(Xs, X) :- Xs = [X | _].

The first line says that this is a predicate (logic statement) that has two parts, the first is a list of some type T (it is polymorphic), the second is an item of type T.

The fourth line should be familiar to a prolog programmer, but briefly, the right side says that Xs is defined as X cons’d to an unnamed element. head can be seen as defining a relationship between Xs and X, where the specifics are that Xs is a list that has as it’s first element X.

Now with regular prolog, only the fourth line would be necessary, and that definition allows some interesting generalization. Because head([1,2,3],Y) will bind Y to 1, while head([1,2,3],1) will be true (or some truthy value), and if head(X,Y) were used in a set of other statements, together they would only yield a result if X (wherever it was bound, or unified, to a value) had as it’s first value Y, whatever Y was.

Since Mercury is statically typed, it adds what it calls modes to predicates, which specify whether a certain argument (that’s probably not the right word!) is going to be given, or whether it is going to be figured out by the predicate. The other thing it has is specifications about whether the predicate is deterministic. There are a couple options, but the two that are relevant to this example are det, which means fully deterministic, for every input there is exactly one output, and semidet, which means for some inputs there is an output, for others there is not (ie, the unification fails). These allow the compiler to do really interesting things, like tell you if you are not covering all of the possible cases if you declare something as det (whereas the same code, as semidet, would not cause any errors).

What is fascinating about this predicate head is that it has two modes defined, one being the obvious head that we know from Haskell etc:

:- mode head(in,    out) is semidet. 

Which states that the first argument is the input (the list) and the second is the output (the element), and it is semidet because for an empty list it will fail. The next is more interesting:

:- mode head(in(non_empty_list), out) is det.

This says for an input that is a non_empty_list (defined in the standard libraries, and included below), the second argument is the output, and this is det, ie fully deterministic. What this basically means is that failure is incorporated into the type system, because something that is semidet can fail, but something that is det cannot (neat!). Now the standard modes are defined (something like):

:- mode in == (ground >> ground).
:- mode out == (free    >> ground).

Ground is a something that is bound, and the >> is showing what is happening before and after the unification (the analog to function application). So something of mode in will be bound before and after, whereas something of mode out will not be bound before (that’s what free means) and it will be bound afterwards. That’s pretty straightforward.

What get’s more interesting is something like non_empty_list, where inst stands for instantiation state, ie one of various states that a variable can be in (with ground and free being the most obvious ones):

:- inst non_empty_list == bound([ground | ground]).

What this means is that a non_empty_list is defined as one that has a ground element cons’d to another ground element. (I don’t know the syntax well enough to explain what bound means in this context, but it seems straightforward). What this should allow you to do is write programs that operate on things like non-empty-lists, and have the compiler check to make sure you are never using an empty list where you shouldn’t. Pretty cool!

Obviously you can write data types in Haskell that also do not allow an empty list, like:

data NonEmptyList a = NonEmptyList a [a]

And could build functions to convert between them and normal lists, but the fact that it is so easy to build this kind of type checking on top of existing types with Mercury is really fascinating.

This is (obviously) just scratching the surface of Mercury (and the reason all of this stuff actually works is probably more due to the theoretical underpinnings of logic programming than anything else), but seeing the definition of head gave me enough of an ‘aha!’ moment that it seemed worth sharing.

If any of this piqued your interest, all of it comes out of the (wonderful) tutorial provided at the Mercury Project Documentation page. If there are any inaccuracies (which there probably are!) send them to daniel@dbpatterson.com.