Dear Marcin,
I think we have reached now a point in the discussion that will only result
in yes and no.
1. Even as I still think that the forall in runST is misplaced I still stand
open for everyone that could
put forall s. (ST s a) in an acceptable logical phrase. forall and exist
work like that PERIOD. And if you want an excellent mathematical society
from which I borrowed this formal logic (still the best I ever saw) then I
only have to name the French mathematical society NICOLAS BOURBAKI. I guess
none of the readers on the Haskell -list has ever read their "Theory of
sets". The foundation upon which they wanted to build the whole of math..
Their books are the best books on mathematics that I have ever seen ; the
formulation is always precise . Ok enough "laudatio" (latin).
The sad thing is : they never reached their goal.
2. I still try to be open for any new insights (I am myself involved in a
conservative extension of their logic :
a work that I shall restart as soon as possible) but then you will have to
do a minimum of effort to make some things clear and not answer most of the
time in semi-programmese - mathese .
3. Promise me to reply from which doubly quantified formula your formula
comes from.
> 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.
NO, they did not explain : at the very best they gave a site to look at .
Which I shall do if my phone bill allows it.
I did expect these explanations from you, otherwise withdraw your claim. So
in the next reply surprise me with these explanations (copy and paste ).
>
> > > > 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.
OK this is something to start from. I rehearse the definitions and the
little program I found in the paper.
newSTRef :: a -> ST s (STRef s a)
readSTRef :: STRef s a -> ST s a
and
f :: STRef s a -> STRef s a
f v = runST( newSTRef v >= \w -> readSTRef w)
Let's start
v has type STRef s a
newSTRef v has type ST s (STRef s (STRef s a)) (THIS is of the form ST
s (STRef s T(s))
w has type STRef s (STRef s a)
readSTRef w has type ST s (STRef s a)
runST gets as argument ST s (STRef s a) and the typechecker or whatever
thing complains.
AM I right or not.?
Since I know that this program works (found in the paper) you are going to
use the following trick:
newSTRef :: forall s,a . a -> ST s (STRef s a)
Ok, a "needs" to be instantiated , I prefer substituted
(STRef s a | a) forall s. [ a -> ST s (STRef s a)]
== forall s1 . [ STRef s a -> ST s1 (STRef s1 (STRef s a))
Ok in logic one has the following rule for forall :
forall s1 . [STRef s a -> ST s1 (STRef s1 (STRef s a)) => forall s.
[STRef s a -> ST s (STRef s (STRef s a))]
Now where in the Haskell documentation is written down NOT to use
forall s. [ STRef s a -> ST s (STRef s (STRef s a))]
and thus not to use
STRef s (STRef s a) as type for w.
So, at this point I guess a little daemon informs the typechecker that the
type for w is in reality
STRef s1 (STRef s a) and this little daemon performed a check to see if s1
does not occur in STRef s a
and further informs the typechecker that s1 from now on is never to be
allowed to become s.
Next readSTRef w gets type ST s1 (STRef s a)
and the argument of runST can now work and will deliver something with type
STRef s a
look closely at
newSTRef :: a -> ST s (STRef s a) and at
runST :: forall s .(ST s a) -> a
as seen above : newSTRef is NOT allowed to DELIVER something of the type ST
s (STRef s T(s))
also runST is NOT allowed to ACCEPT anything with type ST s T(s)
Do you see the similarity
>
> I have posted a legal and correct program which uses newSTRef with
> such type.
Well , if that's true there is a problem ( I think)
>
> 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 thought this program is above , see f v
(believe it or not I still have not typed some little code in Hugs in my
Windows NT OS ; I guess I am lazy)
>
> > 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.
In that case see above : f v , I thought would work ( found in paper)
>
> > > 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
I hope I do.
> means, and how types are constructed, and what type variables mean
> (even if the assumption is wrong)
You mean I don't know the definition of forall?
Thanks anyway.
>
> Your example gave the same meaning to `b and forall.
NOT true : forall works on a proposition and delivers another proposition .
And this should REMAIN so.
`b on the contrary works on a type and delivers a new type.
Quite different things , I would say.
>I don't see
> any gain in changing the symbol from forall to `b, without changing
> anything else.
Only a few lines added to the documentation . Nothing for the typechecker
nor for GHC changes. But the language
changes a micro-little. Is it worth that change : I say YES.
>
> > 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.
IT DOES : that is a well known rule of forall (forall x,y . alpha(x.y) =>
forall x. alpha(x,x) )
I cannot change this rule for you nor for the president of the U.S.A .
Should I feel sorry?
> I can explain it again.
Fine , I know the outcome.
>
> 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.
(You shall see below that I did my best to get the original formula back)
Either I do not understand you now about which formula you are talking ,
either you have committed GROSS errors.
Let's see:
forall a,b . a^2 > b is false since 1^2 /> 3 . anyway this remains TRUE
:
forall a,b . a^2 > b IMPLIES forall a . a^2 > a
and forall Real(a) . a^2 > a is not true for a = 0 but amazingly forall a >
1 . a^2 > a is true
this should however not surprise us (EX FALSO QUODLIBET (latin) : a false
assertion implies anything ).
Let us polish this a bit
forall a, b > 1 . a^2 > b implies forall a > 1 . a^2 > a
forall a,b > 1. a^2 > b is FALSE but amazingly forall a > 1. a^2 > a is
TRUE .
However you can not DERIVE that forall a > 1 . a^2 > a is TRUE using the
next rule
P => Q (true)
P (true)
*********
Q (true)
I forgot the latin name for this ancient rule.
> The second term means forall s. s^2 > s+1, which is false.
>From which formula do you come , let's try ... you come from a formula with
2 forall's but which one ???
Well I am not clairvoyant : you will tell me in your reply isn't it?
> So the first does not imply the second.
Dear Marcin , for once and for all : forall x,y . alpha(x,y) IMPLIES
forall x . alpha( x ,x)
>
> > 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.
It does not mean the same thing , I rehearse:`b applied to a parameterized
type delivers a new type
forall applied to a formula yields a new formula.
Technically : forall x . x /= y == `t ( `sq /= y) (<-- formula)
and similarly `b s. ST s a == `b (ST `sq a ) (<--- type)
More forall obeys certain rules making many victims ; `b s. (ST s a) means
the DOMAIN of runST is not
all ST s a for any s and a , NO the DOMAIN of runST is ST s a without
anything of the form ST s T(s) :
in some sense `b restricts the too great domain ST s a to a domain obtained
from ST s a by substracting any
"diagonal element" ST s T(s)
>
> > > > 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.
I can only say here : ???????????????
>
> > > runST':: forall s. ST s Int -> Int
> > > runST' x = runST x
> > >
> > > Should it compile with your type of runST?
Ok you want an answer.
MY type is : forall a . [ forall Variable(s) ni Free(a). ST s a -> a]
next
(Int | a) [ forall Variable(s) ni Free (a) . ST s a -> a] ==
forall Variable(s) ni Free(Int) . (ST s Int -> Int)
Variable(s) is true , and s ni Free(Int) is true also since Int does not
contain s , so the conditions for the
function runST are fullfilled . So ("my") runST will work.
> >
> > 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.
I didn't say that I couldn't , I did say that I didn't like to do it .
>
> > 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.
by general a, I mean a type variable that can be substituted by any other
type(variable)
So, in this sense s is not general since one declares State s , i.e. s is
a type variable of type State .
(I hope )
>
> > > 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).
I cannot follow here, didn't you define runST' x = runST x ?
If runST x works then this means (see my definition of runST ) that the
type of x is allowable by runST.
Now if type of x is ST World Int then my runST and the official runST will
not work, say runST x = error and
so runST' x = error
I don't see the rest of your partially defined runST' ?
>
> --
> __("< 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-
>
>
>
very friendly
Jan Brosius
PS: for the non existing Haskell committee : is it now clear that there is
much confusion?
