Re: more detailed explanation about forall in Haskell
Jan Brosius wrote: "x" in the domain of your model, and that that element, at least, satisfies x is a variable ; no domain ; no model You must have some assumed convention that makes x a variable. For the rest of us it might as well be a constant, because there is no way to tell if it is a variable or not. -- -- Lennart
Re: more detailed explanation about forall in Haskell
Jan Brosius writes: I must put this in the good way; [forall x . alpha(x)] = alpha(x) is True Yes, by instantiation. I disagree. You disagree with my agreeing with you? If alpha(x) is TRUE then the following is true : alpha(x) = [forall x. alpha(x)] No, alpha(x) only asserts that some element named x satisfies alpha. It does not follow that therefore every other element also satisfies alpha. No the variable x means that it can be substituted by any term. That is the real meaning of a variable (at least in classical logic). Only when the variable is bound by a forall. It is exactly the same situation as with lambda-calculus and lambda. The term "x" denotes a fixed element of its type. When I bind it, as in "\x - x", I'm saying that that x may range over any element in the type. Once I've said that, yes, I can substitute any element for x in the body. (\x - P(x)) t = P(x) [t/x] Consider e.g. Carl Witty's formula : prime(x) == x is a prime number. Then prime(2) == (2|x) prime(x) is true , and prime (4) is false Take something else alpha(x) == prime(x) AND ¬ prime(x) ( ¬ signifies not) then alpha(x) is a false formula and you have ¬ [exists x. alpha(x)] On the contrary beta(x) == ¬ alpha(x) is true for any x Yes, because x is bound in the body of beta. beta := \x - not(alpha(x)) BTW, I don't understand your "(2|x)" notation. Is this a substitution? So if alpha(x) is TRUE then [forall x. alpha(x) ]= alpha(x) This does not follow. It is truth-equivalent to: Sorry, I disagree Well, you certainly have the right to disagree. But you are disagreeing with every logician since Gentzen. [forall x. alpha(x)] = True ( In the above you should at the very least not forget to mention that [forall x. alpha(x)] must be true ) Isn't that what I wrote? In principle True is a sloppy expression for saying that [forall x . alpha(x)] is a theorem of some mathematical theory. I have used True because discussing mathematical theories would have lead the discussion out of the scope of the discussion. For instance let "T=" denote a mathematical theory with equality then one has "T=" -| x = x that is the formula x = x is a theorem in "T=" . More sloppy the formula x=xis TRUE in "T=" This has no bearing on the discussion. which is equivalent to: forall x. alpha(x) which is only true when every element satisifies alpha; so it is not a tautology. I repeat: you do not understand the difference between bound and free variables. I disagree a free variable is not a constant. I didn't say it _was_ a constant. I said it behaved like a constant, but that they are syntactically distinct because you cannot bind a constant. A bound variable is a variable tied to a quantifier. In principle a bound variable is not visibly. This is best illustrated by Bourbaki's approach where they first define : exists x . alpha(x) == (`t x (alpha)| x) alpha where if e.g. alpha(x) == x = x then `t x (alpha) == `t ( `sq = `sq ) where `sq denotes a small square and where here both `sq are tied to `t by a line In this way I can really say that in [existx x. x = x] the variable x has disappeared. Finally Bourbaki defines forall x . alpha(x) == ¬ [exists x . ¬ alpha(x)] Sorry, I don't understand your notation, or what relevance this has. I repeat : there are no domains in propositional calculus , but I am aware that in some text books about propositional calculus one speaks about it , I regard this as cheating : introducing a concept that one is going to define later. I remember my prof, in logic in 1 cand. math - physics where his first lesson began by writing on the blackboard : p V ¬ p and he only said " p or not p " " tertium non datur" " a third possibility is not given " His whole course was as formally as possible, and variables were not supposed to range about a domain. I don't understand what relevance this has. A free variable behaves like a constant. No a constant is always the same constant, it is never substituted by something else, it is "immutable". A variable is a placeholder for a Term ( a constant is a special term) I see where you are heading. In the reduction laws, you substitute for free variables. This is true, but you can only substitute for a free variable if it was bound in an outer scope, and you are stripping off the binding, as in the beta-equality for lambda-calculus, which I will repeat: (\x - P(x)) t = P(x) [t/x] You cannot simply substitute any value you please for an arbitrary free variable and expect the new term to be equal to the old one. For example in Haskell, fst :: (a,b) - a is a free variable in every term (where it's not shadowed). Now if I have the term fst p and I substitute snd for fst: (fst p) [snd/fst] = snd p but
Re: more detailed explanation about forall in Haskell
Frank Atanassow [EMAIL PROTECTED] writes: I agree, and I think it's hopeless. This is my last message to the Haskell list on the subject. There is nothing Haskell-specific any longer about this discussion. Uh, I feel I'm a bit of a hobbyist on this list, but what exactly is the relevance of all this? Flipping through these messages, I feel I have aquired some grasp of forall, but in what contexts is forall used in Haskell - can anybody point me to an URL that explains or exemplifies? -kzm -- If I haven't seen further, it is by standing in the footprints of giants
Re: more detailed explanation about forall in Haskell
There is a good introduction by Cardelli and Wegner:
Luca Cardelli and Peter Wegner. On understanding types, data abstraction,
and polymorphism. Computing Surveys, 17(4):471-522, 1985.
available from Cardelli's page at
http://research.microsoft.com/Users/luca/Papers/OnUnderstanding.A4.ps
http://research.microsoft.com/Users/luca/Papers/OnUnderstanding.{US,A4}.{ps.pdf}
--
Frank Atanassow, Dept. of Computer Science, Utrecht University
Padualaan 14, PO Box 80.089, 3508 TB Utrecht, Netherlands
Tel +31 (030) 253-1012, Fax +31 (030) 251-3791
Re: more detailed explanation about forall in Haskell
On 19 May 2000, Ketil Malde wrote: Frank Atanassow [EMAIL PROTECTED] writes: I agree, and I think it's hopeless. This is my last message to the Haskell list on the subject. There is nothing Haskell-specific any longer about this discussion. Uh, I feel I'm a bit of a hobbyist on this list, but what exactly is the relevance of all this? Flipping through these messages, I feel I have aquired some grasp of forall, but in what contexts is forall used in Haskell - can anybody point me to an URL that explains or exemplifies? How about: http://haskell.org/onlinereport/decls.html http://www.haskell.org/ghc/docs/latest/users_guide/universal-quantification.html http://www.cse.ogi.edu/PacSoft/projects/Hugs/pages/hugsman/exts.html http://www.cs.chalmers.se/~augustss/hbc/decls.html /Lars L
Re: more detailed explanation about forall in Haskell
|From: Lennart Augustsson [EMAIL PROTECTED] |To: Jan Brosius [EMAIL PROTECTED] |Cc: Frank Atanassow [EMAIL PROTECTED]; [EMAIL PROTECTED] |Sent: Friday, May 19, 2000 12:07 PM |Subject: Re: more detailed explanation about forall in Haskell Jan Brosius wrote: "x" in the domain of your model, and that that element, at least, satisfies x is a variable ; no domain ; no model You must have some assumed convention that makes x a variable. That's true . To be complete in Bourbaki's formal logic they don't speak in the beginning about a variable but they define a substitution mechanism for ONLY small latin letters ,denoted ( T | u) S which means replace in S , being just consecutive string of symbols, every occurence of the letter u by T , which itself is also a consecutive string of symbols , I think this corresponds to (T | u) S == (lambda u . S) T (as far as I know lambda- calculus) Of course they begin with a set of allowable symbols. Later when they talk about a mathematical theory they introduce the "metha-mathematical " notion of variable in the following sense a letter t is a variable of the theory if this letter does not occur explicitly in one of the axioms of the theory. Another way to introduce a variable would be to use a special letter say x and to say, that a variable is an x subscripted by an integer number , this would mean that only x0 , x1 , x2 , ... ,x10 , etc. .. are variables. But this is not the place to explain in full detail Bourbaki's approach of formal logic . I thought there is a common consensus in logic about a variable. Allow me to come back to to some meaning of variable expressed by someone else in a previous email. A person said something like this " alpha(x) means that alpha(x) is true for some x " (where alpha(x) denotes a formula containing a variable x .) Now if one looks carefully this above sentence means formally [exists x. alpha(x) is true] which is a FALSE assertion. To be honest he didn't wrote the above english phrase not like this , but he represented it by the implication alpha(x) = [exists x . alpha(x)] which is a totally other thing . This implication should more be read as " if alpha(x) is true for some x then there exists an x such that alpha(x) is true" Now as everybody can see the above phrase looks a bit strange . It would have been better to replace it by (T | x) alpha(x) = [exists x . alpha(x)] where T is a TERM not containing the letter x which can be read " if alpha(x) is true for some x = T then there exists an x such that alpha(x) is true " which is perhaps an english phrase that makes more sense (I don't know) . Bourbaki uses this implication ( (T | x) alpha(x) = [exists x . alpha(x)] where T is a TERM not containing the letter x ) as an axiom scheme for his theory with quantifiers . Bourbaki makes a distinction about axioms and speaks about explicit axioms and axiom schemes. But the above remarks would have lead the discussion off the road and also not everybody knows about Bourbaki. When I referred to variables and to the forall quantifier I implicitly thought that there was a common consensus about the use of variables and the forall quantifier. Now it doesn't bite me if someone regards variables as ranging over a domain . But I had to reply since one was insinuating that I don't understand the difference between free and bound variables , that is saying as much as : you don't understand logic. As Mark Jones has allready said this thread should end or come to a conclusion. Unfortunately he said more than that . He said that the discussion was all about the difference a - a and forall a. a - a . And that's not true . One only has to read the first 2 or 4 emails about this thread of discussion. On the other hand someone's remark and about the meaning Haskell gives to these two types and I wonder since today if one means by a - a a type indication to be understood as a function having this type signature means that the function is only defined for some a 's and by forall a. a - a a type indication to be understood as a function that is really defined for ALL type's a . The above is just a question . If my interpretation is right then one can change a - a by [exists a. a - a] But again my first email didn't talk about that , as every reader willing to look in the archives would acknowledge. Friendly Jan Brosius PS : by saying weird I didn't mean illigitimate I meant more something like "it surprises me" where I am talking as a mathematician trying to use Haskell , not knowing the type system that is used nor the theory behind it , only being surprised that in some cases forall cannot be understood anymore as forall in formal logic. E.g. it is a true fact that Bourbaki doesn't use forall before a type , and I thought it is common consensus in formal logic used in math th
RE: more detailed explanation about forall in Haskell
Frank Atanassow wrote: However, I think maybe it has demonstrated that the implicit forall'ing in Haskell can be confusing in practice. In particular, it makes it hard to talk unambiguously about types of non-top-level definitions/terms. I'm sure this pot has been stirred up enough already, but as a newbie to Haskell I also found the "forall" rules counter-intuitive with regard to exitential types. (i.e. the use of forall a. when exists a. might have been clearer.) I hope that at some point this area of Haskell will be revised. --Peter Douglass
Re: more detailed explanation about forall in Haskell
I also think it is hopeless , but I still want to try again *- Original Message - *From: Frank Atanassow [EMAIL PROTECTED] *To: Jan Brosius [EMAIL PROTECTED] *Cc: Frank Atanassow [EMAIL PROTECTED]; [EMAIL PROTECTED] *Sent: Friday, May 19, 2000 12:59 PM *Subject: Re: more detailed explanation about forall in Haskell *Jan Brosius writes: * I must put this in the good way; * * [forall x . alpha(x)] = alpha(x) is True * * Yes, by instantiation. * * I disagree. *You disagree with my agreeing with you? About what do you agree with me? * If alpha(x) is TRUE then the following is true : alpha(x) = [forall x. * alpha(x)] * * No, alpha(x) only asserts that some element named x satisfies alpha. It * does * not follow that therefore every other element also satisfies alpha. * * No the variable x means that it can be substituted by any term. That is the * real meaning of a variable * (at least in classical logic). *Only when the variable is bound by a forall. It is exactly the same situation *as with lambda-calculus and lambda. The term "x" denotes a fixed element of *its type. When I bind it, as in "\x - x", I'm saying that that x may range *over any element in the type. Once I've said that, yes, I can substitute any *element for x in the body. * (\x - P(x)) t = P(x) [t/x] * Consider e.g. Carl Witty's formula : prime(x) == x is a prime number. * Then prime(2) == (2|x) prime(x) is true , and prime (4) is false * * Take something else alpha(x) == prime(x) AND ¬ prime(x) ( ¬ signifies * not) * * then alpha(x) is a false formula and you have ¬ [exists x. alpha(x)] * * On the contrary beta(x) == ¬ alpha(x) is true for any x *Yes, because x is bound in the body of beta. I have seen what you mean by bound. Clearly you are talking about something else than quantified logic * beta := \x - not(alpha(x)) You are talking about lambda calculus where I am talking about quantified logic *BTW, I don't understand your "(2|x)" notation. Is this a substitution? Yes * So if alpha(x) is TRUE then [forall x. alpha(x) ]= alpha(x) * * This does not follow. It is truth-equivalent to: * * Sorry, I disagree *Well, you certainly have the right to disagree. But you are disagreeing with *every logician since Gentzen. I disagree with you Frank , the rest is your imagination. * [forall x. alpha(x)] = True * * ( In the above you should at the very least not forget to mention that * [forall x. alpha(x)] must be true ) *Isn't that what I wrote? Of course not , what you wrote down is FALSE stated like that. Don't you see that? * I repeat: you do not understand the difference between bound and free * variables. * * I disagree a free variable is not a constant. * A free variable behaves like a constant. * * No a constant is always the same constant, it is never substituted by * something else, it is "immutable". * * A variable is a placeholder for a Term ( a constant is a special term) *I see where you are heading. In the reduction laws, you substitute for free *variables. This is true, but you can only substitute for a free variable if it *was bound in an outer scope, and you are stripping off the binding, as in the *beta-equality for lambda-calculus, which I will repeat: I am not talking about reduction laws * (\x - P(x)) t = P(x) [t/x] *You cannot simply substitute any value you please for an arbitrary free *variable and expect the new term to be equal to the old one. For example in *Haskell, fst :: (a,b) - a is a free variable in every term (where it's not *shadowed). Now if I have the term * fst p *and I substitute snd for fst: * (fst p) [snd/fst] = snd p *but * fst p /= snd p *which demonstrates that substitution on free variables is not sound in *general. No you still don't understand me * This is the reason for abstraction: it asserts that a free variable *in the scope of the abstraction can range over the whole domain, so any *substitution will preserve equality. It is exactly the same with forall. * It is not "implicitly" * quantified in any way, because it denotes a specific element. The only * difference between a constant and a free variable is syntactic: a free * variable can be bound in an outer scope, * * No the real role of a variable say x in a formula alpha(x) or a term T(x) * is a PLACEHOLDER ready to be substituted by a Term (e.g. constant or a * parameterized term) * * And that's the reason why I should find it weird if In Haskell 98+ one * would distinguish between * * a - a and [forall a. a - a] * * while a constant cannot. * * The sentence "alpha(x)" asserts that there is a _distinguished_ * element * named * * NO , saying that there is a distinguished element T that satisfies * alpha * implies * * that exists x. alpha(x) is true * * Yes, it also impli
Re: more detailed explanation about forall in Haskell
As Mark Jones has allready said this thread should end or come to a conclusion. Unfortunately he said more than that . He said that the discussion was all about the difference a - a and forall a. a - a . And that's not true . One only has to read the first 2 or 4 emails about this thread of discussion. I can't resist another comment. I think you are both right here. In Haskell there are no free type variables, it just looks as if there is because of a Haskell convention. If you write f :: a - a it really means f :: forall a . a - a So if "a - a" appears as a type signature it is indeed equal to "forall a . a - a" because Haskell has implicit forall quantifers for the free type variables of a signature. On the other hand, if we talk about a subexpression having type "a - a" (which there is no syntax for in Haskell) this does not imply that it has type "forall a . a - a", but rather that it has a type where the variable "a" has been bound in some outer scope. I think the source of all this debate is the convetion that type variables are implicitely quantified. I agree with Jon here, it was a mistake. -- Lennart
RE: more detailed explanation about forall in Haskell
Jan Brosius wrote: look at this example: alpha(x) == x is_an Integer = x^2 -1 this is an example of a formula that is true *If you want to come up with your own logic, where alpha(x) is equivalent to *forall x. alpha(x), then that's fine. No, if alpha(x) is a true formula then forall x. alpha(x) is again a true assertion I think part of the confusion here has to do with the notation alpha(x). The traditional mathematical notation f(x) is ambiguous. It may either refer to an abstraction or an application. In this regard, lambda notation is much superior. What does the alpha(x) here mean? If we assume it is a function like: alpha = \ x . (x is_an Integer = x^2 -1 ) then it is meaningful to debate whether or not the inner 'x's refer to the same x as the lambda bound x or whether "x is_an integer" creates a new binding. On the other hand, if we assume that alpha(x) is an application of alpha to x then the debate seems to be whether x refers to some value, or whether it is simply a place-holder. Perhaps Jan can clarify what is meant here. --Peter Douglass
Re: more detailed explanation about forall in Haskell
Peter Hancock writes: [..] Please guys, you are making clowns of yourselves. Amen to that! I've just added the above subject line to my kill file, rather than stop reading the Haskell list altogether. --KW 8-) -- : Keith Wansbrough, MSc, BSc(Hons) (Auckland) ---: : PhD Student, Computer Laboratory, University of Cambridge, UK. : : Native of Antipodean Auckland, New Zealand: 174d47'E, 36d55'S. : : http://www.cl.cam.ac.uk/users/kw217/ mailto:[EMAIL PROTECTED] : ::
Re: more detailed explanation about forall in Haskell
Fri, 19 May 2000 14:48:24 +0200, Jan Brosius [EMAIL PROTECTED] pisze:
On the other hand someone's remark and about the meaning Haskell gives to
these two types and I wonder since today if one means by a - a a type
indication to be understood as a function having this type signature
means that the function is only defined for some a 's and by forall a.
a - a a type indication to be understood
as a function that is really defined for ALL type's a .
Not quite. Let's have an example:
rep:: Int - (a - a) - (a - a)
rep 0 f = id
rep n f = f . rep (n-1) f
What is the type of f inside rep?
It is not "forall a. a - a". If it was, one could write
rep 0 f = if f True then id else undefined
and it would not have any semantics, because one can pass the function
"\x - x+1" as the second argument of rep.
It is not "exists a. a - a". If it was, one could not write the
second equation for rep, because the function "not" should have the
type "exists a. a - a" too, and it clearly cannot be used instead of
"f" in the second equation. In other words, the fact that exists some
type "a" for which "f" has the type "a - a" does not guarantee that
this is exacly this "a" that is needed here.
So what is the type of f?
Answer: it is "a - a", where "a" is bound by the fact that rep is
polymorphic. It is bound by an implicit kind-of-lambda over types
at the definition of rep.
You cannot write such type in a standard Haskell program, i.e. you
cannot change "f" in the body of rep by "(f :: sometype)", for any type
expression "sometype". But this type, depending on instantiation of a
polymorphic function it is used in, clearly exists, has well-defined
semantics, and is extremely useful.
I am well aware that the predicates (I would prefer to speak about
functional relations) Free ( ) and Variable( ) are NOT IMPLEMENTED
yet , so up to now these predicates serve only the purpose of an
additional documentation ;
They don't have any semantics defined yet. I mean not informal
explanation what they mean, but how they fit into the type system
of Haskell, what are the typing rules.
I'm afraid it cannot be done in any useful way.
But I think they might be useful.
E.g. let's trying to say that instead of the function
pr2:: (a, b) - b
pr2 (x,y) = y
I wanted a slightly differing function
pr2':: forall a. [forall b `notin Free(a) . (a,b) - b]
pr2' (x,y) = y
What do you gain by the restriction of type of pr2', compared to
pr2? How can the body of a function make use of the restriction? If it
cannot, I don't see why to complicate the type system by introducing
useless constructs.
But first, we must know what it means at all.
With the above I filter out all arguments having a type of the form
(a, T(a)) ;
f:: forall c. c - [c]
f y = let g x = pr2' (x, y) in ...
Does the above compile when we replace "..." with something of the
right type (e.g. []), and if so, what is the inferred type of g as
seen inside "..."?
--
__("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-
Re: more detailed explanation about forall in Haskell
hello, i have been following the evolution of haskell for about 2 years now in my spare time, but haven't had time to really get into haskell programming. so i am not an expert or anything. i do not see the need for the "forall" quantifier to be written explicitly however, and i quite like the way haskell currently deals with the situation. here is how i think about functions and their types. i would be glad if someone points out any mistakes i made, as (as i wrote above) i am by no means an advanced haskell user and am still learning. anyways here we go: 1) f :: Int f is of type integer 2) f :: Int - Int f is a function, which given an integer produces and integer 3) f :: a f is of types 'a', where 'a' denotes some type (since we haven't imposed any restrictions on 'a' it can be any type, so the implicit universal quantification done by haskell makes sense) (would bottom be of this type?) 4) f :: a - Intf is a function, which given an object of some type 'a' returns an integer (i.e. f does not assume anything about what its parameter might be, so f works on paramters of any type) 5) f :: a - a f is a function, which given an object of some type 'a' returns an object of the *same* type 'a' 9again no restrictions on what 'a' might be) 6) f :: (Eq a) = a f is of type 'a', but 'a' is of class Eq, so now we have imposed some restrictions on the types of which f can be, i.e. any type, which can deal with equality 7) f :: (Eq a) = a - Int is a function, which assumes that its parameter can deal with equality (so the function can compare the parameter to things for equality). however it does not assume anything else about its parameter. etc... so my questions are: 1) what would it mean if one writes f :: a (in general: how does one think of unbound type variables)? this is i think what the big discussion was all about, here are the solutions i can see: 1.1 this is an ivalid expressions, but then we get a more verbose version of what we have at the moment, is it worthed? 1.2 it is a valid expression and is the same as f :: forall a.a , i.e. it is implicitly universally quantified by haskell, so f :: forall a.a and f :: a is really the same thing. the probelm with this is that there is more than one way to write the same thing and will probably confuse the issue even more. 1.3 it is a valid expression, but has some other meaning, but what? 1.4 f is a type variable :-) . i just tought of this now, and i think this *really* will confuse things 2) how will one write constraints on the types (e.g. as in (7) above)? i presume that since with the 'forall' we get the whole scoping thing, so the constraints have to be written per quantifier, i.e. something like: f :: forall a of_class Eq. (a - Int) but what about: f :: forall a of_class Eq. forall a.a now i think f :: forall a.a something like this may happen in a large type expressions (and with 'forall' they will become quite large), when one renames variables, and accidentally a type variable might get bounded by the wrong quantifier. 3) is 'forall' going to be used at the type level as well, i.e. would one have to write: data forall a. BinaryTree a = Empty | BT a (BinaryTree a) (BinaryTree a) 3.1 now as far as i understand BinaryTree is of kind * - * (ie a type constructor), which is different to * would the 'forall' for types range over * only, or both? 4) why is 'forall' needed? could someone plese give an example. thanks yavor -- iavor s. diatchki university of cape town email: [EMAIL PROTECTED] web:http://www.cs.uct.ac.za/~idiatchk
Re: more detailed explanation about forall in Haskell
From: Peter Douglass [EMAIL PROTECTED] To: 'Jan Brosius' [EMAIL PROTECTED]; Frank Atanassow [EMAIL PROTECTED] Cc: [EMAIL PROTECTED] Sent: Friday, May 19, 2000 6:03 PM Subject: RE: more detailed explanation about forall in Haskell | Jan Brosius wrote: | | look at this example: | | alpha(x) == x is_an Integer = x^2 -1 | | this is an example of a formula that is true | Sorry, this is not my logic. Since this formula is "true" it is allowed to be generalized forall x . alpha(x) == forall x. (x is_an Integer = x^2 -1) and this may be rewritten in a more known form forall x. alpha(x) == [forall x is_an Integer. (x^2 -1)] or still another way forall x. alpha(x) == [forall x `element_of` N) .( x^2 -1)] (where N denotes the set of integers) which can be read as " forall x element of the set of integers N , x^2 -1 " The forall in the above expression is an example of a bounded forall. It is also an example of a so called closed formula (because having no free variables anymore ) or also called a sentence. An other example , let R be the set of real numbers and we want to express that the square of a real number is always = 0 then on can write beta == [forall x `element_of R . ( x^2 = 0)] then by definition of a bounded forall : beta == [forall x . (x `element_of R = x^2 = 0 )] and define next : alpha (x) ==( x `element_of R = X^2 =0 ) Next remember that everybody agreed that the following is a TRUE implication: (*) forall x . alpha(x) = alpha(x) Finally remember that the Modus Ponens rule gives us a way to derive new theorems from implications : P = Q true Ptrue *** Q true Then I get [forall x . alpha(x)] = alpha(x) (true) forall x . alpha(x) (true) *** alpha(x) (true) So we get the true formula alpha(x) where x is free. I only wanted to state that this is not my logic and that IF one accepts the validity of the Modus Ponens rule and the fact agreed by everybody that the implication [forall x . alpha(x)] = alpha(x) is true, then one HAS to accept that the following formula alpha(x) is true. Finally, since I have been attacked by someone to have misread Bourbaki's book , well here you have something: Book entitled : " N. Bourbaki Elements de Mathematique editor : Hermann, Paris 1970 page: E I.39 Theoreme 1. - x = x " Designons par S la relation x = x de T0. .. For those who don't know French : In Bourbaki one proves theorem 1 : x = x this shows that alpha(x) == x = x is a true formula in a quantified theory with an equal sign A message to the one who liked to ridiculize me so much : If you don't agree with all this , please send your comments directly to Bourbaki (a famous french society of mathematicians ) , say to these mathematicians they are a laughing stock for all logicians from the time of Tarski , Gentzen and ... your name . Please don't forget to put a stamp on the envelope ( joke about Dutch). I hope that this will settle once and for all that this is not my logic , but I appreciate it much that you (the person in Dutch - land) want to give me full credit of their work. | *If you want to come up with your own logic, where alpha(x) | is equivalent to | *forall x. alpha(x), then that's fine. | | No, if alpha(x) is a true formula then forall x. alpha(x) is | again a true assertion | | I think part of the confusion here has to do with the notation alpha(x). | The traditional mathematical notation f(x) is ambiguous. It may either | refer to an abstraction or an application. In this regard, lambda notation | is much superior. What does the alpha(x) here mean? | If we assume it is a function like: | alpha = \ x . (x is_an Integer = x^2 -1 ) | then it is meaningful to debate whether or not the inner 'x's refer to the | same x as the lambda bound x or whether "x is_an integer" creates a new | binding. | On the other hand, if we assume that alpha(x) is an application of alpha | to x then the debate seems to be whether x refers to some value, or whether | it is simply a place-holder. | Perhaps Jan can clarify what is meant here. | --Peter Douglass | | | | Still friendly greetings Jan Brosius
Re: more detailed explanation about forall in Haskell
Fri, 19 May 2000 19:47:38 +0200, Iavor Diatchki [EMAIL PROTECTED] pisze: i do not see the need for the "forall" quantifier to be written explicitly however, It is needed when the quantifier is inside a function argument, to spell the difference between f1 :: forall a. ([a] - [a]) - [a] - [a] and f2 :: (forall a. [a] - [a]) - [a] - [a] the second being the same as f2 :: forall a. (forall b. [b] - [b]) - [a] - [a] What is the difference? f1 cannot assume anything about "a". It only knows that the function passed as the first parameter can be applied to a value of the same type as the second parameter, yielding the same type, and that this type is a list of something. f2 can use its first parameter for any type "a" it chooses, even for different types in different places. For example to apply it to [False,False,True] and check if the first element of the result is True. When calling f1, we can pass it a function [Int]-[Int] and a list of Ints, or similarly for another type. OTOH as the first argument of f2 we must pass a polymorphic function that will accept any list, independently of the second argument. For example id, reverse, List.cycle, (take 5) and (\x - x++x) are OK, but sort is not. I am generally talking about Haskell with GHC and Hugs extensions. Standard Haskell does not have explicit foralls, one cannot define a function like f2 in it, and one cannot write a type signature depending on type variables that are bound outside. forall is also used in local universal quantification and local existential quantification in data types - both are language extensions. I will not write about them here. and i quite like the way haskell currently deals with the situation. Me too. Since in 99% of cases the quantifier is at the top of the signature, I like having it implicit in those cases, although it causes troubles (see below). Some people get confused, but IMHO they would get confused even when explicit forall was mandatory - the problem is in them, not in Haskell's syntax. 3) f :: a f is of types 'a', where 'a' denotes some type This descripton looks unclear for me. I hope you meant that f can be used as a value of any type the caller chooses. So the caller can use f as a String. OTOH there is no much freedom in implementation of f, The only choice is bottom, and it can only be spelt differently: f = f f = undefined f = error "foo" They are theoretically the same, but in practice their effects are different. 4) f :: a - Int f is a function, which given an object of some type 'a' returns an integer In other words, the caller can choose a type for "a" and use "f" as the type "a - Int". This does not explain the intuitive meaning of "f" so well, but allows uniform understanding of all polymorphic types. so my questions are: 1) what would it mean if one writes f :: a (in general: how does one think of unbound type variables)? This type signature in program source means the same as "f :: forall a. a". Except two cases: - In a method signature inside class declaration, when "a" was in the class head. It means that f will have the type "forall a. Class a = a". - With GHC and Hugs extension of pattern type signatures, it means "f :: a" (for "a" bound outside) if "a" was indeed bound outside by a pattern type signature. Example: g :: b - b -- The name "b" here is independent of all other names, g (x::a) = -- but the name "a" defined here can be used below: ... where f1 :: a -- The type of f1 is the same as of g's argument. -- It is not implicitly quantified by forall here! f2 :: b -- The type of f2 is forall b. b. -- This is the same type as forall z. z, etc. f3 :: forall a. a -- The type of f3 is the same as of f2. -- Thus forall can be used to be sure that we introduce -- a new type variable, and not mention one bound outside. When you use "f :: a" in an expression, not in a type signature among declarations, in GHC these rules apply too. In standard Haskell the second rule obviously does not apply, because there are no pattern type signatures, but the first does not apply either, which is not very obvious (one has a chance to write such expression in the default implementation of a method). In Hugs these rules don't apply for types in expressions, but maybe they will, I don't know. 2) how will one write constraints on the types (e.g. as in (7) above)? i presume that since with the 'forall' we get the whole scoping thing, so the constraints have to be written per quantifier, i.e. something like: f:: forall a of_class Eq. (a - Int) No. The context is always written just inside forall, no matter if forall is explicit or not: f :: forall a. Eq a = a - Int Similarly for local quantification: g :: Ord b = (forall a. Eq a = [a] - [a]) - [b] - [b] It does not make sense to write context together with forall when we have
Re: more detailed explanation about forall in Haskell
Thanks for your comments. They are to the point. But the first email arose from the fact that someone else claimed that the forall quantifier was used in the same way as in (say "classical") logic. I still claim that everything could be put in a classical logic framework, which is then another framework than the one proposed in Haskell Very friendly Jan Brosius - Original Message - From: Lars Lundgren [EMAIL PROTECTED] To: Jan Brosius [EMAIL PROTECTED] Cc: [EMAIL PROTECTED] Sent: Wednesday, May 17, 2000 10:56 AM Subject: Re: more detailed explanation about forall in Haskell On Tue, 16 May 2000, Jan Brosius wrote: - Original Message - From: Lars Lundgren [EMAIL PROTECTED] Sent: Tuesday, May 16, 2000 1:54 PM Subject: Re: more detailed explanation about forall in Haskell On Tue, 16 May 2000, Jan Brosius wrote: Ok I understand this isomorphism better. However this remark seems to be of no value to functional programmers. Why trying to mix terms( otr types) with relations ? What is a 'type' in your oppinion? I look at it as a set (either a variable set or a specific set). E.g. I look at Bool as a specific set which itself contains values True , False that are not sets. Next I interpret something like f :: a - Int as a family (indexed by a) of functions of " set" a into set Int. So in other words, f will map any value - given that it is an element of the right set (i.e given that it satisfies the precondition) to a value that is an element of Int - sounds like a postcondition to me. I didn't come into problems by this interpretation after having read the Haskell's User Guide. Which is my only general source about Haskell. It is up to someone else to say if such an interpretation shall lead into misinterpretation. I think Haskell will not be attractive to mathematicians if types MUST be read as formula's . But of course, that is not the case, but it might help if you want to understand the rationale behind the choice of name for the type quantifier "forall". If that is the case I can only say that I find the term "functional programming" a bit strange. Isn't a type a statement about pre- and post-conditions, i.e. a formula? I can't answer this since I have never read the definition of a type in say typed lambda calculus. I wasn't after a definition, I just tried to explain that it is quite natural to view types as formulas, and that it is not in conflict with other views. (and it is not restricted to type systems for fp languages) I have a book about logic that deals about plain lambda calculus and that deals about "restricted" typed lambda calculus (where a type is not considered as a formula). I never read the definition of Hindley-Milner types. If you read the typing rules, remember to have a reference of the natural deduction rules with you... And the only introduction about types were the general user's guides from Clean , SML , Ocaml and of Haskell. If you are interested in systems that exploit the isomorphism further you can take a look at : cayenne, agda, alfa from: http://www.cs.chalmers.se/Cs/Research/Logic/implementation.mhtml /Lars L
Re: more detailed explanation about forall in Haskell
From: Frank Atanassow [EMAIL PROTECTED] To: Jan Brosius [EMAIL PROTECTED] Cc: [EMAIL PROTECTED] Sent: Wednesday, May 17, 2000 1:35 PM Subject: Fw: more detailed explanation about forall in Haskell Jan Brosius writes: Why do some computer scientists have such problems with the good logical forall and exist. Remember that good old logic came first. On it was build SET theory. On it was built topological space To prove some theorem in lambda calculus one used a topological model. You see : good old logic came FIRST afterwards came theorems of typed lambda calculus . This is not the sophistic question : what came first : the egg or the chicken. NO good old logic came first . Your argument is absurd and irrelevant. SORRY, this is quite TRUE , in fact [forall x. alpha(x)] = alpha(x) Here, I have to say that the above equivalence is false . SHAME on me. I must put this in the good way; [forall x . alpha(x)] = alpha(x) is True If alpha(x) is TRUE then the following is true : alpha(x) = [forall x. alpha(x)] So if alpha(x) is TRUE then [forall x. alpha(x) ]= alpha(x) Sorry for the error the above true equivalence seems to be easily considered as wrong . Why? Because alpha(x) is TRUE can be read as alpha(x) is TRUE for ANY x. I think this is one of the roots of your misconceptions. These two propositions are certainly not equivalent. Maybe it is because you have been told that, in Haskell, syntax we typically elide the "forall" quantifier. The sentence "alpha(x)" asserts that there is a _distinguished_ element named NO , saying that there is a distinguished element T that satisfies alpha implies that exists x. alpha(x) is true So the following implication is true (T | x) alpha(x) = exists x. alpha(x) that is , if alpha(T) is true then [exists x. alpha(x)] is true more precisely , let c be a constant , and if alpha(c) is true then you can say that exists x. alpha(x) is true. "x" in the domain of your model, and that that element, at least, satisfies x is a variable ; no domain ; no model "alpha". The sentence "forall x. alpha(x)", OTOH, asserts that _any_ element in your domain satisifies "alpha". So if your domain is a set D, then a model of "alpha(x)" needs a subset C of D to interpret "alpha", along with a member X of C to interpret "x", and the sentence is true iff X is in C. OTOH, a model of "forall x. alpha(x)" needs only the subset C, and is true iff C=D, since it asserts that for any element Y of D, Y is in C. In Haskell the situation is complicated by the fact that there are no "set-theoretic" models (are you even aware that Haskell's type system is unsound?), and the fact that the domain is multi-sorted. But those facts do not bear on the distinction between the two terms on either side of the equivalence above. Very friendly Jan Brosius -- Frank Atanassow, Dept. of Computer Science, Utrecht University Padualaan 14, PO Box 80.089, 3508 TB Utrecht, Netherlands Tel +31 (030) 253-1012, Fax +31 (030) 251-3791
Re: more detailed explanation about forall in Haskell
Sorry, if in some way I have upset you Sincerely Jan Brosius From: Frank Atanassow [EMAIL PROTECTED] To: Frank Atanassow [EMAIL PROTECTED] Sent: Wednesday, May 17, 2000 1:50 PM Subject: Fw: more detailed explanation about forall in Haskell Frank Atanassow writes: Jan Brosius writes: Why do some computer scientists have such problems with the good logical forall and exist. Remember that good old logic came first. On it was build SET theory. On it was built topological space To prove some theorem in lambda calculus one used a topological model. You see : good old logic came FIRST afterwards came theorems of typed lambda calculus . This is not the sophistic question : what came first : the egg or the chicken. NO good old logic came first . Your argument is absurd and irrelevant. I take it back. There is no argument here, only the childish insinuation that "my daddy can beat up your daddy". So there. blt! -- Frank Atanassow, Dept. of Computer Science, Utrecht University Padualaan 14, PO Box 80.089, 3508 TB Utrecht, Netherlands Tel +31 (030) 253-1012, Fax +31 (030) 251-3791
Re: more detailed explanation about forall in Haskell
Jan Brosius writes: I must put this in the good way; [forall x . alpha(x)] = alpha(x) is True Yes, by instantiation. If alpha(x) is TRUE then the following is true : alpha(x) = [forall x. alpha(x)] No, alpha(x) only asserts that some element named x satisfies alpha. It does not follow that therefore every other element also satisfies alpha. So if alpha(x) is TRUE then [forall x. alpha(x) ]= alpha(x) This does not follow. It is truth-equivalent to: [forall x. alpha(x)] = True which is equivalent to: forall x. alpha(x) which is only true when every element satisifies alpha; so it is not a tautology. I repeat: you do not understand the difference between bound and free variables. A free variable behaves like a constant. It is not "implicitly" quantified in any way, because it denotes a specific element. The only difference between a constant and a free variable is syntactic: a free variable can be bound in an outer scope, while a constant cannot. The sentence "alpha(x)" asserts that there is a _distinguished_ element named NO , saying that there is a distinguished element T that satisfies alpha implies that exists x. alpha(x) is true Yes, it also implies this fact, because it can be derived by extensionality: alpha(x) = exists y. alpha(y) However, existential quantification hides the identity of the element in question. The fact that we know _which_ element it is that satisifies alpha permits us to say more. This is why: exists x. alpha(x), alpha(x), and forall x. alpha(x) are not truth-equivalent. Rather we have: forall y. alpha(y) = alpha(x) and alpha (x) = exists z. alpha(z) "x" in the domain of your model, and that that element, at least, satisfies x is a variable ; no domain ; no model A model must assign an element in the domain to each free variable. You need a model to determine the truth-value of a first-order proposition which is not tautological. We are trying to establish the truth-value of a proposition with a free variable; therefore we need a model. A model needs a domain of elements to draw from. Therefore we need a domain. OK? -- Frank Atanassow, Dept. of Computer Science, Utrecht University Padualaan 14, PO Box 80.089, 3508 TB Utrecht, Netherlands Tel +31 (030) 253-1012, Fax +31 (030) 251-3791
Re: more detailed explanation about forall in Haskell
From: Frank Atanassow [EMAIL PROTECTED] To: Jan Brosius [EMAIL PROTECTED] Cc: [EMAIL PROTECTED] Sent: Thursday, May 18, 2000 2:53 PM Subject: Re: more detailed explanation about forall in Haskell Jan Brosius writes: I must put this in the good way; [forall x . alpha(x)] = alpha(x) is True Yes, by instantiation. I disagree. If alpha(x) is TRUE then the following is true : alpha(x) = [forall x. alpha(x)] No, alpha(x) only asserts that some element named x satisfies alpha. It does not follow that therefore every other element also satisfies alpha. No the variable x means that it can be substituted by any term. That is the real meaning of a variable (at least in classical logic). Consider e.g. Carl Witty's formula : prime(x) == x is a prime number. Then prime(2) == (2|x) prime(x) is true , and prime (4) is false Take something else alpha(x) == prime(x) AND ¬ prime(x) ( ¬ signifies not) then alpha(x) is a false formula and you have ¬ [exists x. alpha(x)] On the contrary beta(x) == ¬ alpha(x) is true for any x So if alpha(x) is TRUE then [forall x. alpha(x) ]= alpha(x) This does not follow. It is truth-equivalent to: Sorry, I disagree [forall x. alpha(x)] = True ( In the above you should at the very least not forget to mention that [forall x. alpha(x)] must be true ) In principle True is a sloppy expression for saying that [forall x . alpha(x)] is a theorem of some mathematical theory. I have used True because discussing mathematical theories would have lead the discussion out of the scope of the discussion. For instance let "T=" denote a mathematical theory with equality then one has "T=" -| x = x that is the formula x = x is a theorem in "T=" . More sloppy the formula x=xis TRUE in "T=" which is equivalent to: forall x. alpha(x) which is only true when every element satisifies alpha; so it is not a tautology. I repeat: you do not understand the difference between bound and free variables. I disagree a free variable is not a constant. A bound variable is a variable tied to a quantifier. In principle a bound variable is not visibly. This is best illustrated by Bourbaki's approach where they first define : exists x . alpha(x) == (`t x (alpha)| x) alpha where if e.g. alpha(x) == x = x then `t x (alpha) == `t ( `sq = `sq ) where `sq denotes a small square and where here both `sq are tied to `t by a line In this way I can really say that in [existx x. x = x] the variable x has disappeared. Finally Bourbaki defines forall x . alpha(x) == ¬ [exists x . ¬ alpha(x)] I repeat : there are no domains in propositional calculus , but I am aware that in some text books about propositional calculus one speaks about it , I regard this as cheating : introducing a concept that one is going to define later. I remember my prof, in logic in 1 cand. math - physics where his first lesson began by writing on the blackboard : p V ¬ p and he only said " p or not p " " tertium non datur" " a third possibility is not given " His whole course was as formally as possible, and variables were not supposed to range about a domain. A free variable behaves like a constant. No a constant is always the same constant, it is never substituted by something else, it is "immutable". A variable is a placeholder for a Term ( a constant is a special term) It is not "implicitly" quantified in any way, because it denotes a specific element. The only difference between a constant and a free variable is syntactic: a free variable can be bound in an outer scope, No the real role of a variable say x in a formula alpha(x) or a term T(x) is a PLACEHOLDER ready to be substituted by a Term (e.g. constant or a parameterized term) And that's the reason why I should find it weird if In Haskell 98+ one would distinguish between a - a and [forall a. a - a] while a constant cannot. The sentence "alpha(x)" asserts that there is a _distinguished_ element named NO , saying that there is a distinguished element T that satisfies alpha implies that exists x. alpha(x) is true Yes, it also implies this fact, because it can be derived by extensionality: alpha(x) = exists y. alpha(y) However, existential quantification hides the identity of the element in question. The fact that we know _which_ element it is that satisifies alpha permits us to say more. This is why: exists x. alpha(x), alpha(x), and forall x. alpha(x) are not truth-equivalent. Rather we have: forall y. alpha(y) = alpha(x) and alpha (x) = exists z. alpha(z) AND ifalpha(x) is a TRUE formula then alpha(x) = forall x. alpha(x) A better way to express this is Rule of genaralization: alpha(x ) is True (and x is a variable) forall x . alpha(x ) is true I repeat that my use of true or false
Re: more detailed explanation about forall in Haskell
I'm reluctant to get involved in this discussion, cheifly because it seems to me that Jan is attacking a position that has quite a long history with (inter alia) the argument that a different position has a longer history, which doesn't strike me as terribly likely to lead to insight. Also my present powers of concentration don't allow me to keep up with the argument, so I'll just drop in a couple of points and duck out again. [Lars asked] What is a 'type' in your oppinion? [Jan replied] I look at it as a set (either a variable set or a specific set). E.g. I look at Bool as a specific set which itself contains values True , False that are not sets. Next I interpret something like f :: a - Int as a family (indexed by a) of functions of " set" a into set Int. [snippety] It is up to someone else to say if such an interpretation shall lead into misinterpretation. Interpreting types as sets is not straightforward: try "Types are not sets" by James H. Morris, JR. in POPL 1973 as one pointer into this area. I think Haskell will not be attractive to mathematicians if types MUST be read as formula's . If that is the case I can only say that I find the term "functional programming" a bit strange. I don't think anyone said that they must. They can be, and one useful way of interpreting a type is as a statement of limitations on the use and behaviour of a term. f :: A - B can be read as "if x is of type A, then f x will be of type B" x :: forall a . E can be read as "for all types A, x :: E [A/a]" I think the major source of confusion is that Haskell started out using the convention that a type expression containing a free variable was understood as being universally quantified at the top level (a convention which, I might add, I argued against in the first Haskell committee, so nyaa...), but then added 'forall' as an extension later (I thought this was going to happen :-)) Apart from that, I think that (once they have had the conventions and notation described to them) most mathematicians are not going to be put off by the type system. Certainly mathematicians must be warned against interpreting types simply as sets, but they also need to be warned that a "function" is not a function in the mathematical sense either, being constrained by the limits of computation. Isn't a type a statement about pre- and post-conditions, i.e. a formula? I'd say that's another reasonable way of reading them. I can't answer this since I have never read the definition of a type in say typed lambda calculus. Go on then! It won't hurt! Cheers, Jón -- Jón Fairbairn [EMAIL PROTECTED] 18 Kimberley Road[EMAIL PROTECTED] Cambridge CB4 1HH+44 1223 570179 (after 14:00 only, please!)
Re: more detailed explanation about forall in Haskell
Ok I understand this isomorphism better. However this remark seems to be of no value to functional programmers. Why trying to mix terms( otr types) with relations ? Anyway, in intuitionistic logic it is natural indentify proofs and programs and proposition and types. Maybe best illustrated by the BHK (Brouwer-Heyting-Kolmogoroff) semantics: A proof of a /\ b is a proof of a and a proof of b, hence a /\ b = (a,b) Sorry, are you going to say that a tuple (a,b) is the same as " a AND b " Not quite. He said that tuples and logical conjunctions are often identified in some logics. Here's an explanation attempt from a non-specialist: In some logics (keywords: intuitionistic, constructive), propositions are not accepted as true unless they come with an explicit, constructive proof. This has useful applications for typed programming languages. Read types as claims of existence (e.g., "Bool" interpreted as a proposition means "there are booleans", and in general, a type "t" when interpreted as a proposition, means "there are objects of type t"). Now, the core of constructive logics is that we do not accept such claims to be true unless we are given an example, or at least a method by which such a concrete example can be constructed. For base types such as "Bool", this is quite simple (*), as we can give some example objects, each of which is a proof of our claim True :: Bool-- read: "True" is a boolean (so there are booleans) False :: Bool -- read: "False" is a boolean For complex types constructed from simpler types, we can give proofs constructed from the simpler proofs that prove the existence claims for the element types. (Int,Bool) -- read: there are pairs of integers and booleans (1,False)::(Int,Bool) -- read: "(1,False)" is such a pair To proof the existence of pairs of integers and booleans, I have to prove the existence of integers AND I have to prove the existence of booleans. Also, I cannot simply say "'Int and Bool' is true because I've seen proofs for 'Int' and for 'Bool' - trust me!". In constructive logic, you won't believe me without the constructive proof. So I have to package my two proofs for "Int" and for "Bool" into one pair of proofs. And if I have a proof for the existence of pairs, I can extract from it the proofs for its component types. This is why pairs correspond to conjunctions in such a logic. With these examples, Thorsten's brief summary (with the slight corrections noted earlier) should make sense, I hope, but for completeness: Either a b -- read: there are objects of type a OR there are objects of type b -- to prove this I can either give a (non-bottom) object/proof of type a -- OR a (non-bottom) object/proof of type b, -- so this corresponds to a disjunctive proposition a - b -- read: provided that there are objects of type a, -- there are objects of type b -- to prove this, I have to give an object of type b, -- but I may assume that I have an object of type a at hand -- so this corresponds to an implication In formal logic we say just this a (true) a = b (true ) * b (true) Which happens to correspond to the typing rule for function application: x :: a f :: a - b -- f x :: b Given a proof for "as exist" and a proof for "if as exist, then bs exist as well", we can construct a proof that "bs exist" by simply applying the proof for the implication to the proof of its assumption; evaluating the function applications corresponds to simplifying the proof (we hope). As an example how do we prove (a \/ b) /\ c - (a /\ c) \/ (a /\ b) in Haskell ? lem :: (Either a b,c) - Either (a,c) (b,c) lem (Left a,c) = Left (a,c) lem (Right b,c) = Right (b,c) Sorry I don't have to know all this , do you really think I am illiterate in propositional logic or boolean algebra The beauty of this correspondence (or isomorphism) is that you can use what you already know (about logic) in a new context (types). lem can be interpreted as a proof for the proposition corresponding to its type (it constructs a proof for the right-hand side from a proof of the left-hand side). The main caveat is the insistence on constructive proofs (in the classical logic most of us tend to learn, there is this favourite proof technique: if I assume that xs don't exist, I am led to a contradiction, so xs have to exist, even if I haven't seen any of them yet - this is not acceptable in constructive logics). [haven't read the papers on a correspondence for classical logic yet, but I assume they exist, for otherwise I would contradict Frank Atanassow ;-] The disputed forall is just the (2nd order) quantification over all propositions. forall a,b . (a, b) - b -- read: for all (types) a and for all (types) b, if (a proof exists that) -- a(-typed objects)s exist and (a proof exists that) b(-typed objects)s -- exist,
Re: more detailed explanation about forall in Haskell
I reply , but I like to make some comments before:
As readers would have noticed from the former email my answers are put here
in a different context.
This might give the reader the false impression that I made some serious
mistakes in the formal
email.
Fri, 12 May 2000 00:42:52 +0200, Jan Brosius [EMAIL PROTECTED]
pisze:
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)
Here you have omitted something of the former email . By doing that the
context of the below has changed.
Readers may think that I committed an error! Is this a HONEST way to reply?
Let's start
v has type STRef s a
...for "s" and "a" coming from the instantiation of a polymorphic
function "f". Yes.
Next one sees that below something is reproduced but out of the context of
the former email.
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.
where "s1" is free (thus can be later generalized over) and "s" and
"a" come from the environment inside "f" (thus are monomorphic).
Really? are there now 2 sorts of variables , variables that are variables
and variables that are not variables?
Interesting?
It would have the type you wrote if "v" was created in this thread.
??
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.
Why then doen't you repeat it here? Because this is most interesting for the
reader.
In which email have you told it ? In a private email ? or in the
Haskell-list?
IT DOES : that is a well known rule of forall (forall x,y . alpha(x.y)
=
forall x. alpha(x,x) )
I see no "forall s" in the left type.
I shall make it easier:
forall s1. ST s1 T(s) is EQUIVALENT with forall s1,s. ST s1 T(s)
Now forall s1.s ST s1 T(s) IMPLIES ( =) forall s1. ST s1 T(s1)
Marcin, forall s1 . alpha(s1,s) is EQUIVALENT with alpha(s1,s)
One has alpha(s1,s) IMPLIES alpha(s,s) and the latter is EQUIVALENT to
forall s. alpha (s,s)
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':: ST s Int - Int
runST' x = ...
Inside the body of runST' "x" has the type "ST s Int", with "s"
taken from the environment.
s is here a type variable , isn't it?
When runST' will be later applied to a value of the type "ST s Int"
with "s" free, "x" will have the type "ST s Int" with nothing more
known about "s". (If runST was applied to this value directly, it
would be OK.)
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
Has something changed in the documentation?
But you have to compile runST' _now_, and decide whether the first
argument of ST from the type of "x" is a type variable.
Haskell does not have this problem. It does not ever check if a type
is a type variable, but if it is a _free_ type variable, i.e. one
that can be generalized over.
what's the difference between a -free-type variable and a type variable (if
not
bound by a quantifier)?My, my!! Haskell is even more difficult than I
thought.
runST':: forall s. ST s Int - Int
runST' x = runST x
Should it compile with your type of runST?
"my" type of runST is nothing else but the official runST .
So, I expect that if s is instantiated to the type RealWorld you will get a
problem,
since is not defined for s = RealWorld because runST will not work with
with s= RealWorld.
So, you should get (I guess) an error.
function runST are fullfilled . So ("my") runST will work.
With this I mean MORE "my" runST is nothing but the OFFICIAL runST.
So I see that your runST' is only partially defined
, like e.g. head :: [a] - [a] where in the definition one does not
consider the case [a] == [] .
Now I write
len :: Int
len = runST' (liftM length (readFile "foo") :: ST RealWorld Int)
which creates a global value of type Int which changes in time. Oops!
Oops! Did the above program work in Hugs ? Or did it come from your
imagination?
VERY FRIENDLY
JAN BROSIUS
--
__("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-
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)),
thus the type of newSTRef must be as in Haskell, not as you say.
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.
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.
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-
Re: more detailed explanation about forall in Haskell
On Tue, 16 May 2000, Jan Brosius wrote: Ok I understand this isomorphism better. However this remark seems to be of no value to functional programmers. Why trying to mix terms( otr types) with relations ? What is a 'type' in your oppinion? Isn't a type a statement about pre- and post-conditions, i.e. a formula? /Lars L
Re: more detailed explanation about forall in Haskell
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-
Re: more detailed explanation about forall in Haskell
- Original Message - From: Lars Lundgren [EMAIL PROTECTED] Sent: Tuesday, May 16, 2000 1:54 PM Subject: Re: more detailed explanation about forall in Haskell On Tue, 16 May 2000, Jan Brosius wrote: Ok I understand this isomorphism better. However this remark seems to be of no value to functional programmers. Why trying to mix terms( otr types) with relations ? What is a 'type' in your oppinion? I look at it as a set (either a variable set or a specific set). E.g. I look at Bool as a specific set which itself contains values True , False that are not sets. Next I interpret something like f :: a - Int as a family (indexed by a) of functions of " set" a into set Int. I didn't come into problems by this interpretation after having read the Haskell's User Guide. Which is my only general source about Haskell. It is up to someone else to say if such an interpretation shall lead into misinterpretation. I think Haskell will not be attractive to mathematicians if types MUST be read as formula's . If that is the case I can only say that I find the term "functional programming" a bit strange. Isn't a type a statement about pre- and post-conditions, i.e. a formula? I can't answer this since I have never read the definition of a type in say typed lambda calculus. I have a book about logic that deals about plain lambda calculus and that deals about "restricted" typed lambda calculus (where a type is not considered as a formula). I never read the definition of Hindley-Milner types.And the only introduction about types were the general user's guides from Clean , SML , Ocaml and of Haskell. /Lars L
Re: more detailed explanation about forall in Haskell
although this argument originated from a discussion of rank-2 polymorphism in Haskell's type system, the part I am replying to addresses only first-order predicate logic (also called "predicate calculus"). Jan Brosius asserts Now forall s1. ( ST s1 T(s)) IMPLIES forall s . ( ST s T(s) ) Marcin replies 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. Jan's assertion and Marcin's counter-assertion are later repeated two more times in different words. I think Marcin's counterexample completely disproves Jan's assertion. I am adding my thoughts to the discussion simply to argue for Marcin's conclusion using different (and more numerous) words and concepts. it might prove illustrative to quantify every variable in Jan's assertion. this means quantifying the single free occurence of s. there are two ways to do that, and I am tempted to say that this next way is the right way. forall s.((forall s1. ( ST s1 T(s))) implies forall s . ( ST s T(s) )) (redundant parentheses added for emphasis.) but to be perfectly intellectually honest, Jan wrote the formula, so Jan has a right to decide what it means. Jan could have meant this next. the only syntactic difference between that last formula and this next one is that the scope of the "forall s" that I added to Jan's assertion is limited to the left of the "implies". (forall s,s1.( ST s1 T(s))) implies forall s . ( ST s T(s) ) the latter has the considerable advantage of being true whereas the former is false. however, the true one is less useful in establishing conclusions than the false one. if we have already proved (forall s1. ( ST s1 T(foo))) for some concrete thing "foo", then the false formula allows us immediately to conclude forall s.(ST s T(s)). moreover, Jan wrote that "(forall y) ( forall x ) alpha(x,y) is equivalent with alpha(x,y)". I am tempted to say that that is just wrong, but rather I ask Jan: do you think that the two formulae, which I call the false one and the true one, are equivalent? btw, the natural-deduction style of proof is a lot more useful than that Bourbaki stuff for understanding this dispute. eg, here is a proof in the natural-deduction style of the "true formula". step 1. suppose (forall s,s1.( ST s1 T(s))). step 2. consider an arbitrary thing, foo. step 3. by instatiation of the s in step 1, (forall s1.(ST s1 T(foo))). step 4. by instatiation of the s1 in step 3, (ST foo T(foo)). step 5. summarizing steps 2-4, (forall s.(ST s T(s. step 6. summarizing steps 1-5, (forall s,s1.( ST s1 T(s))) implies forall s . ( ST s T(s) ) here is an invalid proof of the false formula. step 3 is invalid because to replace an old quantified variable with a new one is only valid if the new variable does not occur free in the old variable's scope. this error is called "variable capture". step 1. consider an arbitrary thing. call it s this time instead of foo. step 2. suppose (forall s1.(ST s1 T(s))) step 3. change the quantified variable from s1 to s, yielding (forall s. (ST s T(s))). step 4. summarizing steps 2-3, (forall s1.(ST s1 T(s))) implies forall s . ( ST s T(s) ) step 5. summarizing steps 1-4, forall s.((forall s1. ( ST s1 T(s))) implies forall s . ( ST s T(s) )) this has been a very tedious post. if you've read this far I would love to know which if any of the "proof assistants" you reccommend that can be used to let the machine perform the checking of "trivial but tedious" proofs like those last 2.
Re: more detailed explanation about forall in Haskell
Tue, 16 May 2000 22:37:45 +0200, Jan Brosius [EMAIL PROTECTED] pisze:
newSTRef applied to some value can have a type ST s (STRef s T(s)),
That is strange , can you give a little example?
I've given it four mail pairs ago, but here it is again:
refRef :: ST s Int
refRef = do
v1 - newSTRef 0
v2 - newSTRef v1 -- Here!
v1' - readSTRef v2
readSTRef v1'
(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 see nothing that could be described as 2 sorts of type variables.
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.
Of course it does not compile in Haskell. This was to show that your
checking "whether something is a type variable" is meaningless: here
a type is a type variable as far as I can tell, but runST requires
some different condition.
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 .
It is not - and that's why in Haskell 98 you cannot write the
type signature of "f" inside the definition of "f1". If you write
"f:: a - a", it means "f :: forall a. a - a", but "f" has a
different type.
In GHC you can write the type of "f", provided that you have given a
name to the type variable in question, using a pattern type signature
or result type signature (the latter not working yet).
Third If I would give any meaning to forall a. a- a then I
would give it the same meaning as a - a .
Wrong. The first is the type of a function that is polymorphic:
works for any argument type and gives a result of the same type
(there exist only three function of that type in Haskell 98:
bottom, function that always returns bottom, and identity).
The second is the type of a function from "a" to "a". Depending on what
"a" is, it can mean different things. For example if "a" is bound at
some outer function definition, it is the function from the whatever
type the outer function has been instantiated to, to the same type.
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]
How can you propose a better type of runST if you don't understand
such basic things?!
To use f1, you choose a type for "a", pass a function of the type
"a - a" and get a function [Int] - [Int]. For example you can
pass not (of type Bool-Bool) to f1.
To use f1', you must pass a polymorphic function of the type
"forall a. a - a" to it, and get a function [Int] - [Int].
You have only three choices for the first function.
To implement f1, you must be prepared for any type for "a" a caller has
chosen. It is hard to use the first argument in an interesting way,
because you have no values of type "a" other than bottom, and there
is little to do with a value of type "a" you get from the function,
because you don't know what "a" will be.
To implement f1', you know that the function is polymorphic, and you
can use it on any type you wish. For example apply it to each element
of the list and then to the list itself.
--
__("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-
Re: more detailed explanation about forall in Haskell
- Original Message - From: Marcin 'Qrczak' Kowalczyk [EMAIL PROTECTED] Sent: Tuesday, May 16, 2000 11:40 PM Subject: Re: more detailed explanation about forall in Haskell Tue, 16 May 2000 22:37:45 +0200, Jan Brosius [EMAIL PROTECTED] pisze: newSTRef applied to some value can have a type ST s (STRef s T(s)), That is strange , can you give a little example? I've given it four mail pairs ago, but here it is again: refRef :: ST s Int refRef = do v1 - newSTRef 0 I have not the do notation definition in front of me, so I guess (I am lazy): type of v1 is ST s (STRef s Int) ? (or STRef s Int ?) v2 - newSTRef v1 -- Here! Ok, type of v2 is ST s1 [STRef s1 (ST s (STRef s Int)] ? (or STRef s1 [STRef s Int] ?) which is of the form ST s1 (STRef s1 T(s)) with the additional condition given to the type checker that s1 =/ s and will always be considered as different i.e. s1 =/ s This shows that the additional comments given by me for the signature of newSTRef are not redundant. v1' - readSTRef v2 readSTRef v1' (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 see nothing that could be described as 2 sorts of type variables. Sorry, what were you then talking about in the former email?? 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. Of course it does not compile in Haskell. This was to show that your Why then did you say it compiled? checking "whether something is a type variable" is meaningless: here a type is a type variable as far as I can tell, but runST requires some different condition. NO. As I said allready before the socalled "my" runST is nothing else but a better documented runST. The Terms Variable(s) and Free(a) are not implemented (yet) This is for the implementor to do ,if he wants. If these "terms" could be implemented that could allow a richer set of functions then one can have today. 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 . It is not - and that's why in Haskell 98 you cannot write the type signature of "f" inside the definition of "f1". If you write "f:: a - a", it means "f :: forall a. a - a", but "f" has a different type. In GHC you can write the type of "f", provided that you have given a name to the type variable in question, using a pattern type signature or result type signature (the latter not working yet). Third If I would give any meaning to forall a. a- a then I would give it the same meaning as a - a . Wrong. The first is the type of a function that is polymorphic: works for any argument type and gives a result of the same type (there exist only three function of that type in Haskell 98: bottom, function that always returns bottom, and identity). The second is the type of a function from "a" to "a". Depending on what "a" is, it can mean different things. For example if "a" is bound at some outer function definition, it is the function from the whatever type the outer function has been instantiated to, to the same type. 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] How can you propose a better type of runST if you don't understand such basic things?! I don't understand illogical things. You on the contrary made mistake after mistake with your so called counterexample. Moreover you said your runST' did compile and now you say your runST' does not compile. Next time please don't lie. Try to be as clear as possible. Because I don't use forall in a bad and meaningless manner. You do ,perhaps Haskell 2 does, when it is not necessary. a - a should mean an endomorphism e.g. id etc.or something like f :: Int - Int f x = x^2 + x + 1 is an instance of an endomorphism a - a forall a. a - a should mean the same thing but clearly it does not in Haskell 2 . Please people, do not accept this in Haskell 2 ? I am almost sure there is no need for it. To use f1, you choose a type for "a", pass a function of the type "a - a" and get a function [Int] - [Int]. For example you can pass not (of type Bool-Bool) to f1. Yes, and inid . f (where f is as above f x = x^2 + x + 1 and where id x = x ) you cannot pass type Bool - Bool to id . Very Friendly Jan Brosius Very primitive explanation to defend the writings a - a and forall a. a - a as different . If Haskell 2 interprets a - a as ea GENERAL endomorphism ther is no problem at all.
Re: more detailed explanation about forall in Haskell
Claus Reinke writes: [nice exposition of C-H correspondence state threads] The main caveat is the insistence on constructive proofs (in the classical logic most of us tend to learn, there is this favourite proof technique: if I assume that xs don't exist, I am led to a contradiction, so xs have to exist, even if I haven't seen any of them yet - this is not acceptable in constructive logics). [haven't read the papers on a correspondence for classical logic yet, but I assume they exist, for otherwise I would contradict Frank Atanassow ;-] Here's a nice example, which you alluded to. Reading | as `or' and ~ as `not', a|~a is a theorem of classical logic but not intuitionistic logic. By definition, ~a = a-_|_ (falsum). A proof of this proposition is given by the term /\ a - \\(m::a|n::a-Void) - [n] (\x - [m] x)-- /\ is big-lambda "[m] t" and "\\m::a - t" are new term forms. They throw and catch continuations, where a continuation accepting values of type a is something of type a - Void. Void is the empty type, so this means that a continuation is a something like a function which never returns. "[m] t" takes a term t :: a, and yields a term of type Void with a fresh free variable m :: a-Void. You can think of [m] t as meaning, "throw value t at continuation m". When this gets reduced, the current context is discarded and execution proceeds from m, with t as input. "\\" is usually written with Greek letter `mu'. In "\\m::a - t", the term t must be of type Void and possess a free variable m :: a-Void; the result is a term of type a, in which m is now bound. You can think of "\\m::a - t" as meaning, "catch a value v thrown to continuation m and return v as the result". Note that since t has type Void, it must always throw something and can never return normally. (In case of conflicts, which value gets caught depends of course on the reduction order.) "\\(m::a|n::b) - t" is a pattern-matching variation on the mu-binder. t is again of type Void, but the result is of type a|b. The meaning is that it catches values thrown to either continuation, injects it into the sum, and then returns it. (There is also variant "[m|n] t" of the "[m] t" syntax, but we don't need it.) So what does our term /\a - \\(m::a|n::a-Void) - [n] (\x - [m] x) mean? Well, when it gets reduced, it remembers its calling context and associates it with m and n. Then it initially returns (by throwing it at n) to that context the closure (\x-[m]x)::a-Void which gets injected into the right summand. Execution proceeds, and if at any point this closure ever gets applied to some value v, then the original context is magically restored, but this time with v injected into the left summand. So this is an example of the time-travelling effect you get with multiply-invoked continuations (because we can consider that there is only one continuation of type a|a-Void.) Incidentally, the reason you need a special form for continuation "application" is that I glossed over a technical detail concerning whether to take ~a or a-Void as primitive. At least in the lambda-mu calculus, you're not allowed, actually, to write "f x" if f::A-Void for any A; you have to use "[f] x". I forget the details. -- Frank Atanassow, Dept. of Computer Science, Utrecht University Padualaan 14, PO Box 80.089, 3508 TB Utrecht, Netherlands Tel +31 (030) 253-1012, Fax +31 (030) 251-3791
Re: more detailed explanation about forall in Haskell
Fri, 12 May 2000 00:42:52 +0200, Jan Brosius [EMAIL PROTECTED] pisze:
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
...for "s" and "a" coming from the instantiation of a polymorphic
function "f". Yes.
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))
where "s1" is free (thus can be later generalized over) and "s" and
"a" come from the environment inside "f" (thus are monomorphic).
It would have the type you wrote if "v" was created in this thread.
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 see no "forall s" in the left type.
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':: ST s Int - Int
runST' x = ...
Inside the body of runST' "x" has the type "ST s Int", with "s"
taken from the environment.
When runST' will be later applied to a value of the type "ST s Int"
with "s" free, "x" will have the type "ST s Int" with nothing more
known about "s". (If runST was applied to this value directly, it
would be OK.)
When runST' will be applied to a value of the type "ST RealWorld Int",
"x" will have the type "ST RealWorld Int".
But you have to compile runST' _now_, and decide whether the first
argument of ST from the type of "x" is a type variable.
Haskell does not have this problem. It does not ever check if a type
is a type variable, but if it is a _free_ type variable, i.e. one
that can be generalized over.
runST':: forall s. ST s Int - Int
runST' x = runST x
Should it compile with your type of runST?
function runST are fullfilled . So ("my") runST will work.
Now I write
len :: Int
len = runST' (liftM length (readFile "foo") :: ST RealWorld Int)
which creates a global value of type Int which changes in time. Oops!
--
__("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-
Re: more detailed explanation about forall in Haskell
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 ifforall x,y alpha(x,y) is truethen 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
Re: more detailed explanation about forall in Haskell
On Thu, 11 May 2000, Jan Brosius wrote: Marcin Kowalczyk wrote at Wed, May 10, 2000 7:54 PM : Types can be treated as logical formulas, according to the Curry-Howard isomorphism. Sorry, never heard of in logic. But perhaps you can explain. M H Sørensen and P Urzyczyn. Lectures on the Curry-Howard Isomorphism. Available as DIKU Rapport 98/14, 1998. Keywords: The Curry-Howard isomorphism, Logic, Lambda-Calculus http://www.diku.dk/research-groups/topps/bibliography/1998.html#D-368 /Lars L
Re: more detailed explanation about forall in Haskell
Thorsten Altenkirch writes: Jan Brosius writes: Marcin Kowalczyk wrote at Wed, May 10, 2000 7:54 PM : 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 hope it is ok if I reply, although I am sure Marcin can defend himself just as well] Maybe because you have only learnt about classical logic, which is a shame especially for a computer scientist. Have a look at a standard text book, like Troestra van Dalen's "Intuitionism I,II". BTW there is a C-H correspondence for classical logic too, although it requires a constructive presentation of the rules and considerable care with reduction laws. The trick is to model the type of a continuation as a negated proposition, with reductio ad absurdum as a call/cc-like operation. See for example: C.-H. L. Ong, A semantic view of classical proofs: type-theoretic, categorical, denotational characterizations. In Proceedings of 11th IEEE Annual Symposium on Logic in Computer Science, IEEE Computer Society Press, pp. 230-241, 1996. -- Frank Atanassow, Dept. of Computer Science, Utrecht University Padualaan 14, PO Box 80.089, 3508 TB Utrecht, Netherlands Tel +31 (030) 253-1012, Fax +31 (030) 251-3791
Re: more detailed explanation about forall in Haskell
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-
Re: more detailed explanation about forall in Haskell
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
