Again a typo. Please read something like MutVar s
Bool. Sorry
Scott
----- Original Message -----
Sent: Monday, August 19, 2002 5:41 AM
Subject: Re: Question aboutthe use of an inner forall
Well I don't feel alone anymore.
Here follows how I think runST :: (forall s. ST s
a) -> a works:
if a is represented by e.g.
MutVar s a . Then the compiler complains because it did
find an s in the "data" represented by a. This
s must first be eliminated by some other combinators(?) .
I agree that something must be written for the
argument of runST to warn programmers about the possible "representations" of a.
But I still have problems that one has chosen
forall.
Scott
----- Original Message -----
Sent: Monday, August 19, 2002 5:19 AM
Subject: Re: Question aboutthe use of an inner
forall
>
> ----- Original Message -----
> From: "Ashley Yakeley"
<ashley@semantic.org>
> To:
"Scott J." <jscott@planetinternet.be>; "Haskell
Cafe List"
> <haskell-cafe@haskell.org>
> 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
> any errors.
>
> 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***
> as
> (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
> follows
> 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
> with runST
>
> #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
> #
> #<interactive>:1:
> #
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
> ignorance are:
>
> 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
> cohesive.
>
> Maybe
that helps.
>
> Jay Cox
>
>
>