[Haskell-cafe] Aren't type system extensions fun?

[Ryan Ingram]

On 5/26/08, Andrew Coppin <andrewcoppin at btinternet.com> wrote:
> This is probably the first real use I've ever seen of so-called rank-2
> types, and I'm curios to know why people think they need to exist.
> [Obviously when somebody vastly more intelligent than me says something is
> necessary, they probably know something I don't...]

The usual example I've seen for "beauty in rank-2 types" is the ST monad.

ST lets you define 'stateful' imperative algorithms with destructive
update, but be able to call them safely from pure-functional code.

This is made safe by a "phantom" type variable and the rank-2 type of runST:

> runST :: forall a. (forall s. ST s a) -> a

The "s" in ST logically represents the "initial state" used by the
imperative computation it represents; it tracks any allocations and
updates that need to be made before the computation can run.  By
requiring that the passed in computation works for *any* initial
state, you guarantee that it can't reference any external store or
return data from within the store; for example, consider this:

> newSTRef :: forall s a. a -> ST s (STRef s a)

> mkZero :: forall s. ST s (STRef s Int)
> mkZero = newSTRef 0

Now consider trying to type "runST mkZero"; first we generate a new
type variable "s1" for the "s" in mkZero, then use it to instantiate
the result type, "a":

runST :: (forall s. ST s (STRef s1 a)) -> STRef s1 a

Now we need to unify s1 with s to match mkZero's type for the first
argument.  But we can't do that, because then "s" escapes its forall
scope.  So we can statically guarantee that no references escape from
runST!

---

Another example that I personally am attached to is Prompt:
http://hackage.haskell.org/cgi-bin/hackage-scripts/package/MonadPrompt

(There's no Haddock documentation on that site, but the source code is
well-commented and there's a module of examples).

The function I want to talk about is "runPrompt"

> prompt :: forall p a. p a -> Prompt p a
> runPrompt :: forall p r. (forall a. p a -> a) -> Prompt p r -> r

Lets instantiate p and r to simplify things; I'll use [] for p and Int for r.

> test1 :: Prompt [] Int
> test1 = prompt [1,2,3]

> test2 :: Prompt [] Int
> test2 = do
>    x <- prompt ['A', 'B', 'C']
>    return (ord x)  -- ord :: Char -> Int

Now, the type of runPrompt specialized for these examples is
> runPrompt :: (forall a. [a] -> a) -> Prompt [] Int -> Int

Notice that we need to pass in a function that can take -any- list and
return an element.  One simple example is "head":
> head :: forall a. [a] -> a
> head (x:xs) = x

So, putting it together:

ghci> runPrompt head test1
1
ghci> runPrompt head test2
65  -- ascii code for 'A'.

Now, this isn't that great on its own; wouldn't it be useful to be
able to get some information about the type of result needed when
writing your prompt-handler function?  Then you could do something
different in each case.

That's a question for another topic, but to get you started, start
looking around for information on GADTs.

  -- ryan