Wed, 3 May 2000 13:04:32 +0200, Jan Brosius <[EMAIL PROTECTED]> pisze:
> So I looked to the example below:
>
> forall x . x + a > x is not true , however forall x. x + a >= x is true,
If "a" is 1, then the first is true too.
> > runST :: forall a. (forall s. ST s a) -> a
> >
> > It means that ST is a function that can be instantiated for any "a",
>
> you mean also for a = STRef s a
For some s (bound outside) - yes.
> > takes a value of type "ST s a" which can be instantiated for any "s",
>
> so also for s =s
But the s bound by this forall is different than any s that occurs in a.
> > and returns a value of type "a".
>
> and ... which delivers ST s STRef s a
You meant ST s (STRef s a). No, you confused two different s's.
One is bound by this forall and the other is bound somewhere outside.
It cannot be the same s because forall introduces a fresh type
variable, visible only inside forall.
To write down the type "forall s. ST s a" (which is exactly the same
type as "forall s1. ST s1 a", because names of local variables don't
matter, as they are not visible outside anyway) instantiated for
a = STRef s a, you must write "forall s1. ST s1 (STRef s a)".
Note that I used two a's too. This can at most cause confusion for
a human, but is not a problem for a computer language. When I write
"instantiated for a = STRef s a", the two a's are different: the first
belongs to the type signature "ST s a", the second to "STRef s a".
I could write a1 and a2 to prevent confusion.
"forall s. ST s (STRef s a)" is not an instance of "forall s. ST s a"
for any a.
Similarly to write down the result of inlining the function st inside f in
st a = \s -> a+s
f s = st (2*s)
you must write "f s = \s1 -> 2*s+s1", not "f s = \s -> 2*s+s". And it
is not a problem for a language if you pass the expression "2*a"
as an argument to a function whose parameter is called "a".
The compiler is not a C macro processor. It manages semantic entities,
not only source strings.
> > 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.
>
> Let us polish it a bit more then (I couldn't find anymore a confirmation in
> the GHC/HUGS extension libraries
> that IO a = ST RealWorld a )
>
> runST:: forall a. forall Free( s ) ni FreeV ( a ) . ( ST s a -> a)
I said above why this is wrong.
--
__("< 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-
