[Haskell-cafe] Aren't type system extensions fun?
Ryan Ingram
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
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
More information about the Haskell-Cafe
mailing list