- Haskell-Cafe - Haskell.org

Re: Question aboutthe use of an inner forall
by Ashley Yakeley 19 Aug '02

19 Aug '02

At 2002-08-18 20:12, Scott J. wrote: >So let's come backe to runST. > >runST ::( forall s) (ST s a )-> a > >So I insist what is the statement ST s a ? Oh it's not really a statement, it just plays a similar role in types that statements play in logic. The comparison runs something like this: type variable variable type statement type constructor function "->" implies application derivation "forall" universal quantification type specialisation specialisation For instance, in logic if you have "A" and you have "A implies B", you can derive "B". Likewise, if you have a value of type "a", and a value of type "a -> b", by using function application you can obtain a value of type "b". The type theory has the same structure as the logic, merely a different interpretation. -- Ashley Yakeley, Seattle WA

2 1

Re: Question aboutthe use of an inner forall
by Ashley Yakeley 19 Aug '02

19 Aug '02

At 2002-08-18 20:19, Jay Cox wrote: >#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 I don't understand this either, actually: $ ghci -fglasgow-exts -package lang ___ ___ _ / _ \ /\ /\/ __(_) / /_\// /_/ / / | | GHC Interactive, version 5.04, for Haskell 98. / /_\\/ __ / /___| | http://www.haskell.org/ghc/ \____/\/ /_/\____/|_| Type :? for help. Loading package base ... linking ... done. Loading package haskell98 ... linking ... done. Loading package lang ... linking ... done. Prelude> :module ST Prelude ST> :type runST Inferred type is less polymorphic than expected Quantified type variable `s' escapes Expected type: ST s a -> t Inferred type: (forall s1. ST s1 a) -> a Prelude ST> What's up with that? Can't I even look at the type? Is this the monomorphism restriction or something? -- Ashley Yakeley, Seattle WA

1 0

Fw: Question aboutthe use of an inner forall
by Scott J. 19 Aug '02

19 Aug '02

Again a typo. Please read something like MutVar s Bool. Sorry Scott ----- Original Message ----- From: Scott J. To: Jay Cox Cc: haskell-cafe(a)haskell.org 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" <sqrtofone(a)yahoo.com> To: "Scott J." <jscott(a)planetinternet.be>; "Haskell Cafe List" <haskell-cafe(a)haskell.org> Sent: Monday, August 19, 2002 5:19 AM Subject: Re: Question aboutthe use of an inner forall > > ----- Original Message ----- > From: "Ashley Yakeley" <ashley(a)semantic.org> > To: "Scott J." <jscott(a)planetinternet.be>; "Haskell Cafe List" > <haskell-cafe(a)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 > > >

1 0

Re: Question aboutthe use of an inner forall
by Ashley Yakeley 19 Aug '02

19 Aug '02

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

3 3

Re: Question aboutthe use of an inner forall
by Ashley Yakeley 19 Aug '02

19 Aug '02

At 2002-08-18 18:19, Scott J. wrote: >A question: s is not a type variable as a isn't it? Both are quantified type variables. But only one of those quantifiers can be placed at the top level of the expression. runST :: forall a. ((forall s. ST s a) -> a) > I mean a can be of type Integer while s cannot. Well yes, you can specialise "forall a" to Integer. So runST can be specialised to this type: runST ::[special] (forall s. ST s Integer) -> Integer ...whereas you cannot specialise "s" in the same way. Think of it in terms of logic, if for all a: f(a), then by simple specialisation f(Integer). -- Ashley Yakeley, Seattle WA

2 1

Re: Fw: Question aboutthe use of an inner forall
by Ashley Yakeley 19 Aug '02

19 Aug '02

At 2002-08-18 19:15, Jan Brosius wrote: >Still some question: Ok a is not a type but Integer is a type . But a can >be > instantiated to integer. This comes pretty close to call a therefore a type > variable, Isn't it? "a" is a type variable. "Integer" is a type. "forall a. a" is also a type, but frequently "forall"s at the top level are elided. -- Ashley Yakeley, Seattle WA

1 0

Fw: Question aboutthe use of an inner forall
by Scott J. 19 Aug '02

19 Aug '02

Sorry there are two mailers on this machine Regards SCott ----- Original Message ----- From: "Jan Brosius" <jscott(a)planetinternet.be> To: "Jon Cast" <jcast(a)ou.edu> Cc: <haskell-cafe(a)haskell.org> Sent: Monday, August 19, 2002 4:15 AM Subject: Fw: Question aboutthe use of an inner forall > Still some question: Ok a is not a type but Integer is a type . But a can > be > instantiated to integer. This comes pretty close to call a therefore a type > variable, Isn't it? > > And otherwise why writing forall a etc. > > Regards > > Scott > > ----- Original Message ----- > From: "Scott J." <jscott(a)planetinternet.be> > To: "Jon Cast" <jcast(a)ou.edu> > Cc: <haskell-cafe(a)haskell.org> > Sent: Monday, August 19, 2002 4:09 AM > Subject: Re: Question aboutthe use of an inner forall > > > > Still some question: Ok a is a type and Integer is a type . But a can be > > instantiated to integer. This comes pretty close to call a therefore a > type > > variable. > > > > Regards > > > > Scott > > > > ----- Original Message ----- > > From: "Jon Cast" <jcast(a)ou.edu> > > To: "Scott J." <jscott(a)planetinternet.be> > > Cc: "Ashley Yakeley" <ashley(a)semantic.org>; <haskell-cafe(a)haskell.org> > > Sent: Monday, August 19, 2002 3:48 AM > > Subject: Re: Question aboutthe use of an inner forall > > > > > > > "Scott J." <jscott(a)planetinternet.be> wrote: > > > > A question: s is not a type variable as a isn't it? I mean a can be > > > > of type Integer while s cannot. > > > > > > Guessing at your question: > > > > > > a has no type (and neither does s); it /is/ a type. In Haskell, types > > > have kinds. And, both a and s have kind *. > > > > > > Now then, the user can instantiate a to Integer, yes. And the user > > > cannot instantiate s to anything---that's what the `forall' is for. > > > runST will (theoretically) instantiate s to something. That could be > > > Integer if the language implementors felt like it. The user of runST > > > certainly has to be prepared for the possibility. > > > > > > Does that come close to answering your question? > > > > > > > Regards, > > > > > > > Scott > > > > > > Jon Cast > > > _______________________________________________ > > > Haskell-Cafe mailing list > > > Haskell-Cafe(a)haskell.org > > > http://www.haskell.org/mailman/listinfo/haskell-cafe > > > > > > > _______________________________________________ > > Haskell-Cafe mailing list > > Haskell-Cafe(a)haskell.org > > http://www.haskell.org/mailman/listinfo/haskell-cafe > > >

1 0

Fw: Question aboutthe use of an inner forall
by Jan Brosius 19 Aug '02

19 Aug '02

Still some question: Ok a is not a type but Integer is a type . But a can be instantiated to integer. This comes pretty close to call a therefore a type variable, Isn't it? And otherwise why writing forall a etc. Regards Scott ----- Original Message ----- From: "Scott J." <jscott(a)planetinternet.be> To: "Jon Cast" <jcast(a)ou.edu> Cc: <haskell-cafe(a)haskell.org> Sent: Monday, August 19, 2002 4:09 AM Subject: Re: Question aboutthe use of an inner forall > Still some question: Ok a is a type and Integer is a type . But a can be > instantiated to integer. This comes pretty close to call a therefore a type > variable. > > Regards > > Scott > > ----- Original Message ----- > From: "Jon Cast" <jcast(a)ou.edu> > To: "Scott J." <jscott(a)planetinternet.be> > Cc: "Ashley Yakeley" <ashley(a)semantic.org>; <haskell-cafe(a)haskell.org> > Sent: Monday, August 19, 2002 3:48 AM > Subject: Re: Question aboutthe use of an inner forall > > > > "Scott J." <jscott(a)planetinternet.be> wrote: > > > A question: s is not a type variable as a isn't it? I mean a can be > > > of type Integer while s cannot. > > > > Guessing at your question: > > > > a has no type (and neither does s); it /is/ a type. In Haskell, types > > have kinds. And, both a and s have kind *. > > > > Now then, the user can instantiate a to Integer, yes. And the user > > cannot instantiate s to anything---that's what the `forall' is for. > > runST will (theoretically) instantiate s to something. That could be > > Integer if the language implementors felt like it. The user of runST > > certainly has to be prepared for the possibility. > > > > Does that come close to answering your question? > > > > > Regards, > > > > > Scott > > > > Jon Cast > > _______________________________________________ > > Haskell-Cafe mailing list > > Haskell-Cafe(a)haskell.org > > http://www.haskell.org/mailman/listinfo/haskell-cafe > > > > _______________________________________________ > Haskell-Cafe mailing list > Haskell-Cafe(a)haskell.org > http://www.haskell.org/mailman/listinfo/haskell-cafe >

1 0

Re: Question aboutthe use of an inner forall
by Jon Cast 19 Aug '02

19 Aug '02

"Scott J." <jscott(a)planetinternet.be> wrote: > A question: s is not a type variable as a isn't it? I mean a can be > of type Integer while s cannot. Guessing at your question: a has no type (and neither does s); it /is/ a type. In Haskell, types have kinds. And, both a and s have kind *. Now then, the user can instantiate a to Integer, yes. And the user cannot instantiate s to anything---that's what the `forall' is for. runST will (theoretically) instantiate s to something. That could be Integer if the language implementors felt like it. The user of runST certainly has to be prepared for the possibility. Does that come close to answering your question? > Regards, > Scott Jon Cast

2 1

Question aboutthe use of an inner forall
by Scott J. 17 Aug '02

17 Aug '02

Hi, It goes about the State tansformer monad ST s a. I think how it works but as a logician the use of an internal forall is difficult to swallow. Let's first see a statement in Haskell. One can type foo :: a -> b as a function We can be not sloppy (but this gives unnecessary clutter in the program I think) and type it as: forall a,b foo :: a -> b Now this is a statement in logic, it can be true or false. However what for heaven's sake should I think of runST :: forall a ( forall s ST s a) -> a ? In logic forall x forall y statement(x.y) is equivalent to: forall y forall x statement(x,y). Why the use of the inner forall in runST?This is not a normal function declaration in mathematics. Since Haskell is Hindley-Milner typed and can't use an inner forall . Why the use an inner forall. Has imagination dried up (sorry, if this seems impolite)? Thx Scott

1 0