Wed, 10 May 2000 16:18:06 +0200, Jan Brosius <[EMAIL PROTECTED]> pisze:
> 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. I see no reason to change the notation of forall in types,
which coresponds to forall in formulas.
> b. bad use :
>
> newSTRef:: forall s.a . a -> ST s STRef s a
You meant ST s (STRef s a).
> 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:
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.
> 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.
> 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.
> (It is not supposed to be known that ST s a is in reality implemented
> as a function.).
Why is this a problem?
> There are 2 ways to circumvent this problem.
There is no problem!
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?
> 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?
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. That's
why I am asking for a definition: the example did not explain it.
> 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"?
Consider:
runST':: forall s. ST s Int -> Int
runST' x = runST x
Should it compile with your type of runST?
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"?
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.
> 5. Using `b as defined above
You did not define `b :-)
> ------=_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-
