Question aboutthe use of an inner forall
Sun, 18 Aug 2002 22:19:47 -0500
----- Original Message -----
From: "Ashley Yakeley" <email@example.com>
To: "Scott J." <firstname.lastname@example.org>; "Haskell Cafe List"
Sent: Friday, August 16, 2002 11:15 PM
Subject: Re: Question aboutthe use of an inner forall
> At 2002-08-16 20:57, Scott J. wrote:
> >However what for heaven's sake should I think of
> >runST :: forall a ( forall s ST s a) -> a ?
> runST :: forall a. ((forall s. ST s a) -> a)
> "For all a, if (for all s, (ST s a)) then a."
> You may apply runST to anything with a type of the form (forall s. ST s
> a), for any 'a'.
I'm very fuzzy to the details of type theory in general so please forgive
I noted the same question as Scott's when I first learned about ST threads.
When you have a rank-2 polymorphic function, like
runST::forall a . ( forall s . ST s a) -> a
the type means the function takes an argument ***at least as polymorphic***
(forall s . ST s (some type a independent of s)). If (runST stthread ) has
type String, then stthread must at least have type ST s String.
Why do you need this apparent mumbo jumbo about Rank-2 polymorphism? It
insures your ST threads are threadsafe (or so I have been led to believe).
You will not be able to throw a mutable reference outside of the thread.
take this long interaction from ghci (the ST> is the prompt, and what
on the same line is the code entered. For instance :type gives the type of
the following code. I have separated ghci input/ouput from comments by
placing # in front of the IO).
#ST> :type newSTRef (3::Prelude.Int)
#forall s. ST s (STRef s PrelBase.Int)
The type variable a is replaced by, or a has the value of, (STRef s
PrelBase.Int). but this depends on s.
#ST> :type readSTRef
#forall s a. STRef s a -> ST s a
#ST> :type (do x<-newSTRef (3::Prelude.Int);readSTRef x)
#forall s. ST s PrelBase.Int
a here is replaced by PrelBase.Int. the code in the do statement is runnable
#ST> runST (newSTRef (3::Prelude.Int))
#Ambiguous type variable(s) `a' in the constraint `PrelShow.Show a'
#arising from use of `PrelIO.print' at <No locn>
#In a 'do' expression pattern binding: PrelIO.print it
# Inferred type is less polymorphic than expected
# Quantified type variable `s' escapes
# It is reachable from the type variable(s) `a'
# which is free in the signature
# Signature type: forall s. ST s a
# Type to generalise: ST s1 (STRef s1 PrelBase.Int)
# When checking an expression type signature
# In the first argument of `runST', namely
# `(newSTRef (3 :: PrelBase.Int))'
# In the definition of `it': runST (newSTRef (3 :: PrelBase.Int))
above is a demonstration of how the type checking prevents
using/reading/modifying references outside of the ST world.
I realize this is a bit of an incomplete explanation: Some questions I
would like to answer to help your comprehension but cannot due to my
1. how do you measure the polymorphic nature of a type so that you can say
it is "at least as polymorphic"? I have a fuzzy idea and some examples (Num
a => a vs. forall a . a vs. forall a . [a], etc.) but I haven't yet found
out for myself a precise definition.
2. what does it mean that type variable "escapes", and why is it bad? A
reasonable answer isn't popping into my head right now. Something about how
the type of a program should be fully resolved pops into my head but nothing
Maybe that helps.