> May 03, 2000 12:53 AM Marcin 'Qrczak' Kowalczyk wrote:
> 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)".
>
So I looked to the example below:
forall x . x + a > x is not true , however forall x. x + a >= x is true,
of course as you say below if we talk about the wel known +.
> 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.
>
As I said above , both sentences are false
> It's the same with runST.
>
> > runST :: (forall s . ST s a ) -> a
> >
> > What sort of sentence could be meant by this?
>
I have the impression thatyou haven't read anything what I said before
> 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",
you mean also for a = STRef s a
> takes a value of type "ST s a" which can be instantiated for any "s",
so also for s =s
> and returns a value of type "a".
and ... which delivers ST s STRef s a
I only followed what you sais before about any s and aboyt any 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.
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)
>
> 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.
I think I have allready answered above and in my email enough this
rewriting either is not necessary or it means
something differently.
>
> --
> __("< 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-
>
>
>
Thanks anyway for reading and commenting honestly
but the impression that the use of quantifiers is abusive in many ways is
only reinforced
Friendly
Jan Brosius