Re: aide SVP
I guess he is asking how to define a modifiable list in Haskell. I leave the answer to the experts. AFAIK updating in place can only be done with the (ST s) monad. Scott - Original Message - From: fouad ktiri [EMAIL PROTECTED] To: [EMAIL PROTECTED] Sent: Friday, August 30, 2002 2:03 PM Subject: aide SVP Bonjour, Comment faire pour stocker des données dans une liste comme en programmation normale (x=x+1) Merci beaucoup __ Boîte aux lettres - Caramail - http://www.caramail.com ___ Haskell-Cafe mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell-cafe
Fw: Fatima 10
- Original Message - From: Marita Wojdak [EMAIL PROTECTED] To: 1MargieD [EMAIL PROTECTED] Sent: donderdag 1 juni 2000 16:58 Subject: Fw: Fatima 10 God love you, Marita Helpers of Our Lady Queen of Peace http://web.frontier.net/cgallagher - Original Message - From: DougMarianne Moore [EMAIL PROTECTED] To: [EMAIL PROTECTED]; [EMAIL PROTECTED]; [EMAIL PROTECTED]; [EMAIL PROTECTED]; [EMAIL PROTECTED]; [EMAIL PROTECTED]; [EMAIL PROTECTED]; [EMAIL PROTECTED]; [EMAIL PROTECTED]; [EMAIL PROTECTED]; [EMAIL PROTECTED]; [EMAIL PROTECTED]; [EMAIL PROTECTED]; [EMAIL PROTECTED]; [EMAIL PROTECTED]; [EMAIL PROTECTED]; [EMAIL PROTECTED]; [EMAIL PROTECTED]; [EMAIL PROTECTED]; [EMAIL PROTECTED]; [EMAIL PROTECTED]; [EMAIL PROTECTED]; [EMAIL PROTECTED]; [EMAIL PROTECTED]; [EMAIL PROTECTED]; [EMAIL PROTECTED]; [EMAIL PROTECTED]; [EMAIL PROTECTED]; [EMAIL PROTECTED]; [EMAIL PROTECTED]; [EMAIL PROTECTED]; [EMAIL PROTECTED]; [EMAIL PROTECTED]; [EMAIL PROTECTED]; [EMAIL PROTECTED]; vgalleg Sent: Thursday, June 01, 2000 1:03 AM Subject: Fatima 10 Jacinta's Visions Of The Holy Father One day we spent our siesta down by my parents' well. Jacinta sat on the stone slabs on top of the well. Francisco and I climbed up a steep bank in search of wild honey among the brambles in a nearby thicket. After a little while, Jacinta called out to me: "Didn't you see the Holy Father?" "No". "I don't know how it was, but I saw the Holy Father in a very big house, kneeling by a table, with his head buried in his hands, and he was weeping. Outside the house, there were many people. Some of them were throwing stones, others were cursing him and using bad language. Poor Holy Father, we must pray very much for him." I have already told you, how one day two priests recommended us to pray for the Holy Father, and explained to us who the Pope was. Afterwards Jacinta asked me: "Is he the one I saw weeping, the one Our Lady told us about in the secret?" "Yes, he is", I answered. "The Lady must have shown him also to those priests. You see, I was not mistaken. We need to pray a lot for him". At another time, we went to the cave called Lapa Cabeco. As soon as we got there, we prostrated on the ground, saying the prayers the Angel had taught us. After sometime, Jacinta stood up and called to me: "Can't you see all those highways and roads and fields full of people, who are crying with hunger and have nothing to eat? And the Holy Father in a church praying before the Immaculate Heart of Mary? And so many people praying with him?" Some days later, she asked me: "Can I say that I saw the Holy Father and all those people?" "No! Don't you see that that's part of the secret? If you do they'll find out straight away." "All right! Then I'll say nothing at all." Visions of War One day, I went to Jacinta's house to spend a little while with her. I found her sitting on her bed, deep in thought. "Jacinta, what are you thinking about?" "About the war that is coming. So many people are going to die, and almost all of them are going to hell! Many homes will be destroyed and many priests will be killed. Look I am going to Heaven, and as for you, when you see the light which the Lady told us would come one night before the war, you run up there too." "Don't you see that nobody can just run up to Heaven!" "That's true, you cannot! But don't be afraid! In Heaven I will be praying hard for you, for the Holy Father, for Portugal, so that the war will not come here, and for all the priests." Your Excellency is not aware that a few years ago, God manifested that sign, which astronomers chose to call an aurora borealis. I don't know for certain, but I think if they investigated the matter, they would discover that, in the form in which it appeared, it could not possibly had been an aurora borealis. Be that as it may, God made use of this to make me understand that His justice was about to strike the guilty nations. For this reason, I began to plead insistently for the Communion of Reparation on the First Saturdays, and the consecration of Russia. My intention was to obtain mercy and pardon, not only for the whole world but for Europe in particular. When God, in His infinite mercy, made me feel that the terrible moment was drawing near, Your Excellency may recall how, whenever occasion offered, I took the opportunity of pointing out, I still say that the prayer and penance which have been done in Portugal, have not yet appeased the Divine Justice, for they have not been accompanied by either contrition or amendment. I hope that Jacinta is interceding for us in Heaven. As I said in the notes I sent about the book called Jacinta, she was most deeply impressed by some of the things revealed to us in the secret. Such was the case with the vision of hell and the ruin of so
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
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
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
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
Fw: Fw: more detailed explanation about forall in Haskell
- Original Message - From: Jan Brosius [EMAIL PROTECTED] To: Carl R. Witty [EMAIL PROTECTED] Sent: Thursday, May 18, 2000 12:06 PM Subject: Re: Fw: more detailed explanation about forall in Haskell Thanks Carl for letting me see an ugly error that I made . SHAME on me. the equivalence [forall x. alpha(x)] = alpha(x) is ONLY TRUE if alpha(x) is a TRUE formula. [forall x. alpha(x)] = alpha(x) is TRUE Let's see what happens when alpha(x) is FALSE for not all x and if one would accept that:alpha(x) = [forall x. alpha(x)] is TRUE. Since alpha(x) is FALSE there might still be a constant c such that alpha(c) is TRUE Then (Modus Ponens) alpha(c) = [forall x. alpha(x)] alpha(c) * forall x . alpha(x) is TRUE which is of course false this shows that the implication alpha(x) = [forall x. alpha(x)] is in general false (it is only true if alpha(x) is a true formula. Very friendly Jan Brosius .From: Carl R. Witty [EMAIL PROTECTED] To: Jan Brosius [EMAIL PROTECTED] Cc: [EMAIL PROTECTED] Sent: Wednesday, May 17, 2000 4:24 AM Subject: Re: Fw: more detailed explanation about forall in Haskell "Jan Brosius" [EMAIL PROTECTED] writes: SORRY, this is quite TRUE , in fact [forall x. alpha(x)] = alpha(x) 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. (Is there something wrong with the education of a computer scientist?) Jan, could you tell us whether you think the following statements are true or false? Let prime(x) mean "x is a prime number". 1. [forall x. prime(x)] = prime(x) 2. forall x.([forall x. prime(x)] = prime(x)) 3. forall y.([forall x. prime(x)] = prime(y)) 4. [forall x. prime(x)] = prime(y) 5. [forall x. prime(x)] = prime(2) 6. [forall x. prime(x)] = prime(2) 7. prime(2) = [forall x. prime(x)] 8. prime(2) 9. [forall x. prime(x)] = prime(4) 10. [forall x. prime(x)] = prime(4) 11. prime(4) = [forall x. prime(x)] 12. prime(4) 13. forall x. prime(x) 14. prime(x) 15. Statement 1 above means the same thing as statement 2 above. 16. Statement 2 above means the same thing as statement 3 above. 17. Statement 3 above means the same thing as statement 4 above. 18. Statement 5 above is a substitution instance of statement 3; thus, if statement 3 were true, statement 5 would be true. 19. Statement 13 above means the same thing as statement 14 above. If we follow the convention that free variables are to be considered implicitly universally quantified, my vote is that statements 6, 8, 9, 10, 11, 15, 16, 17, 18, and 19 are true; the rest are false. Carl Witty
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
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, then (a proof exists that) b(-typed object)s exist forall a,b . a - b - b -- read: for all a and for all b, if as exist, then (a proof exists that) -- the existence of bs implies the existence of bs forall a,b . (a - b) - b -- read: for all a and for all b, if (a proof exists that) the existence of -- as implies the existence of bs, then bs exist forall b. (forall a. a - b) - b -- read: for all b, if (a proof exists that) for all a, the existence of as -- implies the existence of bs, then bs exist -- [note the limited scope of the inner forall] None of the statements that correspond to these types is true unless you can give concrete non-bottom elements of the types (empty types correspond to false propositions). So, "xs exist" should probably rather be "xs can be constructed". In all of these cases, the proofs would be functions, and the correspondence between types and propositions allows us to derive some properties that such functions must have (*). In the third case, the argument proof/function must not make any assumptions about as, because it has to work on all as (the proof has to be supplied before a specific a is given; the quantification over a is inside the parameter proof). In the second case, the proof can be given after both a and b have been given (the proof is inside of both quantifiers). It is this limitation of potential function definitions by their required type that is used in the context of runST. runST :: forall a. (forall s. ST s a) - a -- read: for all a, if (a proof exists that), -- for all s, objects of type ST s a exist, -- then objects of type a exist I think a functional programmer wouldn't like to read it as that, sorry. I just want to ask if this reflects completely the idea of runST as defined in Haskell? I can also say that there is an algebraic isomorphism from propositional calculus onto a boolean algebra. ARE we for this reason going to mix+ with or etc. e.g. a or b + c and d . f This doen't look as a good logic course to me. It only confuses. Very friendly Jan Brosius Again, there is a quantifier inside an inner proof/function. To construct an object of type a, runST (as a proof for the non-emptyness of its type) can make any assumption it needs about s, and so the inner proof can make no assumptions about s. It is not necessary for ST s a to be a function, but it should be a container, because the inner proof is runST's only source of as. To expand this a little, assume that ST s a was just a type of pairs, then noRunST st@(sv,av) = (fst.last) [(av,True,"or not"),(av,sv,sv)] would require that the type s of the value sv can be instantiated to both Bool and String, but would ignore sv and return av, justifying the type noRunST :: forall a. (forall s. (s,a)) - a noRunST is an overly lazy state transformer: as it ignores its state parameter, it would happily accept any non-constructive proof for the state component of the pair. But in a world without bottom (*), we have little chance of constructing the required proof parameter ourselves, and we have to use the primitives supplied for the ST monad - they thread the state along, making sure that only one state type is used in all operations of a given sequence, without making any further assumptions about what that type may be. A primitive operation doSomeThing :: forall s,a. ST s a is a proof that objects of the required type exist, which we can feed into runST, but what about operations such as get :: forall s. ST s (T s) -- where T is some type constructor, -- but not a type synonym that ignores s Doesn't this allow the "hidden" state type to escape? Well, no: the requirement in runST is that the proof parameter cannot make any assumptions about s. In particular, we cannot assume that there is any relation between s and a (as get does) in runST :: forall a. (forall s. ST s a) - a So, this is why an "internal" use of the state type is okay (has a type) runST (get return ()) :: () whereas an escaping reference to the "hidden" state type runST get :: ??? is not okay (does not have a type in this system). [I thought this was discussed extensively in the "State in Haskell"-paper, but found, to my surprise, that the explanation was intermingled with problem descriptions and details about the type checking process..] and what I was saying (UP TO NOW NOBODY could show where I was wrong) is the following: Hi, folks you can forget everything about this second order quantification, the usual forall does all . You might want to have a look at Mark Jones' paper on "First-class Polymorphism with Type Inference" (which should be available via his home page, http://www.cse.ogi.edu/~
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
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
- 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.
Fw: more detailed explanation about forall in Haskell
- Original Message - From: Jan Brosius [EMAIL PROTECTED] To: Richard Uhtenwoldt [EMAIL PROTECTED] Sent: Wednesday, May 17, 2000 1:23 AM Subject: Re: more detailed explanation about forall in Haskell - Original Message - From: Richard Uhtenwoldt [EMAIL PROTECTED] To: Jan Brosius [EMAIL PROTECTED] Cc: [EMAIL PROTECTED] Sent: Tuesday, May 16, 2000 11:06 PM Subject: 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. Now I understand what Marcin meant with this "counterexample". I admit I was very puzzled to find out where these formulas came from. It's a pity that I didn't saw it in a previous email. I guess Marcin meant with first term: forall s1. ST s1 T(s) == forall s1. s1^2 T(s) == forall s1. s1^2 s + 1 As everybody can notice the first term is FALSE . Indeed let s1 = 1 and s =1 and we get a false assertion. (the assertion 1^2 20 However [forall s1. ST s1 T(s) ] = [ forall s. ST s T(s)] is always TRUE. Since EX FALSO QUODLIBET ( a false assertion implies everything) if we would say [ forall s1. ST s1 T(s) ] = [ forall s . ST s T(s)] ( remember always ) TRUE forall s1. ST s1 T(s) (FALSE) *** forall s . ST s T(s) == forall s . s^2 s + 1 (TRUE or FALSE) ( here FALSE) The above rule is called a syllogism Marcin departed in his reasoning allready with a false assertion. The error he committed was to say that the first term was true for the case s = -2 . Here it is clear what confusion computer scientists might experience if they lose the real meaning of a variable. Indeed if I would put s =3 then everybody sees that one gets a FALSE assertion forall s1. s1^2 4 (false for s1 = 1) So Marcin's statement that he gave a counterexample was FALSE. (Sometimes one needs to reread something several days later in order to see what was meant by somebodyelse) 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. Well Marcin's counterexample is FALSE ( see above) I am adding my thoughts to the discussion simply to argue for Marcin's conclusion using different (and more numerous) words and concepts. too numerous and thus too dangerous. 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) )) WARNING : The notation forall s1 , s . alpha(s1, s) is since unbounded forall's commute simply an abbreviation for either forall s1. forall s . alpha(s1,s) or forall s. forall s1 . alpha(s1,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) ) yes using braces is better if there is risk of confusion the latter has the considerable advantage of being true whereas the former is false. If you mean by the former : [forall s1. ST s1 T(s) ] = [forall s. ST s T(s)] then I must say that on the contrary this is TRUE REMEMBER : [ forall s1. ST s1 T(s)] is EQUIVALENT to [forall s1, s . ST s1 T(s)] These are the formall rules of forall (even not using Bourbaki's logic) 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) ( foral
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 compile
Fw: more detailed explanation about forall in Haskell
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". Sorry, but I cannot study all sorts of logic that circulate around. I don't know what a computer scientist is supposed to know. I follow Bourbaki's logic where there is no need for an axiom of choice . However the so called axiom of choice is there a theorem that is one proves that the Cartesian product of a non empty family of non empty sets is in fact non empty. What about me : I have done theoretical physics and mathematics. I have embraced formal logic ,and the whole of math can be build on it. Formal logic is not sentimental. 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 " Then the Haskell language didn't state it. Sorry, a tuple is a tuple and nothing else, what you tell me is that the notation of tuple can be used as logical AND for propositions. A proof of a \/ b is a proof of a or a proof of b, hence a /\ b = Either a b You mean a V b = Either a b ? I guess you mean with a V b the logical or? A proof of a - b is a method to calculate a proof of b from a proof Here you use the sign - (function ) for the sign = (implies) of a hence a - b = a - b In formal logic we say just this a (true) a = b (true ) * b (true) There is no proof of False, hence one would identify False with the empty type, but as far as I know there is no empty type in Haskell? 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 (a + b) . c = a . c + b . c (distributivity) AND (a.b) + c = (a+c).(b+c) The disputed forall is just the (2nd order) quantification over all propositions. RunST is not the only disputed thing . newSTRef is also disputed. and what I was saying (UP TO NOW NOBODY could show where I was wrong) is the following: Hi, folks you can forget everything about this second order quantification, the usual forall does all . What I want to say is this : put forall s. ST s a in a logical phrase . This is an invitation. By the way I am trying to forward my comments to the Haskell committee. How can I reach them? It is a pleasure to know that somebody else than Marcin is also reading , because the discussion is reaching the point where it will be yes against no . Please people don't come with books nor with names to strengthen claims. Talk logically about it , try to define very clearly what you mean. 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 Seems more an issue of explanation?! Sorry , I don't understand . In a logical language there are RELATIONS (formula's if you want) and TERMS (types if you want) and these 2 are distinct and shall ever be distinct. But if I can learn something new , why not ? e.g. (a,b) is a tuple , a special TERM and no RELATION . But you and the Haskell committee are free to INTERPRET this as a AND b , but in that latter case a and b denote RELATIONS . In the former case a and b denote TERMS Cheers, Thorsten May I forward this mail to the Haskell - mailing list? I saw that your email allready found his way to the Haskell-list Very friendly Jan Brosius
reaching Haskell committee
Hi, is there any way to email written stuff to the Haskell committee? Very Friendly Jan Brosius
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 jo
more detailed explanation about forall in Haskell
to be known that ST s a is in reality implemented as a function.). There are 2 ways to circumvent this problem. c1. Use a new free variable binder ,e.g. `b ,for types to mean the following: `b s. ST s a is the type of ALL ST s a with the EXCEPTION of all types of the form ST s T(s) and then give runST the type signature runST :: forall a. (`b s . ST s a) - a c2. Use the following type signature for runST runST :: forall a. [forall s ni Free( a ) . ST s a - a] If we are supposed to know that IO a = ST World a then use the signature runST :: forall a. [forall Variable ( s ) ni Free ( a ) . ST s a - a ] where Variable (s) means " s is a type variable". Since Variable (World) is not true , the above type signature will not allow that runST accepts types of the form IO a as argument. 4. If it were possible to interrogate the typechecker in the following way : typeOf (x) = typeOf (y) then it would be possible to give a direct definition of runST. 5. Using `b as defined above we could give now the following type signature for newSTRef newSTRef :: forall a . a - (`b s. ST s (STRef s a)) Here `b s. ST s (STRef s a) will mean the type of ALL ST s (STRef s a) with the EXCEPTION of any type of the form ST s (STRef s T(s)) As we can see `b appears as a type restrictor. Thanks for reading , sorry for the typo's. Very Friendly, Jan Brosius PS: I have the impression that no notice is taken of the remarks given in my first email. I hope the Haskell committee will take notice of these remarks after reading these more detailed explanation. It is a bit sad that I cannot send a pdf form as an attachment . This would allow better reading and better checking for typo's .
Re: discussing basAlgPropos
I also support the idea's , and It doesn't chande the language it only structures it, but I am a lightweight in Haskellland. Sometimes I wonder if the readers are overworked or just plainly arrogant. Friendly Jan Brosius - Original Message - From: Jan Skibinski [EMAIL PROTECTED] To: S.D.Mechveliani [EMAIL PROTECTED] Cc: [EMAIL PROTECTED] Sent: Tuesday, May 02, 2000 2:31 PM Subject: Re: discussing basAlgPropos Sergey: I will only make a short observation here - skipping other unnecessary details which do not move this discussion in right direction. You misread me, I wanted to help. Specifically, I sensed a tone of resignation in your letter dated Wed, 26 Apr, 2000 in reponse to Fergus: Fergus: I think the "jury" is unlikely to rewrite the proposal; Fergus: more likely, they will simply reject the proposal. Fergus: It is up to the proponent(s) of the proposal to rewrite it. Sergey:I have no idea of how such committee may appear. Sergey:Neither do I care much of what with this proposal will happen. If you are satisfied with a current process, I rest my case. Friendly, Jan P.S. I read your proposal. I saw your comments within it. I could even extract some sort of a small and a big picture. But this is not good enough to attract general attention and to make it easy to discuss about. The onus is still on you, to be frank.
Re: About the abuse of forall in Haskell
- Original Message -
From: Jan Brosius [EMAIL PROTECTED]
To: Marcin 'Qrczak' Kowalczyk [EMAIL PROTECTED]
Cc: [EMAIL PROTECTED]
Sent: Wednesday, May 03, 2000 1:04 PM
Subject: Re: About the abuse of forall in Haskell
May 03, 2000 12:53 AM Marcin 'Qrczak' Kowalczyk wrote:
Tue, 2 May 2000 22:47:08 +0200, Jan Brosius [EMAIL PROTECTED]
pisze:
First I want to end this with the following observation : if the
forall in ( forall s1 . ST s1 T(s) ) really had the meaning
of the logical forall , that is if " forall s1 . ST s1 T(s)
is true then the case ST s T(s) i.e. the case for s1 = s is
also true.
Wrong implication. "forall s. ST s T(s)" is not an instance (result
of some variable substitution) of "forall s1. ST s1 T(s)". Variable
substitution is not a textual replacement, because variables are
lexically scoped - you cannot rebind a variable to a different
qualifier and say that it's the same thing.
"forall s1. ST s1 T(s)" does not imply "forall s. ST s T(s)".
So I looked to the example below:
forall x . x + a x is not true , however forall x. x + a = x is true,
Of course not . Let me correct myself
forall Positive ( x ) . x + a = a is true.
Friendly
Jan Brosius
of course as you say below if we talk about the wel known +.
Let's move to another domain. "forall x. x+a x" does not imply
"forall a. a+a a" when variables denote real numbers. For example
when "a" (bound somewhere outside) equals 1, then the first sentence
is true and the second is false.
As I said above , both sentences are false
It's the same with runST.
runST :: (forall s . ST s a ) - a
What sort of sentence could be meant by this?
I have the impression thatyou haven't read anything what I said before
Let's rewrite it by making foralls explicit:
runST :: forall a. (forall s. ST s a) - a
It means that ST is a function that can be instantiated for any "a",
you mean also for a = STRef s a
takes a value of type "ST s a" which can be instantiated for any "s",
so also for s =s
and returns a value of type "a".
and ... which delivers ST s STRef s a
I only followed what you sais before about any s and aboyt any a
I don't see any problem with this. There exists no type "a" for which
you could use runST to apply it to a value of type "forall s. ST s [s]".
If we accept this we can now give the following type signature for
runST
runST:: forall a . forall s ni FreeV( a ) . ST s a - a
If you mean parentheses put such:
runST :: forall a . forall s ni FreeV( a ) . (ST s a - a)
then this is wrong, because when we take a = Int and s = RealWorld,
runST could have the type ST RealWorld Int - Int, which must not be
possible, because a value of type "ST RealWorld Int" may describe
a computation that has I/O effects.
Let us polish it a bit more then (I couldn't find anymore a confirmation
in
the GHC/HUGS extension libraries
that IO a = ST RealWorld a )
runST :: forall a. forall Free( s ) ni FreeV ( a ) . ( ST s a - a)
If you mean parentheses put such:
runST:: forall a . (forall s ni FreeV( a ) . ST s a) - a
then it's exactly the same as currently. "forall s" introduces a
fresh type variable "s". It cannot be bound in some type outside
by definition.
I think I have allready answered above and in my email enough this
rewriting either is not necessary or it means
something differently.
--
__("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-
Thanks anyway for reading and commenting honestly
but the impression that the use of quantifiers is abusive in many ways is
only reinforced
Friendly
Jan Brosius
Re: your mail
Well it is a question that originated after studying the (mathematical)
strange typing for runST.
Besides runST I had no other specific problem in my mind and I thought if
it was possible to interrogate the typechecker to contol
(only in the compiler phase) the flow just as runST is in some sense doing.
But perhaps it is not possible in a statically typed language.
More about this will be clear in a forthcoming email that I am now preparing
titled "About the abuse of frall in Haskell"
Friendly
Jan Brosius
Tue, 2 May 2000 10:14:40 +0200, Jan Brosius [EMAIL PROTECTED] pisze:
Suppose in some function definition some variable is of type A s a and
I
want to do something like this : if the type variable of the first
parameter
in A s a
is s then do this if not then do something else.
This is what classes are for, even if not exactly in the way you mean.
This is a complex subject: they are powerful, but many things that
seem to be almost possible cannot be done with them, and there are
many extensions to Haskell related to classes.
Remember that there is no "else". Everything must be positive.
And it must fit into the statically typed world.
Tell us what the specific problem is. Maybe some completely different
approach would be reasonable for it.
--
__("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-
No Subject
Hi, Is it possible to interrogate the typechecker from within a Haskell program Friendly Jan Brosius
Fw: doubly linked list
Jerzy Karczmarczuk wrote: Yes, Simula-67. Actually *they did* that. A "node" had two sub-classes, the link and the head, and the link chain was doubly attached to the head. This structure has been havily used for the maintenance of the co-routine bedlam exploited in simulation programs. The idea of double lists was to permit a fast two-directional navigation, and the ease of insertion/deletion. But in Haskell, where the beasts are not mutable: ... Actually, has anybody really used them for practical purposes? Jerzy Karczmarczuk Caen, France Well I want to see the simulation of a mutable doubly linked list too. The author of Lout writes in his documentation that after much searching he was compelled to use doubly linked C lists. In Ocaml there was recently an online English version about using pointers in Ocaml (if people would like to do this) . I have got yesterday the solution of implementing doubly linked lists, it was rather short. I also wonder how one could simulate objects with mutable state in Haskell. Another question : is there any way to interrogate the typechecker from within a Haskell program? Could this be put on the wishlist? Friendly Jan Brosius
doubly linked list
Hi, I wonder if it is possible to simulate a doubly linked list in Haskell. Friendly Jan Brosius
Re: doubly linked list
- Original Message - From: Chris Okasaki [EMAIL PROTECTED] To: [EMAIL PROTECTED] Sent: Thursday, April 27, 2000 4:13 PM Subject: Re: doubly linked list I wonder if it is possible to simulate a doubly linked list in Haskell. Depends on what you mean. - Using mutable state in a monad you can implement a doubly linked list directly. please show me how to implement using mutable state in a monad Friendly Jan Brosius
a newbie's question about something related to runST
Hi, First I give the following primitive operations newVar :: a - ST s (MutVar s a) readVar :: MutVar s a - ST s a writeVar :: MutVar s a -a - ST s () Next consider the function f :: MutVar s a - Mut Var s a f v = runST (newVar v `thenST` \w - readVar w) 1. What is the type given to newVar v by the typechecker? Friendly Jan Brosius
Re: a newbie's question about something related to runST
On 26-Apr-2000, Jan Brosius [EMAIL PROTECTED] wrote: Hi, First I give the following primitive operations newVar :: a - ST s (MutVar s a) readVar :: MutVar s a - ST s a writeVar :: MutVar s a - a - ST s () Next consider the function f :: MutVar s a - Mut Var s a f v = runST (newVar v `thenST` \w - readVar w) 1. What is the type given to newVar v by the typechecker? Let's see... `v' has type `MutVar s a', and after renaming apart `newVar' has type `forall a2,s2 . a2 - ST s2 (MutVar s2 a2)', so, substituting `Mutvar s a' for `a2', we see that `newVar v' has type `forall s2 . ST s2 (MutVar s2 (MutVar s a))'. -- Ok, Next recall runST :: forall s. (ST s a) - a and let runST1 give the type signature runST1 :: ST s a - a consider v = runST1 ( newVar True) Then newVar True gets the type ST s (MutVar s a) ( I prefer the more sloppy notation without a forall as it gives less clutter). In runST1 :: ST s a - a Let us substitute a by say MutVar s a we then get after renaming the s in runST1 by s2 ST s2 ( MutVar s a ) - MutVar s a ) Have we finished ? One would say no : one needs a substitution for s2 , If we don't "cheat" we must now substitute s2 by s and we get ST s (MutVar s) - MutVar s a In principle this is not the type of runST. Because technically the "domain" of runST is of the form ST s a where a is never of the form T(s) Finally consider runST :: forall s . ( ST s a) - a What to do now ? let us first substitute a by MutVar s a as shown above. After renaming there remains forall s2 . ( ST s2 (MutVar s a)) - MutVar s a What is now the meaning of the forall s2 above? If it means that s2 can be substituted then we must substitute it by s But that is not what one wants : one wants s2 to remain non free. Where I wanted to come is this: give runST the type signature runST :: exists s . ( ST s a ) - a and technically we have also a bounded variable s. What is the reason for choosing forall against exists ? I think there is no reason for it. But I can be wrong. Friendly Jan Brosius
Human rights
Dear Friends, Please do not ignore this email. This is something that we ashuman beings need to support - I don't know if this is going to help but pleasetakeabout 3 minutes out of your life to do your part. Madhu, the government of Afghanistan, is waging a war upon women.Since theTaliban took power in 1996, women have had to wear burqua and havebeenbeaten and stoned in public for not having the proper attire, even ifthismeans simply not having the mesh covering in front of their eyes.One woman was beaten to death by an angry mob of fundamentalists foraccidentally exposing her arm while she was driving.Another was stoned to death for trying to leave the country with aman thatwas not a relative. Women are not allowed to work or even go out inpublicwithout a male relative; professional women such as professors,translators, doctors, lawyers, artists and writers have been forcedfromtheir jobs and stuffed into their homes. Homes where a woman ispresent must have their windows paintedso that she can never be seen by outsiders They must wear silentshoes so that they are never heard.Women live in fear of their lives for the slightest misbehavior. Because they cannot work,those without male relatives orhusbands are either starving to death or begging on the street, evenif they hold Ph.D.s. Depression is becoming so widespread that it has reachedemergency levels. There is no way insuch an extreme Islamic society to know the suicide rate withcertainty, but relief workers areestimating that the suicide rateamong women, who cannot find proper medication and treatment forsevere depression and would rather taketheir lives than live in such conditions, has increasedsignificantly.There are almost no medical facilities available for women. At oneof the rare hospitals for women, areporter found still, nearly lifeless bodies lying motionless on topof beds, wrapped in their burqua,unwilling to speak, eat, or do anything, but slowly wasting away.Others have gone mad and were seencrouched in corners, perpetually rocking or crying, most of them infear. One doctor is considering,when what little medication that is left finally runs out, leavingthese women in front of thepresident's residence as a form of protest. It is at the point wherethe term "humanrights violations" has become an understatement. Husbands have thepower of life and death over theirwomen relatives, especially their wives, but an angry mob has just asmuch right to stone or beat awoman, often to death,for exposing an inch of flesh or offending them in the slightest way. Women enjoyed relative freedom, to work, dress generally as theywanted, and drive and appear inpublic alone until 1996. The rapidity of this transition is the mainreason for the depression andsuicide; women who were once educators, doctors or simply used tobasic human freedoms, are now severelyrestricted and treated as subhuman in the name of right-wing fundamentalist Islam. It is not theirtradition or 'culture,'but it is alien tothem, and it is extreme even for those cultures where fundamentalismis the rule. Everyone has a rightto a tolerable human existence, even if they are women in a Muslimcountry. If we can threaten and carry out military force in Kosovo in thename of human rights for the sakeof ethnic Albanians, (also Muslims), citizens of the world cancertainly express peaceful outrage atthe oppression, murder and injustice committed against women by the Taliban. STATEMENT: In signing this, we agree that the current treatment of women inAfghanistan is completelyUNACCEPTABLE and deserves action by the United Nations and that thecurrent situation will not betolerated. Women's Rights is not a small issue anywhere, and it isfor women in 1999(2000) to be treated as subhuman and so much as property. Equality and human decency is a RIGHT not afreedom, whether one lives inAfghanistan orelsewhere.1. Barbara Jakschik, PHD, Rome, Italy 2. Carol L. Story, Buckhannon, West Virginia 3. James B. McCafferty, Buckhannon, West Virginia 4. Lynne Snyder, Belington, WV 5. Jan Brosius PhD, Rotselaar , BELGIUM PLEASE COPY this email on to a new message, sign the bottomand forward it to everyone on your distribution lists. If you receive thislist with morethan 300 names on it, please e-mail a copy of it to: mailto:[EMAIL PROTECTED][EMAIL PROTECTED]. Even ifyou decide not to sign, please beconsiderate and do not kill the petition. Thank you!
Re: .gz files
Thanks for this workaround, it worked. This might be a tip to be put on the mailing list, since other people using Windows NT and Winzip might have the same problem. Friendly Jan Brosius - Original Message - From: Simon Peyton-Jones [EMAIL PROTECTED] To: 'Jan Brosius' [EMAIL PROTECTED] Sent: Friday, March 31, 2000 1:58 PM Subject: RE: .gz files | However if you have no problems opening these files with | winzip, then I | don't know | anymore. I do have a problem. I download them. If winzip complains I remove the .gz suffix. Then ghostview reads them fine. I have no idea why they are invisibly uncompressed. I'm just telling you a workaround that works for me Simon
Some questions
Hi, Suppose a denotes a type variable. 1.Can I then say: Bool is of type a ? 2. I suppose I can say that True is of type Bool. However True is not itself a type, isn't it? I suppose that I cannot say that True is of type a, isn't it ? So True is a "value" but not a "type value" , isn't? 3. Now consider the type of state transformers ST s a : in the above s is a type variable that ranges over the values(?) of type State . Since IO a = ST RealWorld a , I deduce that RealWorld is not a type variable (because the first letter is a capital) but a very specific type : i.e. RealWorld is of type State and RealWorld itself contains values but not of type State ; shouldn't I then say that s ranges over "type values " of type state instead of "values" of type State. 4. Consider the type f :: a - b - c. Can I say that f is of type a - b since b is a more general type than the type b - c , and if this is true can I then say that f is also of type a? And if this is true I suppose that "being of type " is a transitive relation among types, isn't? Hoping to get comments Friendly Jan Brosius
Fw: Some questions
2. I would first like to come back to the type signature f :: a - b I can say the type of f is a - b , isn't it? Well, people often do say that, but it is a little sloppy; if you want to be precise, it is more correct to say that the type of `f' is `forall a,b . a - b'. But a and b are both variables. Question can I replace the General type b by the type c - d ? In general that transformation does not preserve type-correctness. Changing `b' to `c - d' in the type signature might change a type-correct program into an ill-typed one. For example, if the program contains foo :: Int - Int foo x = f x then changing the type signature of `f' to `f :: a - c - d' would mean that the previously type-correct call to `f' here would now become a type error. I would rather say that the programmer has not looked well at the definition of f; e.g. if f was defined as f :: a - a f x = x then foo :: Int - Int foo x = f x gives no problem and foo1 :: (Int - Int) - (Int - Int) foo1 x = f x shouldn't give a problem too, should it? It is clear that the type a - a is completely different from the type a - b : you can never go with substution from a - a to a - b but the reverse is possible. Also if f was defined as f :: a - b f x = x wouldn't the typechecker complain? Friendly Jan Brosius
a question about a paper
Hi, Hi, the paper is titled " lazy functional state-threads" . Under the topic "2.4 Encapsulation" consider the code let v = runst (newVar True) in runST (readVar v) Consider the last line ; if the type of readVar v is say " MutVar s Bool" then readVar v will have type "ST s Bool". the article sais " s is free " . So my question is why hasn't readVar v the type " forall s ( ST s Bool) " ? Thanks Jan Brosius
Fw: Fw: a problem concerning a paper
- Original Message -
From: Marcin 'Qrczak' Kowalczyk [EMAIL PROTECTED]
To: [EMAIL PROTECTED]
Sent: Monday, March 20, 2000 8:58 PM
Subject: Re: Fw: a problem concerning a paper
Mon, 20 Mar 2000 14:59:26 +0100, Jan Brosius
[EMAIL PROTECTED] pisze:
let v = runst (newVar True)
in
runST (readVar v)
Consider the last line ;
Consider the first line before, because it must be typed in order to
type the last line.
"newVar True" has type "ST s (MutVar s Bool)".
runST has type "(forall s. ST s a) - a".
The type of expected argument of runST cannot be matched with the
type of the actual argument. "ST s (MutVar s Bool)" is not of the
form "forall s. ST s a" for any type a, because the second argument
of ST depends on the first, yet "forall s. ST s a" says it does not
Yes , but what if I would say using your own explanation below that s is
not a variable anymore
but that it actually has a certain specific type say s0. In that case ...
but to keep this discussion
in sequence I first need to know if this is correct.
(a is bound somewhere outside).
So the first line won't typecheck, and the question whether the last
line would typecheck if the first line would becomes irrelevant.
I think it is relevant, for in the paper it is said that "s is free in ...
and so it doesn't match the type of runST ".
I beg to discuss this paper since it is the most recent explanation of the
implementation of runST
that I could download . If I can understand this paper I can understand the
rest too, I think.
Moreover it is important even for those who only uses Haskell98 since the
implementation
of IO a comes from ST RealWorld a .
Now, consider the following example:
runST $ do
v - newVar True
return (runST (readVar v))
Here the cause is different. The type of "readVar v" is "ST s Bool".
Which s? The s that comes from a lambda-bound variable v, because
readVar requires s from the monad and s from the variable to be the
same. The lambda is hidden inside the do notation:
runST $
newVar True = \v -
return (runST (readVar v))
"ST s Bool" with s taken from the environment does not match
"forall s. ST s a", because runST requires the s to be free.
So , I think you mean s is no longer a variable but has a certain type say
s0. Or am I wrong ?
But again please let us focus the discussion on the paper. Once I understand
this paper I can go on further.
BTW. In GHC and Hugs the names are actually STRef, newSTRef, readSTRef,
writeSTRef.
Please focus the discussion on the paper. ( By the way several (not all)
compressed archived papers
could not be opened by my Winzip program (I use Windows NT ))
--
__("Marcin Kowalczyk * [EMAIL PROTECTED] http://qrczak.ids.net.pl/
\__/ GCS/M d- s+:-- a22 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-
Fw: speed of compiled Haskell code.
- Original Message - From: Ketil Malde [EMAIL PROTECTED] To: Jan Brosius [EMAIL PROTECTED] Cc: [EMAIL PROTECTED]; S.D.Mechveliani [EMAIL PROTECTED] Sent: Tuesday, March 21, 2000 10:14 AM Subject: Re: speed of compiled Haskell code. "Jan Brosius" [EMAIL PROTECTED] writes: But this example task was chosen as unlucky for Haskell. In other, average case, I expect the ratio of 6-10. This seems that Haskell cannot be considered as a language for real world applications but merely as a toy for researchers . Yeah. Let's just lump Haskell in with Perl, Python, Java, Lisp and all those other toy languages, completely useless in the "real world". The only argument against Haskell's performance that IMHO carries any real weight, is that GHC is dog slow as a compiler[0]. No other Haskell programs I've used or written[1] have been slow enough for me NO, NO and NO , please read only what I have written. E.g. I believe that Ocaml is certainly not toy language, it gives as far as people have communicated to me fast compact native code. My question about the speed of Haskell is not meant to upset people. On the contrary Haskell does attract me by its elegance. I just wanted to know what to expect of the code produced. I thought some people could give me some honest answers about it. Recent (really recent ) benchmarks are not available ont the Haskell website as far as I know Friendly Jan Brosius (a lazy wanting to use Haskell ) to notice it. -kzm [0] almost as bad as Microsoft's C++ compiler, imagine that. [1] admittedly not many. Are people using Haskell having problems getting good enough performance? Enough to regret choosing it as a language? (This is not a rhetoric question!) -- If I haven't seen further, it is by standing in the footprints of giants
Re: HaskellDoc?
Frank Atanassow [EMAIL PROTECTED] wrote: Anyway, I don't think the choice of markup is all that crucial, but I think markup for documenting Haskell should also be as functional and elegant as possible. Is Lout a thing to consider? Yes, I think Lout is the best candidate Cheers Jan Brosius
Fw: a problem concerning a paper
Hi, the paper is titled " lazy functional state-threads" . Under the topic "2.4 Encapsulation" consider the code let v = runst (newVar True) in runST (readVar v) Consider the last line ; if the type of readVar v is say " MutVar s Bool" then readVar v will have type "ST s Bool". the article sais " s is free " . So my question is why hasn't readVar v the type " forall s ( ST s Bool) " ? Thanks Jan Brosius
Re: speed of compiled Haskell code.
Sergey Mechveliani [EMAIL PROTECTED] wrote: [..] E.g. if one uses GHC to compile Haskell code into native code what speed performance can be expected versus a same program written in C [..] My experience with the program of generating permutations on [1..10] showed that the code produced by ghc-4.04 is 22 times slower than certain specially written C program. Only the C program algorithm was taken very different from Haskell's one. For each system has its own best algorithm and appropriate data structure. But this example task was chosen as unlucky for Haskell. In other, average case, I expect the ratio of 6-10. This seems that Haskell cannot be considered as a language for real world applications but merely as a toy for researchers . Do Ocaml or MLTon (SML) beat Haskell by a factorof 3? See e.g. What is MLton's efficience versus C? Here are the times in seconds for a few small benchmarks on my 400 MhZ Pentium II. For benchmarks that use arrays, I have also included the time when compiling with the -unsafe flag, which turns off bounds checking. gcc -O2 mlton mlton -unsafe --- - - fft 18.69 31.66 28.69 fib 7.44 9.97 matrix mult 2.65 13.27 6.15 quicksort 17.69 27.80 20.94 tak 15.86 21.99 As you can see mlton -unsafe is within a factor of 2 on all the benchmarks except matrix multiply, which is 2.3 times slower. P.S. As I understand the CPS (continuation passing style ) used to implement SML/NJ will be abandoned as it did not produce small and fast standalone executables I don't think that CPS is entirely the cause of this. Although, I do believe that their use of the heap for allocating stack frames does slow them down. As to size, I think they just haven't gone to enough effort to clean up the exported heaps. Is MLton portable to other OSes? Yes, but it hasn't been done yet. Right now, there is a Windows port underway by [EMAIL PROTECTED], using a crosscompiler from Linux (http://www.devolution.com/~slouken/SDL/Xmingw32/). He just started, so I'm not sure how it will turn out. I am not aware of any other porting efforts. The current focus of our development efforts are improving the performance with an X86 native backend and adding functionality. ### But I am not so sure. It is easy to mistake with such comparison. Cheers Jan Brosius
RE: speed of compiled Haskell code.
Ok, So lazy Haskell (GHC 4.0...) is 10 times slower than a same program coded in C (let forget about Fortran). imperative functional programs like OCaml (or MLTon (SML 97) are 2.5 times slower than C , for any sort of program. Haskell code optimised by strictnes annotions in functions or in datastructures are ? times slower than C. Please correct me where I am wrong and fill in the required number for the ? sign above Friendly Jan Brosius
speed and size of compiled Haskell code
Hi, I wonder if someone could tell me more about the speed and size of compiled Haskell code. E.g. if one uses GHC to compile Haskell code into native code what speed performance can be expected versus a same program written in C (Hints about the nhc compiler are welcome). Is lazyness as good as strictness. What about Haskell 98 versus (I anticipate) Haskell 2 Thanks Jan Brosius
Re: records in Haskell
Does anyone know if this below situation is as bad in say SMLNJ or OCAML?
JanBrosius
- Original Message -
From: Jan Kort [EMAIL PROTECTED]
To: Simon Marlow [EMAIL PROTECTED]
Cc: [EMAIL PROTECTED]
Sent: Thursday, March 16, 2000 12:59 PM
Subject: Re: records in Haskell
Simon Marlow wrote:
Jan Kort writes:
It seem that any record, no matter how trivial, can't be much
longer than about 200 lines in Haskell. If a try to compile a
300 line record containing just:
data X = X {
f1 :: String,
f2 :: String,
f3 :: String,
...
f300 :: String
}
It needs about 90M heap in ghc4.06. Whereas a 150 line record
requires less than 6M heap. After this big gap it levels off
to a somewhat more decent exponential increase: a 450 line
record requires about 180M heap.
I could file a bug report, but it seems that all compilers
(ghc4.06, nhc98, hbc0.9994 and hugs) have this problem. So,
is this a fundamental problem ?
Actually, the 150-line record needs about 20M, and the 300-line record
needs
about 75M. These figures are roughly double the actual residency,
because
GHC's underlying collector is a copying, not compacting, one.
GHC automatically increases the heap size up to a maximum of 64M unless
you
tell it not to (with -optCrts-M32m, for example). I'll bet this is the
source of the confusion.
The heap requirement is still non-linear, but I'm guessing that this is
because for each line you add to the record the compiler has to not only
generate a new selector function, but also add a field to the record
being
pattern matched against in all the existing selectors.
Cheers,
Simon
Thanks for the answers and sorry for the late reaction.
I worked out an example to understand what you wrote.
GHC will probably generate something like this:
data R = R String Integer
deriving (Read,Show)
selectA (R s _) = s
selectB (R _ i) = i
updateA (R _ b) a = (R a b)
updateB (R a _) b = (R a b)
emptyR = R undefined undefined
Which you can then use like this:
updateR = updateB (updateA emptyR "a") 2
testA = selectA updateR
testB = selectB updateR
I agree that the select and update pattern matchings would
get big for a 300 line record, but 75M is a lot of memory.
Especialy because the pattern matches and the right hand
sides of both the selects and updates are trivial pieces
of code: no nesting, no currying etc. But maybe GHC
generates something extra ? Is special code generated
for updating multiple fields for example ?
I can probably work around this in a simple way: since I'm
generating the big record, I might as well generate
the selects, updates and emptyR instead and split them
over a couple of files.
Jan
comparison with the ML family
Hi, compared with Ocaml and SML , Haskell is a more sophisticated and more elegant language. Does anybody know how efficient the Haskell compiler is with regards to impure functional languages. Thanks Jan
Re: typing error?
Thanks to Amr A Sabry for showing the error in my reasoning and thanks to John Launchburry for clarifying the reason of this at first strange example. It helped me a lot about understanding better rank 2 polymorphism. Jan - Original Message - From: John Launchbury [EMAIL PROTECTED] To: Jan Brosius [EMAIL PROTECTED] Cc: [EMAIL PROTECTED] Sent: Monday, July 19, 1999 6:31 PM Subject: Re: typing error? Jan Brosius wrote: I have read the online postscript paper " Lazy Functional State Threads". I think the typing (page 4) f :: MutVar s a - Mutvar s a is wrong, since the definition of f is : f v = runST ( newVar v 'thenST' \w - readVar w) I think you mean page 10... The typing given for f is an instance of the more general typing you gave. The intent was to show that the s-types were not special in any way, and that state threads could manipulate state structures belonging to other threads. There are less contrived examples which are not mere instances of more general polytypes. John
No Subject
Hi, will Haskell compiled programs be faster by using more strictness annotations; I especially think of Clean where strictness annotations are "abundantly" used? Thanks Jan
typing error?
Hi, I have read the online postscript paper " Lazy Functional State Threads". I think the typing (page 4) f :: MutVar s a - Mutvar s a is wrong, since the definition of f is : f v = runST ( newVar v 'thenST' \w - readVar w) and since newVar is typed as: newVar :: a - ST s (MutVar s a) hence v is of type a. Furthermore runST has type runST :: (forall s. ST s a) - a hence f v can't have the type " MutVar s a ". If I understand well the definition of f v ,thenST and readVar (see above) , f v must have type a. Thanks for any comments. Jan
second rank polymorphism
Hi, Is there anyone who can explain to me what is meant by second rank polymorphism. I have already read all available online documentation. In logic one has: forall x forall y = forall y forall x. Doesn't haskell 98 allow in place updating e.g; for records? Thanks Jan
