Tue, 2 May 2000 22:47:08 +0200, Jan Brosius <[EMAIL PROTECTED]> pisze:
> First I want to end this with the following observation : if the
> forall in ( forall s1 . ST s1 T(s) ) really had the meaning
> of the logical forall , that is if " forall s1 . ST s1 T(s)
> is true then the case ST s T(s) i.e. the case for s1 = s is
> also true.
Wrong implication. "forall s. ST s T(s)" is not an instance (result
of some variable substitution) of "forall s1. ST s1 T(s)". Variable
substitution is not a textual replacement, because variables are
lexically scoped - you cannot rebind a variable to a different
qualifier and say that it's the same thing.
"forall s1. ST s1 T(s)" does not imply "forall s. ST s T(s)".
Let's move to another domain. "forall x. x+a > x" does not imply
"forall a. a+a > a" when variables denote real numbers. For example
when "a" (bound somewhere outside) equals 1, then the first sentence
is true and the second is false.
It's the same with runST.
> runST :: (forall s . ST s a ) -> a
>
> What sort of sentence could be meant by this?
Let's rewrite it by making foralls explicit:
runST :: forall a. (forall s. ST s a) -> a
It means that ST is a function that can be instantiated for any "a",
takes a value of type "ST s a" which can be instantiated for any "s",
and returns a value of type "a".
I don't see any problem with this. There exists no type "a" for which
you could use runST to apply it to a value of type "forall s. ST s [s]".
> If we accept this we can now give the following type signature for runST
>
> runST:: forall a . forall s ni FreeV( a ) . ST s a -> a
If you mean parentheses put such:
runST :: forall a . forall s ni FreeV( a ) . (ST s a -> a)
then this is wrong, because when we take a = Int and s = RealWorld,
runST could have the type ST RealWorld Int -> Int, which must not be
possible, because a value of type "ST RealWorld Int" may describe
a computation that has I/O effects.
If you mean parentheses put such:
runST:: forall a . (forall s ni FreeV( a ) . ST s a) -> a
then it's exactly the same as currently. "forall s" introduces a
fresh type variable "s". It cannot be bound in some type outside
by definition.
--
__("< Marcin Kowalczyk * [EMAIL PROTECTED] http://qrczak.ids.net.pl/
\__/ GCS/M d- s+:-- a23 C+++$ UL++>++++$ P+++ L++>++++$ E-
^^ W++ N+++ o? K? w(---) O? M- V? PS-- PE++ Y? PGP+ t
QRCZAK 5? X- R tv-- b+>++ DI D- G+ e>++++ h! r--%>++ y-
