> 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


Reply via email to