----- Original Message -----
From: Jan Brosius <[EMAIL PROTECTED]>
To: Marcin 'Qrczak' Kowalczyk <[EMAIL PROTECTED]>
Cc: <[EMAIL PROTECTED]>
Sent: Wednesday, May 03, 2000 1:04 PM
Subject: Re: About the abuse of forall in Haskell
>
> > 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 not . Let me correct myself
forall Positive ( x ) . x + a >= a is true.
Friendly
Jan Brosius
> 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
>
