What uses have you found for higher-rank types in Haskell? [closed]

Question

Closed. This question needs to be more focused. It is not currently accepting answers.

---

Want to improve this question? Update the question so it focuses on one problem only by editing this post.

Closed last month.

Improve this question

Higher rank types look like great fun. From the Haskell wikibook comes this example:

foo :: (forall a. a -> a) -> (Char,Bool)
foo f = (f 'c', f True)

Now we can evaluate foo id without the compiler exploding. This example is quickly followed in the book by the real-world example I have seen in a few other places: the ST monad and runST. That's pretty cool.

But I have yet to come across a situation where I solve a problem by writing my own function with an argument of higher-rank. Have you? What examples do you have of rank-2 or rank-n polymorphism in the wild?

Answer 1

Weirich and Washburnn's "Boxes go Bananas"! (paper, slides)

Here is a very crude and probably slightly inaccurate explanation of what it's all about: given an inductive type, BGB lets you represent the space of functions from that type which are "positive" -- they never case-discriminate on their arguments. At most they include their arguments as part of other values (usually of the same type).

Weirich+Washburn use this to get a probably-adequate HOAS representation of the lambda calculus in -XRankNTypes Haskell (has anybody proven it adequate yet?).

I use it here (warning: messy code) to turn a

(forall g . GArrow g => g () x -> g () y)

into a

(forall g . GArrow g => g x y)

This works because the rank-2 polymorphic type can't "inspect" the structure of its argument -- all it can do is "paste" that argument into bigger structures. Some trickery lets me figure out where the pasting happens, and then I thread the pasting point(s) (if any) back out to the input of the GArrow.

You can't do this with the Control.Arrow class, because the whole Haskell function space "leaks" into it via arr.

Answer 2

Take a look at functions like withRepoLock in the Darcs source.

Darcs has support for multiple repository formats, and that support is expressed via a typeclass. So you can write code that is generic over repository formats. When actually reading an on-disk repository you want to dispatch to that code through some common code that figures out what format the repository is in and chooses the right typeclass instantiation.

Answer 3

It may be that you have encountered problems where higher ranked types would be useful, but failed to realise it. For instance in the Darcs example they could easily have implemented it without higher ranked types. Instead there would have been preconditions on some functions that the caller would have to make sure they comply with, such as choosing the right instantiation of a function for the repository format.

The advantage of the higher ranked type is that it transfers responsibility for getting this right from the programmer to the compiler. With the conventional approach, if a Darcs developer made a mistake with the repository type the result would either be a run-time error or else corrupted data. With the higher ranked type the developer gets a type error at compile time.

Answer 4

A relatively-simple example of higher-ranked types in action can be found in Luke Palmer's IO-free splittable supply - he shows how to make the use of simple unique-value supplies easier:

runSupply :: (forall a. Eq a => Supply a -> b) -> b