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-thr... 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