:: (Bloggable a) => a -> IO ()

In type theory, the existential quantifier, $$\exists$$ is the dual to the more familiar universal quantifier, $$\forall$$ (which expresses parametric polymorphism). Believe it or not, these existentially quantified types can be useful in day-to-day programming in languages like Haskell where you wish to perform some kind of “information hiding”. As a simple example, consider this program:

data Showable = forall a. Show a => MkShowable a

We start off by declaring a datatype, Showable, with a single constructor, MkShowable that has type $$\forall \alpha. (\text{S}\text{how}~\alpha) \Rightarrow \alpha \rightarrow \text{S}\text{how}\text{able}$$. This is to say, it injects any value with a Show instance into the Showable type.

This is really an existentially quantified datatype. However, many newbies are confused by this pronouncement, as it quite clearly uses the forall keyword, which introduces universal quantification – I’ll come back to that at the end of this article.

instance Show Showable where
    show (Showable x) = show x

This next chunk of code declares that any value of type Showable is itself a member of the Show type class. We implement it by unpacking the Showable value and applying show “recursively” to that value. We are able to do this precisely because of the constraint in the MkShowable constructor that specified that whatever type gets injected into Showable must have a Show instance somewhere.

An aside: this construction has something of the flavour of object orientation, as it implements a uniform interface using dynamic dispatch. I’ll leave it up to the inimitable Oleg to expand on this point…

showable_stuff :: [Showable]
showable_stuff = [MkShowable 1337, MkShowable "I'm a string!", MkShowable 3.1415]

Here we make use of the marvellous information-hiding properties of the existential to create a list holding values of varying types. All we can know about the elements of the resulting list is that they certainly have a Show instance.

main = mapM_ print showable_stuff

This last declaration is just a bit of top-level gunk that outputs all the things in that list to the screen using the Show typeclass.

So, that’s a pretty interesting technique. But in precisely what sense is it existential, given that we got all this going by using the universal quantifier (the forall keyword)? I think the easiest way to look at this problem is using the marvellously useful Curry-Howard correspondence between types and terms in a logic system.

First, remember than the function arrow at the type level ($$\tau_1 \rightarrow \tau_2$$) just corresponds to implication in proofs, and the quantifiers carry through unchanged. Secondly, remember that in the proof system corresponding to simple ML-style types (second-order intuionistic logic) $$\sigma_1 \rightarrow \sigma_2 \equiv \lnot \sigma_1 \lor \sigma_2$$. Thirdly, recall that if $$\alpha$$ is free in $$\sigma_2$$ then $$\forall \alpha. \sigma_1 \lor \sigma_2 \equiv (\forall \alpha. \sigma_1) \lor \sigma_2$$. Finally, you need to know that pushing a negation through an existiental or universal quantifier flips the kind of quantifier we have (the statement that an $$x$$ does not exist satisfying $$P$$ is equivalent to saying that all $$x$$s do not satisfy $$P$$). Now we can gradually manipulate the type of a simple data constructor function into a form that makes it obvious where the existiential comes from. Let’s try this example (which doesn’t have any typeclasses, since they don’t really fit into the classical correspondence):

data K = forall a. MkK a

So MkK has type $$\forall \alpha. \alpha \rightarrow K$$. Let’s push that into the realm of logic and proof and see what we can do:

$$!\begin{array}{ccc}\forall \alpha. \alpha \rightarrow K &=& \forall \alpha. \lnot \alpha \lor K\\ &=& (\forall \alpha. \lnot \alpha) \lor K\\ &=& \lnot (\exists \alpha. \alpha) \lor K\\ &=& (\exists \alpha. \alpha) \rightarrow K\end{array}$$

And we’re done! We can extract this last proof term back out as a type in our source language without any fuss, and hence from only a few logical rules (which, if you didn’t know them, are fairly easy to convince yourself of) we have derived why these constructs are known as “existential”. In fact, some Haskell compilers once supported the exists keywoard to let you declare them directly, but due to precisely this correspondence between the two quantifiers GHC dropped the extra keyword in favour of just using the forall to do both jobs.

As my final year undergraduate project I’ve implemented Philip Wadler’s and Simon Peyton Jones’ Comprehensive Comprehensions in the Glasgow Haskell Compiler. I’m happy to report that my patch was accepted for inclusion in the compiler, so this is a feature you’ll really be able to use come the release of 6.10!

So, what are comprehensive comprehensions? Well, first let’s just review what list comprehensions are:

triples = [(a,b,c) | a <- [1..20]
                   , b <- [a..20]
                   , let sum = a^2 + b^2
                   , c <- [b..20]
                   , sum == c^2]

This Haskell code draws numbers from 1 to 20 into the variable a, and for each one of those elements draws the numbers from a to 20 into b. We then compute the sum of the squares of each of those numbers, and finally give up in all but the case where we can find some c in the range from b to 20 such that that sum is the same as the square of c. Assuming that we have passed this test, we output a tuple containing a, b and c. Clearly, this implements some code for finding small Pythagorean triples.

So, the result will be:

[(3,4,5), (5,12,13), (6,8,10), (8,15,17), (9,12,15), (12,16,20)]

We can build an analogy between what we can do with list comprehensions and what we can do with parts of SQL. Drawing an item from a list is like SELECTion, filtering out certain items is similar to a WHERE clause and so on. However, there are some prominent features of SQL that aren’t so easy to express with just these vanilla list comprehensions. How could we write the following query in Haskell?

SELECT Name, SUM(Salary)
FROM Employees
GROUP BY Dept
ORDER BY SUM(Salary) ASC
LIMIT 5

Well, the answer is that we can use our lovely new generalized list comprehensions and write this:

[(the dept, sum salary)
  | (name, dept, salary) <- employees
  , then group by dept
  , then sortWith by sum salary
  , then take 5]

Notice that the existing keyword “then” is being used to introduce the sorting and grouping functionality that we require: this happens to be a bit different from the syntax in the paper, so be careful you don’t get caught out by this.

What isn’t obvious from the presentation above is just how general these comprehensive comprehensions are! Unlike SQL you can sort or group at any point in the query without making use of subqueries. Unlike SQL you can use any aggregation function, not just one it has defined like COUNT or SUM. Most significantly, unlike SQL you can actually use alternative grouping and sorting functions! So, you could choose a grouping function that actually looked for runs in the thing you are grouping by, or a “sorting” function that just returns the first 5 elements of the list: if you look at the example above we used just this feature to implement the LIMIT clause of SQL.

These new pieces of syntax are pretty nice, and speaking from personal experience it’s quite hard to do heavy duty list manipulation without them once you’ve grown used to having them available. In particular, I found them to have a killer application in the code I used for benchmarking the syntax extension, for slicing and dicing lists of the runtime and heap usage of various program runs.

If you want the full story on how to use the syntax, you can check out the documentation. Go forth and conquer with your new, readable, list-munging powers! I’ll leave you with a picture of the guys you have it all to thank for, those giants of functional programming Simon Peyton Jones and Philip Wadler:

Welcome to the first in what I hope will be an ongoing series of blog posts on research in functional programming. I see a lot of really neat papers come and go that show the great things that are happening in this design space, and I’m hoping to open their discoveries to a slightly wider audience by providing more what I hope are readable descriptions of them for people who don’t have the time to trawl through 20 pages or so. By using examples liberally I hope I can provide an alternative to the sometimes rather dry language of the abstracts. Anyway, that explained we can get on with the show!

A really cute paper just came up on Lambda the Ultimate, about the implementation of a new feature in the .NET functional programming language F# called Active Patterns. The basic idea is to let you pattern match not just structurally, like this:

> data Animal = Armadillo String
| Mink String
| FunctionalProgrammer String Integer
>
> show (Armadillo name) = name
> show (Mink name) = name
> show (FunctionalProgrammer name iq) = name ++ “, IQ of ” ++ (show iq)

But also FUNCTIONALLY, by letting you define your own match functions:

> (|Text|Element|) xmlNode = if xmlNode.ContentType = Text then Text (xmlNode.Text) else Element (xmlNode)
>
> match myXMLNodeInstance of
> Text s -> print (“Looks like a text node containing ” ++ (show s))
> Element e -> print (“Hmm, it’s something else!”)

And actually it goes beyond this because your pattern matching functions can receive arguments before the data you actually want to pattern match on, or can be partial functions (i.e. fail to pattern match on some inputs). Their “curried” nature lets the authors of the paper define a function which lets them write a pattern matching on the Nth bit of an integer, and on that integer rotated N times, where N is potentially supplied at runtime. This clearly has great potential for expressiveness!

I think that’s quite enough about active patterns, but I must say that I’m quite tempted to go and add F# to my repetoire now . Coming up next time, possibly: data parallel Haskell (concurrency for free!) or constructor tagging (cute optimisation for lazy functional languages).