Thu, 11 May 2000 13:48:56 +0200, Jan Brosius <[EMAIL PROTECTED]> pisze:
> > Types can be treated as logical formulas, according to the Curry-Howard
> > isomorphism.
>
> Sorry, never heard of in logic. But perhaps you can explain.
Others explained it better that I could.
> > > 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))
Wrong: it can have this form.
I have posted a legal and correct program which uses newSTRef with
such type.
If you claim that it should not be used with that type, please show
a program which is legal without the restriction of type of newSTRef
and whose semantics are incorrect (e.g. allows a value to depend on
the order of reduction, or allows using IO in pure expressions).
> 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.
There is nothing to explain. newSTRef can be used for any choice of
"s" and "a", exactly as the type says.
> > 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 needs not to be formal. And assume that we both know what forall
means, and how types are constructed, and what type variables mean
(even if the assumption is wrong)
Your example gave the same meaning to `b and forall. I don't see
any gain in changing the symbol from forall to `b, without changing
anything else.
> 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) )
I do see it.
> Now forall s1. ( ST s1 T(s)) IMPLIES forall s . ( ST s T(s) )
It does not. And I have already told why, a few e-mails ago.
I can explain it again.
For the first term to have any meaning, "s" must have a meaning,
because it is a free variable. So for a counter-example assume that
we sit in real numbers and
ST a b means a^2 > b
T(a) means a+1
s means -2
The first term means forall s1. s1^2 > -1, which is true.
The second term means forall s. s^2 > s+1, which is false.
So the first does not imply the second.
> So you do understand a bit , the meaning of `b
Your examples imply that `b means the same as forall. But it does
not explain why you advocate replacing forall with `b if it means
the same thing.
> > > 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.
When you use runST, you don't always know if the type given for "s"
will be instantiated to a type variable or not. Being a type variable
is not a property of a type.
> > 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 explain it if you cannot answer a simple question.
> E.g. do you agree that s and a represent general type variables?
It depends on what does it mean "general" and how they are used.
> > 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)
>From this I assume that the above example should compile, because
you instantiate "s" from the type of runST with "s" from the local
environment of runST', and you don't know anything more about this "s"
here. If so, your type of runST is wrong, because it allows performing
I/O in a pure expression (because nothing prevents me from using runST'
instantiated with RealWorld).
--
__("< 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-
