- Haskell-Cafe - Haskell.org

Question about the use of an inner forall
by Scott J. 19 Aug '02

19 Aug '02

Hi, I am going to stop this discussion . What counts for me at this moment is that I know how it works. I thank everybody who replied to my email. As for the discussion about Curry Howard isomorphism and more about type theory, I shall gladly discuss these things further but than in private email. Hey, I hope really that I know how it works but this seems to be confirmed in these emails. I left Ocamel for Haskell for it's more functional approach. I think documentation about the features extending Haskell 98 is very needed for those who want only to program with the language Haskell. Thx for all replies Scott

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: > 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(?). Right. The `s' is appearing outside the area it is defined in. > 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. `forall' and `Pi' are the basic names for this sort of thing in type theory. See the discussion of the Howard-Curry isomorphism for `forall'. You probably don't want to know about `Pi'. > Scott Jon Cast

1 0

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

19 Aug '02

Jay Cox <sqrtofone(a)yahoo.com> wrote: > From: "Ashley Yakeley" <ashley(a)semantic.org> > > 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)). I'm not sure I understand polymorphic types, but here's my best guess: Polymorphic types form a sub-typing system, with the basic sub-typing judgment: (forall a. S) < [T/a]S where T and S are types, and a may occur free in S, and (<) is the sub-typing relation. From this comes the typing judgment S < T x :: S ----------------- x :: T For the purposes of runST, we only need to worry about one other judgment, the standard judgment for sub-typing function arguments: S < T ------------------- (T -> R) < (S -> R) Justification: basically, the sub-typing statement (S < T) says that every element of S is an element of T. The typing statement (f :: S -> R) says that f can take any value of type S and deliver a value of type R (divergence is a value in Haskell!). Now, if every element of S is an element of T, and f can take every element of T, it follows that f can take every element of S. (x :: S) -> (x :: T) (x :: T) -> (f x :: R) ---------------------------------------------------- (x :: S) -> (f x :: R) is an equivalent way of stating the above judgment. So, runST's types are the super-types of (forall a. (forall s. ST s a) -> a), which means all functions types for which the argument is a super-type of (forall s. ST s a). Does that clarify things any? <snip> Jon Cast

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: > Ok, a and s are type variables. It may be common usage for computer > people Bingo. You're trying to impose a non-CS understanding on a CS statement. If you're familiar with the analogy, it's like a French speaker trying to insist that ``demand'' in English cannot mean an insistence, since it doesn't mean that in English. > but for someone with a math background it is difficult Get used to difficulty. Seriously. > to call forall a a type . In logic one expects a statement in the > scope of forall a like this forall a is not a type (nor a statement) :) It's a phrase in any number of languages, including formal logic and type theory (and it has different, although cognate, meanings in those languages). > (forall a) statement. The statement may or may not depend on a. True. But if you have (forall a. type), that doesn't fit your form. And, just like (forall a. statement) is a statement, (forall a. type) is a type. Easy, no? > So let's come backe to runST. > runST ::( forall s) (ST s a )-> a May I ask a favor? If you're going to discuss type theory, learn our notation: > runST :: (forall s. ST s a) -> a Just a minor nit. > So I insist what is the statement ST s a ? It's not a statement, and forall s. is not a logic quantifier. ST s a is a type, and forall s. is a type quantifier. > Scott Jon Cast

1 0

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

19 Aug '02

Jan Brosius <jscott(a)planetinternet.be> 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? > And otherwise why writing forall a etc. If s, t are types, the type s -> t says ``give me a value of type s, and I'll give you a value of type t''. If a is a type variable, and (given a is a type) s is a type, then forall a. s says ``give me a type t, and I'll give you a value of type s[t]''. More specifically, if you write > f :: a -> b f has the form (\ x :: a -> (y :: b)), where the \ binds values. If you write > f :: forall a. a f has the form (/\ a -> (x :: a)), where the /\ binds types. Now, runST's argument has type forall s. ST s a. In other words, it's essentially a function over types---and it has to take /any/ type runST wants to hand it. > Regards > Scott Jon Cast

1 0

Newbie question, installing hugs on redhat 7.2
by S H 19 Aug '02

19 Aug '02

I'm trying to install the current version of hugs on a red hat 7.1 system (running on VMWare 2.0.1 on top of Win 2K). I downloaded the file hugs98-Dec2001-1.i386.rpm onto the freshly-installed red hat 7.1 (no other software has been installed). It complains that libreadline.so.4 is needed. The system has the package readline-4.1-9 installed which provides libreadline.so.4.1. It appears to require exactly libreadline.so.4 (not >= 4). So, I tried uninstalling readline-4.1-9 so as to install the older package but it complained (unsurprisingly) that lots of packages rely on readline so it wouldn't erase it. I could try a --force with the erase but that seems a tad drastic. Does anyone know a workaround for this, or please tell me if I'm just doing something stupid. Thanks! Simon Handley Palo Alto, CA, USA __________________________________________________ Do You Yahoo!? HotJobs - Search Thousands of New Jobs http://www.hotjobs.com

4 3

The Curry-Howard Isomorphism
by Leon Smith 19 Aug '02

19 Aug '02

For an explanation why runST has the type it does, see page 4 of Simon Peyton-Jones and John Launchbury's paper "Lazy functional state threads" http://research.microsoft.com/Users/simonpj/Papers/lazy-functional-state-th… On Friday 16 August 2002 23:57, Scott J. wrote: >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). True, but that isn't runST's type. "forall a" quantifies over the entire type, whereas "forall s" quantifies over the left hand side of the implication. In other words, you have "forall a. statement(a)", where statement includes a substatement "forall s. substatement(s,a)" Now, using a different argument, since "s" does not appear free on the R.H.S of the implication, "forall s" can be moved outside the implication to quantify over the entire type. However, this brings up an important point about the Curry-Howard Isomorphism, which basically says that types are statements in first-order logic, and the corresponding values are proofs of those statements. When we work in logic, we care mainly about the *statements*. Proofs are ways of justifying new statements. Equivalent statements are in a sense "equal", and can usually be freely substituted for each other. When we have a statement such as P /\ Q, where P and Q are statements such as "John is wearing a kilt" and "John is Scottish", it doesn't really matter which order they come in. Mathematicians generally understand that /\ is commutative, and thus we can use P /\ Q and Q /\ P interchangeably throughout our discussion. (Unless you are writing proofs in certain highly formal proof systems, such as Coq, Isabelle, or Haskell's type system) When we work in type theory, we care mainly about the *proofs*. Statements are ways of constraining our proofs to ensure they are at least somewhat sensible. When we have a type (Int, Char), where Int is the statement "my value is a 32-bit integer", and Char says "my value is a character", order does matter. Here, (4,'H') is a "proof" of the proposition (Int,Char), and ('H', 4) is a proof of the proposition (Char, Int). Although (Int, Char) <=> (Char, Int) are logically equivalent, (4,'H') is a different value than ('H', 4). This equivalence can be "proven" using the function: swap :: (a,b) -> (b,a) swap (x,y) = (y, x) Which, using the Curry-Howard isomorphism, is also a proof that /\ is commutative. In short, just because a type "a" implies type "b", and type "b" implies type "a", doesn't mean they are interchangeable as statements are in logic. Hope this helps, leon

1 0

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