>From: Marcin 'Qrczak' Kowalczyk <[EMAIL PROTECTED]>
>To: <[EMAIL PROTECTED]>
>Sent: Tuesday, May 16, 2000 11:42 AM
>Subject: Re: more detailed explanation about forall in Haskell
> Tue, 16 May 2000 10:54:59 +0200, Jan Brosius <[EMAIL PROTECTED]>
pisze:
>
> > > > newSTRef v has type ST s (STRef s (STRef s a))
> > > > (THIS is of the form ST s (STRef s T(s))
> > >
> > > No. It has the type
> > > ST s1 (STRef s1 (STRef s a))
> >
> > That is indeed what I said in my former email where I stated that
> > newSTRef does NOT deliver something with type St s (STRef s T(s))v
> > and where you said the CONYRARY.
>
> newSTRef applied to some value can have a type ST s (STRef s T(s)),
That is strange , can you give a little example?
> thus the type of newSTRef must be as in Haskell, not as you say.
I agree if you can give me an example. But if you are right then newSTRef
should be more documented,
and then I guess I would still be able to give the correct logical
description of newSTRef.
However everything depends on the answers of the questions posed below.
(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 have no problem with the diference between a variable in a function
definition and in a type signature.
But making a distinction among type variables looks very WEIRD to me.
Sincerely I can't think of any practical (implementation) reason to do this
.
Before saying more I await your answer.
>
> But it does not have such type in your example.
>
> > > When runST' will be applied to a value of the type "ST RealWorld Int",
> > > "x" will have the type "ST RealWorld Int".
> >
> > I thought that runST does not work on types of the form ST Blurb Int
>
> runST was already compiled into the body of runST'. It does not have
> a chance of accepting or rejecting types. What matters when we use
> runST' is the type of runST', nothing more. It allows aplying runST'
> to any type "s", including RealWorld.
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.
I repeat here your runST'
runST' :: ST s Int -> Int
runST' x = runST x
written down like that I thought runST' would work fine as long as runST
works fine.
Since runST does not work on something with type ST World Int , I would
have expected
that since x has now the wrong type thart runST x woulg give an error at
least at runtime.
It looks very strange to me that such a thing can happen. VERY strange.
Since I have not tried
it myself . This is indeed contrary to math: where , if given a function f
: a -> b and if one defines
a function g :: c -> b where c contains a then if one defines
g by : g(x) = f(x) then this automatically guarantees that g and f are
IDENTICAL functions.
Do I have to conclude that Haskell departs from this common sense?
QUESTION : Is this true ?????
>
> > what's the difference between a -free-type variable and a type
> > variable (if not bound by a quantifier)?
>
> 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 .
Next I would read a -> a as: this argument is a (general) endomorphism .
Third If I would give any meaning to forall a. a-> a then I would give it
the
same meaning as a -> a . If Haskell doesn't do so I can only regret this
and 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]
??? What is the practical reason for such a distinction?
Very Friendly
Jan Brosius
> f does not have the type forall a. a->a.
>
> The type variable "a" in the type of "f" here is bound by implicit
> lambda in the definition of f1. It is some concrete type each time
> "f1" is used. The type variable "a" in the type "a->a" of the function
> "\x -> x" is free, so can be generalized over and the function "\x -> x"
> can be instantiated for any choice of "a".
>
> --
> __("< 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-
>
>
>
