- Haskell-Cafe - Haskell.org

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

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