Re: Question aboutthe use of an inner forall - Haskell-Cafe - Haskell.org

newer
Fw: Question aboutthe use of an...

Re: Question aboutthe use of an inner forall

older
Re: Question aboutthe use of an...

Ashley Yakeley

17 Aug 2002 17 Aug '02

12:15 a.m.

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'. -- Ashley Yakeley, Seattle WA

Reply

Sign in to reply online Use email software

Show replies by date

Scott J.

18 Aug 18 Aug

9:19 p.m.

New subject: Question aboutthe use of an inner forall

A question: s is not a type variable as a isn't it? I mean a can be of type Integer while s cannot. Regards, Scott ----- Original Message ----- From: "Ashley Yakeley" To: "Scott J." ; "Haskell Cafe List" Sent: Saturday, August 17, 2002 6:15 AM 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'.

-- Ashley Yakeley, Seattle WA

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

Reply

Sign in to reply online Use email software

Jay Cox

11:19 p.m.

New subject: Question aboutthe use of an inner forall

----- Original Message ----- From: "Ashley Yakeley" To: "Scott J." ; "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 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

Reply

Sign in to reply online Use email software

Scott J.

11:41 p.m.

New subject: 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" To: "Scott J." ; "Haskell Cafe List" Sent: Monday, August 19, 2002 5:19 AM Subject: Re: Question aboutthe use of an inner forall

----- Original Message ----- From: "Ashley Yakeley" To: "Scott J." ; "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 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

Reply

Sign in to reply online Use email software

8311

Age (days ago)

8313

Last active (days ago)

Download

3 comments

3 participants

tags

participants (3)

Ashley Yakeley
Jay Cox
Scott J.