Fw: Question aboutthe use of an inner forall

[Scott J.]

Again a typo. Please read something like MutVar s Bool. Sorry   Scott   ----- Original Message ----- From: Scott J. To: Jay Cox Cc: [EMAIL PROTECTED] 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 ----- From: "Jay Cox" <[EMAIL PROTECTED]> To: "Scott J." <[EMAIL PROTECTED]>; "Haskell Cafe List" <[EMAIL PROTECTED]> Sent: Monday, August 19, 2002 5:19 AM Subject: Re: Question aboutthe use of an inner forall > > ----- Original Message ----- > From: "Ashley Yakeley" <[EMAIL PROTECTED]> > To: "Scott J." <[EMAIL PROTECTED]>; "Haskell Cafe List" > <[EMAIL PROTECTED]> > 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 > > >