>----- Original Message -----
>From: Marcin 'Qrczak' Kowalczyk <[EMAIL PROTECTED]>
>Sent: Tuesday, May 16, 2000 11:40 PM
>Subject: Re: more detailed explanation about forall in Haskell
> Tue, 16 May 2000 22:37:45 +0200, Jan Brosius <[EMAIL PROTECTED]>
pisze:
>
> > > newSTRef applied to some value can have a type ST s (STRef s T(s)),
> >
> > That is strange , can you give a little example?
>
> I've given it four mail pairs ago, but here it is again:
>
> refRef :: ST s Int
> refRef = do
> v1 <- newSTRef 0
I have not the do notation definition in front of me, so I guess (I am
lazy):
type of v1 is ST s (STRef s Int) ? (or STRef s Int ?)
> v2 <- newSTRef v1 -- Here!
Ok, type of v2 is ST s1 [STRef s1 (ST s (STRef s Int)] ? (or STRef s1
[STRef s Int] ?)
which is of the form ST s1 (STRef s1 T(s)) with the additional condition
given to
the type checker that s1 =/ s and will always be considered as different
i.e. s1 =/ s
This shows that the additional comments given by me for the signature of
newSTRef are not redundant.
> v1' <- readSTRef v2
> readSTRef v1'
>
> > (e.g. if there are 2 sorts of type variables in Haskell 2 (or in
> > Haskell 98 ) then I would really like to know what is the practical
> > reason of this.
>
> I see nothing that could be described as 2 sorts of type variables.
Sorry, what were you then talking about in the former email??
>
> > I don't know if it compiles. If it compiles I can only say that
> > this seems strange to me.
> > I certainly should not expect that that is possible.
>
> Of course it does not compile in Haskell. This was to show that your
Why then did you say it compiled?
> checking "whether something is a type variable" is meaningless: here
> a type is a type variable as far as I can tell, but runST requires
> some different condition.
NO.
As I said allready before the socalled "my" runST is nothing else but a
better documented runST.
The Terms Variable(s) and Free(a) are not implemented (yet)
This is for the implementor to do ,if he wants. If these "terms" could be
implemented that could allow
a richer set of functions then one can have today.
>
> > > f1:: (a -> a) -> [Int] -> [Int]
> > > f1 f l = map f l
> > >
> > > This definition does not compile, although f has type a->a.
> >
> > First I didn't know that the use of forall was obligatory in Haskell 98
.
>
> It is not - and that's why in Haskell 98 you cannot write the
> type signature of "f" inside the definition of "f1". If you write
> "f:: a -> a", it means "f :: forall a. a -> a", but "f" has a
> different type.
>
> In GHC you can write the type of "f", provided that you have given a
> name to the type variable in question, using a pattern type signature
> or result type signature (the latter not working yet).
>
> > Third If I would give any meaning to forall a. a-> a then I
> > would give it the same meaning as a -> a .
>
> Wrong. The first is the type of a function that is polymorphic:
> works for any argument type and gives a result of the same type
> (there exist only three function of that type in Haskell 98:
> bottom, function that always returns bottom, and identity).
>
> The second is the type of a function from "a" to "a". Depending on what
> "a" is, it can mean different things. For example if "a" is bound at
> some outer function definition, it is the function from the whatever
> type the outer function has been instantiated to, to the same type.
>
> > I would like to know why for heaven's sake a distinction has to be
> > made between
> >
> > f1:: ( a -> a) -> [Int] -> [Int]
> > and
> > f1':: ( forall a . a -> a) -> [Int] -> [Int]
>
> How can you propose a better type of runST if you don't understand
> such basic things?!
I don't understand illogical things. You on the contrary made mistake after
mistake with your so called counterexample.
Moreover you said your runST' did compile and now you say your runST' does
not compile.
Next time please don't lie. Try to be as clear as possible.
Because I don't use forall in a bad and meaningless manner. You do ,perhaps
Haskell 2 does, when it is not
necessary.
a -> a should mean an endomorphism e.g. id etc.or something like
f :: Int -> Int
f x = x^2 + x + 1
is an instance of an endomorphism a -> a
forall a. a -> a should mean the same thing but clearly it does not in
Haskell 2 .
Please people, do not accept this in Haskell 2 ? I am almost sure there is
no need for it.
>
> To use f1, you choose a type for "a", pass a function of the type
> "a -> a" and get a function [Int] -> [Int]. For example you can
> pass not (of type Bool->Bool) to f1.
Yes, and in id . f (where f is as above f x = x^2 + x + 1 and where id
x = x ) you cannot pass type Bool -> Bool
to id .
Very Friendly
Jan Brosius
Very primitive explanation to defend the writings a -> a and forall a.
a -> a as different .
If Haskell 2 interprets a -> a as ea GENERAL endomorphism ther is no problem
at all.
>
> To use f1', you must pass a polymorphic function of the type
> "forall a. a -> a" to it, and get a function [Int] -> [Int].
> You have only three choices for the first function.
>
> To implement f1, you must be prepared for any type for "a" a caller has
> chosen. It is hard to use the first argument in an interesting way,
> because you have no values of type "a" other than bottom, and there
> is little to do with a value of type "a" you get from the function,
> because you don't know what "a" will be.
>
> To implement f1', you know that the function is polymorphic, and you
> can use it on any type you wish. For example apply it to each element
> of the list and then to the list itself.
>
> --
> __("< 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-
>
>
>
