[Haskell-cafe] Aren't type system extensions fun?
ryani.spam at gmail.com
Tue May 27 19:22:49 EDT 2008
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
Another example that I personally am attached to is Prompt:
(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
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.
More information about the Haskell-Cafe