Marcin Kowalczyk wrote at Wed, May 10, 2000 7:54 PM :
> Wed, 10 May 2000 16:18:06 +0200, Jan Brosius <[EMAIL PROTECTED]>
pisze:
pisze ? you meant wrote? Please don't use Russian in your reply, I don't
know Russian.
Do You know what pisze in Dutch could mean if spoken out loosely?
>
> > 2. Next let me point out once and for all that
> > logical quantifiers are used only in logical formula's .
>
> Types can be treated as logical formulas, according to the Curry-Howard
> isomorphism.
Sorry, never heard of in logic. But perhaps you can explain.
>I see no reason to change the notation of forall in types,
> which coresponds to forall in formulas.
This is your claim . I leave it to you to prove it
E.g. explain to me what is meant by:
forall a. (a,b)
not (a,b)
(a,b) equivalent to forall c. (c,d)
(a,b) implies (c,d)
exists a.(a,b)
(a,b) is true
(a,b) is false
>
> > b. bad use :
> >
> > newSTRef:: forall s.a . a -> ST s STRef s a
>
> You meant ST s (STRef s a).
Yes
>
> > This type signature MUST be replaced by
> >
> > newSTRef:: forall a. [forall s ni Free ( a ) . a -> ST s STRef s a]
> > where Forall s ni Free(a) means " forall s not being a free variable
> > (occurring in ) of a "
>
> Wrong. You disallowed a perfectly legal usage:
NO, NO it seems legal to you and perhaps to others but in the detailed
explanation it was
shown that the version I propose gives the necessary information for the
reader that
the type of newSTRef v shall never be of the form ST s (STRef s T(s))
As I said allready in the first email the following are different functions:
id2 :: forall s, a . (s,a) -> (s,a)
id2 (x,y) = (x,y)
id2" :: forall a. [forall s ni Free(a) . (s,a) -> (s,a)]
id2" (x,y) = (x,y) (here of course the definition is not complete since the
above information cannot be treated now
by the typechecker)
But perhaps you prefer
id2" :: forall a. (forall s. (s,a) -> (s,a))
and tell everybody that forall s in id2" is an example of second rank
polymorphism.
id2 (x,x) will compile but id2" (x,x) not
Other examples:
pr2 :: forall s, a . (s,a) -> a
pr2 (x,y) = y
and
pr2" :: forall a. [forall s ni Free(a) . (s,a) -> a]
pr2" (x,y) = y (here the definition is of course not complete, because the
typechecker can not treat this information
now)
pr2 (x,x) will give x and pr2"(x,x) will do complain the typechecker
But perhaps you will prefer
pr2" :: forall a. (forall s. (s,a) -> a)
and tell everybody that the use of forall s in pr2" is an example of second
rank polymorphism.
> refRef :: ST s Int
> refRef = do
> v1 <- newSTRef 0
> v2 <- newSTRef v1 -- Here!
> v1' <- readSTRef v2
> readSTRef v1'
> and you did not disallow any illegal usage that current rules allow
> (in fact I believe there is not any). Of course you did not allow more,
> because this type is a subset of what we have now.
I did answer this question somewhere above.
>
> > c. illigitimate use :
> >
> > runST:: forall a. ( forall s. ST s a ) -> a
>
> Let's see why do you claim that, because I see nothing wrong here.
>
> > 3. The why
> >
> > b. This is because in reality the function newSTRef is meant to be
> > used only in cases where s is not a free variable of a.
>
> False: see above.
No, I disagree, you must look below for the why.
I know very well that the type newSTRef :: a -> ST s (STRef s a )
shall work , because the typechecker in some way does the job.
But the reason why is not explained to the programmer.
As I said below if forall x,y alpha(x,y) is true then alpha(x, x) is
true
for any x
>
> > c. forall s. ST s a is illigitimate since you can not form a
> > logical phrase with it
>
> You can: for all s, ST(s,a) holds.
Yes? and what does it mean? Up to now it doesn't mean more than (forall
apple . apple ) is true (false ) ?, and
wat does the last thing mean?
>
> > (It is not supposed to be known that ST s a is in reality implemented
> > as a function.).
>
> Why is this a problem?
This is not a problem , but if ST s a :: s -> (s,a) is a function you
could in principle use forall
forall s . ST s a :: s -> (s,a) then means (could then mean) : " forall s
. ST s a is a function of s into (s,a) "
Admitted such a function will be very uncommon. Is it an injection? Then
which injection. Everybody is immediately interested to see the
implementation.
Now if you look at the implementation you will see that it is not an
injection but a family f(a) indexed by a , of
constant functions of s into (s,a) .The actual implementation of f(a)
was not given in the paper.
>
> > There are 2 ways to circumvent this problem.
>
> There is no problem!
Obviously not for you.
>
> And you create additional language, which would have to be understood,
> given a precise meaning, implemented, documented etc. It is not needed.
> BTW, would it change the semantics, or only the language we talk about
> types?
It certainly does not change the way GHC is compiled . It is more a
clarification
for everybody learning these functions , the documentation needs only a FEW
lines more.
BUT it could lead to richer ways of expression than Haskell can do now,
without putting in danger I think
the static typechecking.
>
> > c1. Use a new free variable binder ,e.g. `b ,for types
> > to mean the following:
> >
> > `b s. ST s a
> >
> > is the type of ALL ST s a with the EXCEPTION
> > of all types of the form ST s T(s)
>
> What would be the definition of `b?
Sorry, I bet you can't give the definition of "forall" and of "exists" in
a pure formal way.
It is the same thing as for the notion SET and integer numbers.
Tell a child first what is a set in a math course and next year tell him
that 0 is the empty set.
The loose use of set leaded to a paradox.
I invite you to give a precise meaning of set.
>
> Here `b is exactly the same as forall. "a" could have the form T(s)
> anyway, because "s" is bound here, and "a" is bound outside.
I would say then that you did not understand the use of forall in
forall s . ( ST s a )
That is not a tragedy (I don't understand it too ). What is a tragedy is
that you don't even know
the formal behaviour of forall s . ( ST s a) i.e. you don't seem to see
the difference between
forall s . (ST s T(s))
and
(T(s) | a ) [ forall s. ( ST s a ) ] == forall s1 . ( ST s1 T(s) )
Now forall s1. ( ST s1 T(s)) IMPLIES forall s . ( ST s T(s) )
>That's
> why I am asking for a definition: the example did not explain it.
So you do understand a bit , the meaning of `b
With (`b s. s a ) or better (`b s) ( s a ) s becomes a bound variable, and
a is in the scope ( by using the
parentheses around s a ) of `b . For the rest I could formally write it
down as follows
(`b s ) ( s a ) == `b ( `sq a ) where `sq means a small square tied with a
line to `b .
How would (`b s) ( s T(s) ) look like : for this let us use for convenience
T(s) == s ,
( `b s ) ( s T(s) ) == `b ( `sq `sq) where the 2 squares are
tied to the SAME `b
How would the substitution of a by s into (`b s) ( s a) look like
that is ( s | a ) [ (`b s) (s a) ] == `b ( `sq s ) ==/ `b ( `sq `sq )
A SUGARED version of the 2 above would give
1. `b s ( s s )
2. `b s1 ( s1 s)
This is exactly how TECHNICALLY Forall s . ( ST s a ) would work
>
> > c2. Use the following type signature for runST
> >
> > runST:: forall a. [forall s ni Free( a ) . ST s a -> a]
>
> This is wrong, because allows running IO, as you fix below:
>
> > If we are supposed to know that IO a = ST World a
> > then use the signature
> >
> > runST:: forall a. [forall Variable ( s ) ni Free ( a ) . ST s a -> a ]
> >
> > where Variable (s) means " s is a type variable".
>
> What does it mean "s is a type variable"?
this means that all things of the form Variable ( Sblurb ) are false ,
that is Variable ( World ) is false since World is not a variable.
>
> Consider:
>
> runST':: forall s. ST s Int -> Int
> runST' x = runST x
>
> Should it compile with your type of runST?
I shall not answer your question , since the changes I propose don't
introduce a NEW type system
they are only a BETTER explanation of these forall's. They don't change the
way how GHC would compile.
They only give this little extra information for the reader that is needed.
E.g. do you agree that s and a represent general type variables?
That is why in principle one must write
forall a. forall State s . ( .. ) or equivalently forall State s . forall
a. ( .. )
>
> If yes, I cannot see why do you say that here runST is instantiated
> with a type that is not a type variable. What does it mean "s is
> a type variable"?
It means "World is a type variable " is false (substitution of s by World
here.)
It also means " sWorld is a type variable " is true. (substitution of s by
sWorld here)
>
> If no, it can be used to run an IO computation by evaluation of
> a pure expression, so it is a wrong type for runST.
>
> > 4. If it were possible to interrogate the typechecker in
> > the following way :
> >
> > typeOf (x) = typeOf (y)
> >
> > then it would be possible to give a direct definition of runST.
>
> I don't understand what you mean here.
Here I agree , a better proposal would be
typOf ( x ) == ST s T(s)
but this means that to the typechecker should be explained what the general
PATTERN ST s T(s)
stands for.
Perhaps this would make it clearer (sorry for the non Haskell syntax)
runST :: ST s a -> a
runST x = typOf ( x ) == ST s T(s) -> error
= match x with
ST u v -> v
>
> > 5. Using `b as defined above
>
> You did not define `b :-)
Well , look somewhere above. The formal definition is given there.
>
> > ------=_NextPart_000_00BC_01BFBA9B.533DF5D0
> > Content-Type: text/html;
> > charset="iso-8859-1"
> > Content-Transfer-Encoding: quoted-printable
>
> Please don't post in HTML.
>
> Sorry that I did not answer your last e-mail. I will not answer it,
> because I would not say much more than here. I would say: please
> explain precise meaning of your symbols.
>
> --
> __("< 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-
>
>
>
