[Haskell-cafe] Monaris
Happy new year from Japan. A young talented guy, @fumieval, has released Monaris, a Tetoris clone based on OpenGL. You can install it: % cabal install Monaris To my surprise, this game is implemented with free Monad. ;-) Regards, --Kazu ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Proving programs
Le Tue, 01 Jan 2013 14:24:04 -0900, Christopher Howard christopher.how...@frigidcode.com a écrit : I'm working through a video lecture describing how to prove programs correct, by first translating the program into a control flow representation and then using propositional logic. In the control flow section, the speaker described how the program should be understood in terms of an input vector (X, the inputs to the program), a program vector (Y, the storage variables), and an output vector (Z, the outputs of the program), with X mapping into Y, Y being affected by execution, and X and Y mapping into Z. However, only part way into the video, two practical questions come to mind: 1. Does this approach need to be adjusted for a functional language, in which computation is (at least idealistically) distinct from control flow? 2. How do we approach this for programs that have an input loop (or recursion)? E.g., I have an application that reads one line for stdin, modifies said line, outputs to stdout, and repeats this process until EOF? Should I be thinking of every iteration as a separate program? Have you heard of Agda and Curry-Howard? For imperative programs, you may also be interested in Hoare logic. There are also some tools you may be interested in: - Atelier B - Why3 And probably many others. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Object Oriented programming for Functional Programmers
On Jan 2, 2013, at 2:26 AM, Bob Hutchison hutch-li...@recursive.ca wrote: On 2013-01-01, at 3:47 PM, MigMit miguelim...@yandex.ru wrote: Well, probably one of the reasons is that I've learned Eiffel later than Haskell. But really, Design by Contract — a theory? It certainly is a useful approach, but it doesn't seem to be a theory, not until we can actually prove something about it, and Eiffel doesn't seem to offer anything in this direction. Don't confuse OOSC2 and Eiffel. Eiffel implements the ideas in OOSC2 as best as Meyer can, but they are not the same thing. Well, we were talking about Eiffel. OOSC2 deserves a few unkind words as well, but I won't go there. And, personally, I think I would be willing to call DbC a theory, or a close precursor to a theory. I don't know about DbC in general, but it's implementation in Eiffel seems to be nothing more than a few ASSERT macros, for some weird reason embedded into the language. So, I think, you're saying take away the contracts and the outcome of compilation won't be any different. Whereas take away the types and Haskell is stopped cold. And that difference makes contracts a 'hack' but types not a 'hack'? I wasn't clear enough, sorry. I'm sure it's due to sleep deprivation. Or coffee deprivation. See, there are two parts of Eiffel, as I see it. First one is the contracts part. Second is… well, everything else. Second part seems to be doing all the real job, while the first one is doing something invisible, something that leaves no trace in the final result. Which doesn't mean it's unimportant, of course. The contracts part is designed to help the other part do it's job, but not to do the job by itself. Now, there are two problems with that: 1) The real job part needs helping. And a lot of it, actually, one doesn't need to look very closely to see that Eiffel type system is extremely unsafe (for the statically type language). 2) The contracts part does a very poor job. Instead of really improving the inherent unsafety, it resorts to testing. And... 2') ...not even the real, thorough testing — contracts system would be quite happy if the program works on the developer's machine. Which is the works for me approach certain languages gets rightfully blamed for. Seems to me you're ignoring everything that happens between an empty directory and a working program. Contracts help in that process (I say but can't prove). I agree. They do help — but there are lots of things that help in this transition. Versioning systems. Collaboration tools. Bug tracking software. Text editors. Even debuggers. Pre and post conditions with class invariants are neither types nor unit test, something in between. With the wonderful properties of 'useful' and 'executable'. Sometimes you just have to settle for the hacks. Cheers, Bob On Jan 1, 2013, at 11:41 PM, Mike Meyer m...@mired.org wrote: MigMit miguelim...@yandex.ru wrote: On Jan 1, 2013, at 10:23 PM, Никитин Лев leon.v.niki...@pravmail.ru wrote: Eiffel, for my opinion, is a best OOP language. Meyer use a theoretical approach as it is possible in OOP. Really? Because when I studied it I had a very different impression: that behind this language there was no theory at all. And it's only feature I remember that is not present in mainstream languages is it's pre/postconditions system, which looked like an ugly hack for me. I agree with Leon. Of course, I learned it out of OOSC2, which provides the theory. When compared to mainstream OO languages like C++, Java or Python, it's on a much solider theoretical basis. Compared to something like Scheme, Haskell or even Clojure, maybe not so much. On the other hand, one persons theory is another persons hack. The theory behind the pre/post conditions is Design by Contract. The contracts are as important as the type signature, and show up in the auto-generated docs in eiffel systems. I found at least one attempt to add DbC features to Haskell. I'm not sold on it as a programming technique - the bugs it uncovers are as likely to be in the pre/post conditions as in the code. -- Sent from my Android tablet with K-9 Mail. Please excuse my swyping. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Object Oriented programming for Functional Programmers
On Jan 2, 2013, at 8:44 AM, Никитин Лев leon.v.niki...@pravmail.ru wrote: I said theoratical, but not mathematical or a scientific theory. Than what kind of theory did you mean? image1.gif Meyer have built a quite coherent construction in comparison with other OOP langs. More than Smalltalk, for example? BTW, when I started study haskell i had similar question: is it possible to add DbC to haskell? Does haskell need DbC? For example, class invariants may be expressed in DbC construction (fmap id = id for Functior, for example). 02.01.2013, 02:41, Mike Meyer m...@mired.org: MigMit miguelim...@yandex.ru wrote: On Jan 1, 2013, at 10:23 PM, Никитин Лев leon.v.niki...@pravmail.ru wrote: Eiffel, for my opinion, is a best OOP language. Meyer use a theoretical approach as it is possible in OOP. Really? Because when I studied it I had a very different impression: that behind this language there was no theory at all. And it's only feature I remember that is not present in mainstream languages is it's pre/postconditions system, which looked like an ugly hack for me. I agree with Leon. Of course, I learned it out of OOSC2, which provides the theory. When compared to mainstream OO languages like C++, Java or Python, it's on a much solider theoretical basis. Compared to something like Scheme, Haskell or even Clojure, maybe not so much. On the other hand, one persons theory is another persons hack. The theory behind the pre/post conditions is Design by Contract. The contracts are as important as the type signature, and show up in the auto-generated docs in eiffel systems. I found at least one attempt to add DbC features to Haskell. I'm not sold on it as a programming technique - the bugs it uncovers are as likely to be in the pre/post conditions as in the code. -- Sent from my Android tablet with K-9 Mail. Please excuse my swyping. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Object Oriented programming for Functional Programmers
On Jan 2, 2013, at 10:52 AM, Mike Meyer m...@mired.org wrote: [Context destroyed by top posting.] MigMit miguelim...@yandex.ru wrote: But really, Design by Contract — a theory? It certainly is a useful approach, but it doesn't seem to be a theory, not until we can actually prove something about it, and Eiffel doesn't seem to offer anything in this direction. You just stated (briefly, and not very rigorously) the theory: DbC is a useful approach to programing. Note that it's a theory about *programming*, not the resulting program. Well, you can call that a theory, for sure. But I think it's usually called an observation. I always thought the theory is something that allows us to develop some new knowledge. Just stating that comfortable chairs make programmers more productive doesn't constitute a theory. Type classes are the wrong feature to look at. Type signatures are closer to what DbC is. Are type signatures a hack to get around deficiencies in the type inferencing engine? After all, you can strip all of them away and have essentially the same program. I've tried to clarify my position in my response to Bob Hutchison. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Object Oriented programming for Functional Programmers
On Wed, 2 Jan 2013 13:48:07 +0400 MigMit miguelim...@yandex.ru wrote: On Jan 2, 2013, at 10:52 AM, Mike Meyer m...@mired.org wrote: MigMit miguelim...@yandex.ru wrote: But really, Design by Contract — a theory? It certainly is a useful approach, but it doesn't seem to be a theory, not until we can actually prove something about it, and Eiffel doesn't seem to offer anything in this direction. You just stated (briefly, and not very rigorously) the theory: DbC is a useful approach to programing. Note that it's a theory about *programming*, not the resulting program. Well, you can call that a theory, for sure. But I think it's usually called an observation. An observation is what you make to decide if a theory is true or not. In order to make the observation (at least for theories about helping programmers) you need an implementation so you can observe people using it. I always thought the theory is something that allows us to develop some new knowledge. Yup. Deciding whether or not the theory is true *is* a development of new knowledge. I can say for a certainty that the documentation aspect of DbC makes me more productive. The testing aspect of it needs more testing (sorry). Just stating that comfortable chairs make programmers more productive doesn't constitute a theory. Well, it's not very rigorous, and I can think of some counterexamples. On the other hand, if you reparaphrased (sic) it as Chairs that encourage good posture make programmers more productive, then you have a honest-to-goodness theory. Better yet, it's one that's been thoroughly tested in ergonomics labs around the world. At this point, we're arguing about the semantics of the word theory. On Wed, 2 Jan 2013 13:41:54 +0400 MigMit miguelim...@yandex.ru wrote: I don't know about DbC in general, but it's implementation in Eiffel seems to be nothing more than a few ASSERT macros, for some weird reason embedded into the language. Either you used a particularly poor implementation of Eiffel, or you didn't look at the implementation beyond writing them out. Every Eiffel system I've used included tools that computed the contracts on a method or class (remember, class invariants apply to subclasses, etc.) and displayed them. Those are just as much part of DbC as the assert macros. If you ignore that usage, you've correctly described things. At least as well as saying that a function call implementation is a goto that records a return address, for some weird reason embedded into the language. Or higher level construct is just implementation method, for some weird reason embedded into the language. The weird reason is pretty much always the same: the construct in question carries more semantic meaning than the implementation method. Functions capture the notion of a distinct, reusable chunk of code, that can have properties all it's own. This is a major step up from just having a goto variant with an otog that undoes it. Likewise, pre and post (and invariant) conditions capture the notion of a contract. They express the terms of the contract implemented by some specific bit of code. The contract is part of the interface to that code. If you're actually doing DbC, it's no less important than the rest of the interface. Like, for instance, the type signature. Personally, I don't believe in turning off the conditions, for much the same reason I don't believe in turning off array bounds checking. I think it's better to get the right answer later than to get the wrong answer now. mike -- Mike Meyer m...@mired.org http://www.mired.org/ Independent Software developer/SCM consultant, email for more information. O ascii ribbon campaign - stop html mail - www.asciiribbon.org ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Inference for RankNTypes
Hi list,
I am a bit puzzled by the behaviour exemplified by this code:
{-# LANGUAGE RankNTypes #-}
one :: (forall a. a - a) - b - b
one f = f
two = let f = flip one in f 'x' id
three = (flip one :: b - (forall a. a - a) - b) 'x' id
four = flip one 'x' id
Try to guess if this code typechecks, and if not what’s the error.
While `two' and `three' are fine, GHC (7.4.1 and 7.6.1) complains about `four':
Line 8: 1 error(s), 0 warning(s)
Couldn't match expected type `forall a. a - a'
with actual type `a0 - a0'
In the third argument of `flip', namely `id'
In the expression: flip one 'x' id
In an equation for `four': four = flip one 'x' id
So for some reason the quantified variable in `id' gets instantiated before it
should, and I have no idea why.
Any ideas?
Francesco
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Inference for RankNTypes
At Wed, 02 Jan 2013 12:32:53 +0100,
Francesco Mazzoli wrote:
Hi list,
I am a bit puzzled by the behaviour exemplified by this code:
{-# LANGUAGE RankNTypes #-}
one :: (forall a. a - a) - b - b
one f = f
two = let f = flip one in f 'x' id
three = (flip one :: b - (forall a. a - a) - b) 'x' id
four = flip one 'x' id
Try to guess if this code typechecks, and if not what’s the error.
While `two' and `three' are fine, GHC (7.4.1 and 7.6.1) complains about
`four':
Line 8: 1 error(s), 0 warning(s)
Couldn't match expected type `forall a. a - a'
with actual type `a0 - a0'
In the third argument of `flip', namely `id'
In the expression: flip one 'x' id
In an equation for `four': four = flip one 'x' id
So for some reason the quantified variable in `id' gets instantiated before it
should, and I have no idea why.
Any ideas?
Francesco
OK, I should have looked at the manual first. From
http://www.haskell.org/ghc/docs/latest/html/users_guide/other-type-extensions.html#id623016:
“For a lambda-bound or case-bound variable, x, either the programmer provides an
explicit polymorphic type for x, or GHC's type inference will assume that x's
type has no foralls in it.”. So there is a difference between let-bound things
and the rest.
I still don’t get exactly what’s going on there. What’s the inferred type for
`flip one', and why is it causing that error? Since there really isn’t much to
infer here.
Francesco
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Object Oriented programming for Functional Programmers
Well, we can say "concepts" in place of "theory". And I'm comparing Eiffel with other OOP lang, not with some langs based on a solid math theory (lambda calcules for FP langs, for example). ok? DbC is not the same as "assert macros". First, it has a lang semantic. There is an interesting graduated mechanism to turn off or turn on conditions' checking. Dbc is not only initeresting "concept" of lang. Meyer is considering class as a type in his type system. By the way, preconditions and postconditions of class and its subclass have to be consistient. I don't remeber all details now, as I remeber preconditions of subclass are automaticly logically 'and'ed to preconditions of superclass. This supports "concept" of "class is type" and "subclass is a same type as superclass". Other "concept" - classes are only modules. Other "concept" - "command/query separation" = dividing functions on functions that change state of object and on functions that query some info from function (sic. pure functions!). Other "concept" - polymorphic types (general types) - parametrisied types, including constrained parametrisied types (MAP [V, K - HASHABLE]). Other "concept" - solving multiple inherient problem - "name clashing" And so on. BTW. Why you think that Eiffel type system is unsafe? I don't what is a situation with java type now (not using java for several yeas), but I thought that java type system is more unsafe that eiffel type system. (They said that there were generic types in java). And BTW, smalltalk is a lang with dynamic type system. PS. In structuring programming, to prove correctness of loop construction, you have to write down precondition of loop, loop invariant, loop postcondition. You have to (mathamaticly) prove: if precondition holds than invariant holds (and in result we get solved postcondition).___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Object Oriented programming for Functional Programmers
Opps... I forgot about Eiffel agents! PS. After participationing in this discussion I'm tempting to reread Meyer's book after 10 years interval, to have a detailed look at the eiffel from the FP position. When I read this book first I know nothing about FP. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Inference for RankNTypes
* Francesco Mazzoli f...@mazzo.li [2013-01-02 13:04:36+0100]
At Wed, 02 Jan 2013 12:32:53 +0100,
Francesco Mazzoli wrote:
Hi list,
I am a bit puzzled by the behaviour exemplified by this code:
{-# LANGUAGE RankNTypes #-}
one :: (forall a. a - a) - b - b
one f = f
two = let f = flip one in f 'x' id
three = (flip one :: b - (forall a. a - a) - b) 'x' id
four = flip one 'x' id
Try to guess if this code typechecks, and if not what’s the error.
While `two' and `three' are fine, GHC (7.4.1 and 7.6.1) complains about
`four':
Line 8: 1 error(s), 0 warning(s)
Couldn't match expected type `forall a. a - a'
with actual type `a0 - a0'
In the third argument of `flip', namely `id'
In the expression: flip one 'x' id
In an equation for `four': four = flip one 'x' id
So for some reason the quantified variable in `id' gets instantiated before
it
should, and I have no idea why.
Any ideas?
Francesco
OK, I should have looked at the manual first. From
http://www.haskell.org/ghc/docs/latest/html/users_guide/other-type-extensions.html#id623016:
“For a lambda-bound or case-bound variable, x, either the programmer provides
an
explicit polymorphic type for x, or GHC's type inference will assume that x's
type has no foralls in it.”. So there is a difference between let-bound
things
and the rest.
I don't see how this is relevant.
GHC correctly infers the type of flip one 'x':
*Main :t flip one 'x'
flip one 'x' :: (forall a. a - a) - Char
But then somehow it fails to apply this to id. And there are no bound
variables here that we should need to annotate.
Roman
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Object Oriented programming for Functional Programmers
On 2013-01-02, at 4:41 AM, MigMit miguelim...@yandex.ru wrote: On Jan 2, 2013, at 2:26 AM, Bob Hutchison hutch-li...@recursive.ca wrote: On 2013-01-01, at 3:47 PM, MigMit miguelim...@yandex.ru wrote: Well, probably one of the reasons is that I've learned Eiffel later than Haskell. But really, Design by Contract — a theory? It certainly is a useful approach, but it doesn't seem to be a theory, not until we can actually prove something about it, and Eiffel doesn't seem to offer anything in this direction. Don't confuse OOSC2 and Eiffel. Eiffel implements the ideas in OOSC2 as best as Meyer can, but they are not the same thing. Well, we were talking about Eiffel. OOSC2 deserves a few unkind words as well, but I won't go there. And, personally, I think I would be willing to call DbC a theory, or a close precursor to a theory. I don't know about DbC in general, but it's implementation in Eiffel seems to be nothing more than a few ASSERT macros, for some weird reason embedded into the language. Hmm. I must disagree with you here. I've used three Eiffel systems, ISE, Small/SmartEiffel, and Tower. They all implemented DbC pretty thoroughly. In my opinion, every other implementation of DbC pale in comparison, to the point where they're hardly DbC at all. Are we talking about the same thing? There are three major components (in my opinion) to DbC: pre and post conditions, and class invariants. Pre and post conditions and invariants cannot be implemented simply as asserts. I'll have to refer you to OOSC2 for the (many) details, but a few of the more interesting aspects of these constructs are: 1) error reporting. If a precondition is violated the caller is flagged as the source of the error and error messages, stack traces, etc all reflect the caller. If a post condition is violated it's the callee who is responsible. And the error reports generated are rather good. 2) prepost conditions and class invariants have defined behaviour in cases of inheritance, even/especially multiple inheritance. They are combined non-trivially in subclasses. Without this I don't think you have DbC. 3) invariants are not checked for calls within a class (self.method does not have them checked, other.method does) 4) You have access to all the parameters for prepost conditions, and results for post conditions. Access to the initial state of the object is supposed to be there but I don't think all implementations support that. That's only a brief summary, it goes further than that, again I refer you to OOSC2 (and any of the Eiffel implementations I mentioned, and I don't know of any other implementations). This is nothing like a few assert macros. So, I think, you're saying take away the contracts and the outcome of compilation won't be any different. Whereas take away the types and Haskell is stopped cold. And that difference makes contracts a 'hack' but types not a 'hack'? I wasn't clear enough, sorry. I'm sure it's due to sleep deprivation. Or coffee deprivation. See, there are two parts of Eiffel, as I see it. First one is the contracts part. Second is… well, everything else. Second part seems to be doing all the real job, while the first one is doing something invisible, something that leaves no trace in the final result. Which doesn't mean it's unimportant, of course. The contracts part is designed to help the other part do it's job, but not to do the job by itself. Now, there are two problems with that: 1) The real job part needs helping. And a lot of it, actually, one doesn't need to look very closely to see that Eiffel type system is extremely unsafe (for the statically type language). Feel free to enlighten me about these obvious and extremely unsafe aspects of Eiffel's type system. Personally, I can't say I ever noticed. 2) The contracts part does a very poor job. Instead of really improving the inherent unsafety, it resorts to testing. And… What constitutes a 'good' job? 'Resorts' to testing. I have to admit to resorting to testing on occasion myself. Frequent occasion. Routinely even. :-) 2') ...not even the real, thorough testing — contracts system would be quite happy if the program works on the developer's machine. Which is the works for me approach certain languages gets rightfully blamed for. Really? You believe that automated testing and contracts are why software bugs *are not* found? Seems to me you're ignoring everything that happens between an empty directory and a working program. Contracts help in that process (I say but can't prove). I agree. They do help — but there are lots of things that help in this transition. Versioning systems. Collaboration tools. Bug tracking software. Text editors. Even debuggers. You should read OOSC2. You'll find that this is completely consistent with it. Don't forget that the 'C' in OOSC2 is 'contraction'. Cheers, Bob Pre and post
Re: [Haskell-cafe] Inference for RankNTypes
At Wed, 2 Jan 2013 14:49:51 +0200, Roman Cheplyaka wrote: I don't see how this is relevant. Well, moving `flip one' in a let solves the problem, and The fact that let-bound variables are treated differently probably has a play here. I originally thought that this was because the quantifications will be all to the left in the let-bound variable while without a let-bound variable the types are used directly. However this doesn’t explain the behaviour I’m seeing. GHC correctly infers the type of flip one 'x': *Main :t flip one 'x' flip one 'x' :: (forall a. a - a) - Char But then somehow it fails to apply this to id. And there are no bound variables here that we should need to annotate. Right. The weirdest thing is that annotating `flip one' (as in `three' in my code) or indeed `flip one 'x'' with the type that shows up in ghci makes things work: five = (flip one 'x' :: (forall a. a - a) - Char) id Francesco ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Object Oriented programming for Functional Programmers
On 2013-01-02, at 7:56 AM, Bob Hutchison hutch-li...@recursive.ca wrote: You should read OOSC2. You'll find that this is completely consistent with it. Don't forget that the 'C' in OOSC2 is 'contraction'. 'Construction' of course… the automated spell checker is not my friend :-( ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Object Oriented programming for Functional Programmers
Hi, First, I see (posts on this mailing list) that OO ideas are well known in functional community :) So my questions for you all are: * Is it really worthwhile for me to learn OO-programming? Learn or not to learn? I would say: yes! There is whole new universe to discover: UML, design patterns, classes and objects, data structures based on 'pointers' (and you can modify them, surprise!) and of course many algorithms that work on this structures (please note, that many books about algorithms and data structures take imperative approach), OO databases, many many many libraries for almost any thing! and finally, you will be able to try stable, well known and widely used tools (think about GUIs, game engines, embedded systems, mobile devices and all this fascinating stuff you can do with them). * If so, where should I start? There are plenty of functional programming for OO programmers but I have never seen OO programming for functional programmers. Get a book (big and heavy!), forget all about programming and read it with fresh mind. Do _all_ exercises from that book. * Is it true that learning other programming languages leads to a better use of your favorite programming language? I would say, any know knowledge has impact on your life. Programming skills also. * Will I learn new programming strategies that I can use back in the Haskell world? Here I can't say much, I'm just starting with Haskell, but if you would go with C++, then you will also learn some C by the way, FFI is waiting.. Thanks in advance for your kind responses, I hope it was helpful. Emanuel ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Object Oriented programming for Functional Programmers
On 2013-01-02, at 1:52 AM, Mike Meyer m...@mired.org wrote: [Context destroyed by top posting.] MigMit miguelim...@yandex.ru wrote: But really, Design by Contract — a theory? It certainly is a useful approach, but it doesn't seem to be a theory, not until we can actually prove something about it, and Eiffel doesn't seem to offer anything in this direction. You just stated (briefly, and not very rigorously) the theory: DbC is a useful approach to programing. Note that it's a theory about *programming*, not the resulting program. And by hack I meant not the presence of pre/postconditions, but the fact that they don't affect anything else. Strip all of them away, and you'll have the program which is, essentially, the same (and, in fact, pre/postconditions are supposed to be removed in the final version of the program). Compare this to Haskell types, for example: an untyped version of Haskell won't be able to choose between two class instances, so, that would be an entirely different language. Type classes are the wrong feature to look at. Type signatures are closer to what DbC is. Are type signatures a hack to get around deficiencies in the type inferencing engine? After all, you can strip all of them away and have essentially the same program. Eiffel programmers certainly consider the prepost conditions and invariants to be part of the signature. DbC is closely related to the management of state, and so to the object as a whole not just the parameters to a method. Now, I'm no expert in Haskell so treat the next part of this paragraph accordingly... putting invariants and conditions on monads, in particular to the entry and exit from do notation might be interesting. No particular ideas as to how you'd do that, or even if it'd be useful, but it seems to me to be a bit closer to the level of abstraction where DbC is at in Eiffel. Personally, I think the answer is no, and for the same reason. We add type signatures to top level functions because it helps document the function, and to help isolate type errors during compilation. They makes *programming* easier, even if they don't change the program at all. Pre and Post conditions (and class invariants - they're also part of DbC!) serve pretty much the same function. They help document the classes and methods, and tools that generate class/method documentation from source always include them. They're as important as the type signature. They also help isolate bugs, in that you get told explicitly that routine foo passed in an invalid parameter to bar rather than an exception somewhere deep in the guts of bar that you have to work back from to find foo. As I said before, I'm not sure I agree that the latter is worth the cost of using them for anything complex. The bugs they uncover are as likely to be in the pre/post conditions as in the code proper. The documentation benefit is unquestionable, though. And if some condition is worth documenting, then having it as executable documentation means it gets tested with the rest of the code, so you know the documentation is correct. Which means that just adding conditions to a language misses most of the benefit of DbC. You need to fix the documentation system as well. I can only speak from personal experience here. I used Eiffel as my primary programming language in the 1990's for about 10 years. I wrote a lot of code in Eiffel, and I used prepost conditions and class invariants extensively (and loop invariants surprisingly often). Some of that code would certainly be described as 'complex'. Yes, documentation is a huge part of what DbC gives you, but a peculiarly aggressive kind of documentation that tells you when you're doing it wrong. The biggest problem I had with writing prepost conditions and class invariants was missing part of what should be specified and so letting things pass that shouldn't have. The next biggest problem was being overly specific (I sometimes do the same thing with type signatures in Haskell I'm afraid). Bugs in the code of the conditions and invariants was not much of a problem I found (I can't recall any). It does take a while to learn how to write the conditions and how to accommodate DbC concepts when you write a class or class hierarchy. And, occasionally, the balancing act between DbC and unit tests is tricky. This is the kind of theory that you'll find in OOSC: why the features that are there help make programming easier. Not theories about how they make the resulting program better. Those two have a lot in common, though. Anything that makes witing correct code easier generally results in a better program. -- Sent from my Android tablet with K-9 Mail. Please excuse my swyping. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Inference for RankNTypes
Your example doesn't work for the same reason the following doesn't work: id runST (some st code) It requires the inferencer to instantiate certain variables of id's type to polymorphic types based on runST (or flip's based on one), and then use that information to check some st code (id in your example) as a polymorphic type. At various times, GHC has had ad-hoc left-to-right behavior that made this work, but it no longer does. Right now, I believe it only has an ad-hoc check to make sure that: runST $ some st code works, and not much else. Note that even left-to-right behavior covers all cases, as you might have: f x y such that y requires x to be checked polymorphically in the same way. There are algorithms that can get this right in general, but it's a little tricky, and they're rather different than GHC's algorithm, so I don't know whether it's possible to make GHC behave correctly. The reason it works when you factor out or annotate flip one 'x' is that that is the eventual inferred type of the expression, and then it knows to expect the id to be polymorphic. But when it's all at once, we just have a chain of unifications relating things like: (forall a. a - a) ~ beta ~ (alpha - alpha), where beta is part of type checking flip, and alpha - alpha is the instantiation of id's type with unification variables, because we didn't know that it was supposed to be a fully polymorphic use. And that unification fails. On Wed, Jan 2, 2013 at 8:21 AM, Francesco Mazzoli f...@mazzo.li wrote: At Wed, 2 Jan 2013 14:49:51 +0200, Roman Cheplyaka wrote: I don't see how this is relevant. Well, moving `flip one' in a let solves the problem, and The fact that let-bound variables are treated differently probably has a play here. I originally thought that this was because the quantifications will be all to the left in the let-bound variable while without a let-bound variable the types are used directly. However this doesn’t explain the behaviour I’m seeing. GHC correctly infers the type of flip one 'x': *Main :t flip one 'x' flip one 'x' :: (forall a. a - a) - Char But then somehow it fails to apply this to id. And there are no bound variables here that we should need to annotate. Right. The weirdest thing is that annotating `flip one' (as in `three' in my code) or indeed `flip one 'x'' with the type that shows up in ghci makes things work: five = (flip one 'x' :: (forall a. a - a) - Char) id Francesco ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] [Haskell-beginners] ghc and android
On Tue, Jan 1, 2013 at 3:41 PM, Brandon Allbery allber...@gmail.com wrote: On Tue, Jan 1, 2013 at 9:13 AM, Bernhard Urban lew...@gmail.com wrote: The main issue: The GHC runtime relies on glibc I have to assume this is not meant literally, because ghc works on OS X and *BSD. Right. I was talking about the situation on Linux, hopefully I'm totally wrong with that statement :) How can I build GHC without glibc on Linux? What should I use instead? That would certainly help. Thanks, Bernhard ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Inference for RankNTypes
On Wed, Jan 2, 2013 at 11:20 AM, Dan Doel dan.d...@gmail.com wrote: Note that even left-to-right behavior covers all cases, as you might have: f x y such that y requires x to be checked polymorphically in the same way. There are algorithms that can get this right in general, but it's a little tricky, and they're rather different than GHC's algorithm, so I don't know whether it's possible to make GHC behave correctly. Oops, that should have been, note that not even left-to-right behavior covers all cases. Also, I don't mean to imply that GHC is behaving wrongly. Situations like these are usually the result of necessary trade-offs in the algorithms. GHC does a lot of things that algorithms that successfully check this type of examples don't have to deal with at all. You have to pick your poison. -- Dan ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Inference for RankNTypes
At Wed, 2 Jan 2013 11:20:46 -0500, Dan Doel wrote: Your example doesn't work for the same reason the following doesn't work: id runST (some st code) It requires the inferencer to instantiate certain variables of id's type to polymorphic types based on runST (or flip's based on one), and then use that information to check some st code (id in your example) as a polymorphic type. At various times, GHC has had ad-hoc left-to-right behavior that made this work, but it no longer does. Right now, I believe it only has an ad-hoc check to make sure that: runST $ some st code works, and not much else. Note that even left-to-right behavior covers all cases, as you might have: f x y such that y requires x to be checked polymorphically in the same way. There are algorithms that can get this right in general, but it's a little tricky, and they're rather different than GHC's algorithm, so I don't know whether it's possible to make GHC behave correctly. The reason it works when you factor out or annotate flip one 'x' is that that is the eventual inferred type of the expression, and then it knows to expect the id to be polymorphic. But when it's all at once, we just have a chain of unifications relating things like: (forall a. a - a) ~ beta ~ (alpha - alpha), where beta is part of type checking flip, and alpha - alpha is the instantiation of id's type with unification variables, because we didn't know that it was supposed to be a fully polymorphic use. And that unification fails. Hi Dan, Thanks a lot for the answer, one forgets that with HM you always replace the quantified variables immediately. However I am still confused on how GHC makes it work when I annotate or put things in separate variables. In other words, can you provide links or clarify how this procedure works: The reason it works when you factor out or annotate flip one 'x' is that that is the eventual inferred type of the expression, and then it knows to expect the id to be polymorphic. Thanks, Francesco ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] [Haskell-beginners] ghc and android
Hello, rather than native GHC run on top of Android, I would recommend to have a look at GHC HEAD and attempt to cross-compile to Android. On ghc-cvs@ mailing list I've seen some work done for cross-compiling to QNX/BlackBerry OS 10 so I think Androind should be also doable with some work... Cheers, Karel On 01/ 2/13 05:29 PM, Bernhard Urban wrote: On Tue, Jan 1, 2013 at 3:41 PM, Brandon Allberyallber...@gmail.com wrote: On Tue, Jan 1, 2013 at 9:13 AM, Bernhard Urbanlew...@gmail.com wrote: The main issue: The GHC runtime relies on glibc I have to assume this is not meant literally, because ghc works on OS X and *BSD. Right. I was talking about the situation on Linux, hopefully I'm totally wrong with that statement :) How can I build GHC without glibc on Linux? What should I use instead? That would certainly help. Thanks, Bernhard ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Proving programs
Christopher, there's an introduction to proof for functional programs at http://www.cs.kent.ac.uk/people/staff/sjt/Pubs/ProofChapter.pdf I hope that you find it useful. Kind regards Simon On 1 Jan 2013, at 23:24, Christopher Howard christopher.how...@frigidcode.com wrote: 1. Does this approach need to be adjusted for a functional language, in which computation is (at least idealistically) distinct from control flow? 2. How do we approach this for programs that have an input loop (or recursion)? E.g., I have an application that reads one line for stdin, modifies said line, outputs to stdout, and repeats this process until EOF? Should I be thinking of every iteration as a separate program? Simon Thompson | Professor of Logic and Computation School of Computing | University of Kent | Canterbury, CT2 7NF, UK s.j.thomp...@kent.ac.uk | M +44 7986 085754 | W www.cs.kent.ac.uk/~sjt ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Inference for RankNTypes
If you want to know the inner workings, you probably need to read the OutsideIn(X) paper.* I'm not that familiar with the algorithm. But what happens is something like this When GHC goes to infer the type of 'f x' where it knows that f's argument is expected to be polymorphic, this triggers a different code path that will check that x can be given a type that is at least as general as is necessary for the argument. However, flip one 'x' id gives flip a type like (alpha - beta - gamma) - beta - alpha - gamma. Then, we probably get some constraints collected up like: alpha ~ (forall a. a - a) alpha ~ (delta - delta) That is, it does not compute the higher-rank type of flip one 'x' and then decide how the application of that to id should be checked; it decides how all the arguments should be checked based only on flip's type, and flip does not have a higher-rank type on its own. And solving the above constraints cannot trigger the alternate path. However, when you factor out or annotate flip one 'x', it knows that it's applying something with a higher-rank type (whether because it inferred it separately, or you gave it), and that does trigger the alternate code path. If that's still too vague, you'll have to refer to the paper. -- Dan * http://research.microsoft.com/en-us/um/people/simonpj/papers/constraints/jfp-outsidein.pdf On Wed, Jan 2, 2013 at 11:47 AM, Francesco Mazzoli f...@mazzo.li wrote: At Wed, 2 Jan 2013 11:20:46 -0500, Dan Doel wrote: Your example doesn't work for the same reason the following doesn't work: id runST (some st code) It requires the inferencer to instantiate certain variables of id's type to polymorphic types based on runST (or flip's based on one), and then use that information to check some st code (id in your example) as a polymorphic type. At various times, GHC has had ad-hoc left-to-right behavior that made this work, but it no longer does. Right now, I believe it only has an ad-hoc check to make sure that: runST $ some st code works, and not much else. Note that even left-to-right behavior covers all cases, as you might have: f x y such that y requires x to be checked polymorphically in the same way. There are algorithms that can get this right in general, but it's a little tricky, and they're rather different than GHC's algorithm, so I don't know whether it's possible to make GHC behave correctly. The reason it works when you factor out or annotate flip one 'x' is that that is the eventual inferred type of the expression, and then it knows to expect the id to be polymorphic. But when it's all at once, we just have a chain of unifications relating things like: (forall a. a - a) ~ beta ~ (alpha - alpha), where beta is part of type checking flip, and alpha - alpha is the instantiation of id's type with unification variables, because we didn't know that it was supposed to be a fully polymorphic use. And that unification fails. Hi Dan, Thanks a lot for the answer, one forgets that with HM you always replace the quantified variables immediately. However I am still confused on how GHC makes it work when I annotate or put things in separate variables. In other words, can you provide links or clarify how this procedure works: The reason it works when you factor out or annotate flip one 'x' is that that is the eventual inferred type of the expression, and then it knows to expect the id to be polymorphic. Thanks, Francesco ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Inference for RankNTypes
At Wed, 2 Jan 2013 13:35:24 -0500, Dan Doel wrote: If you want to know the inner workings, you probably need to read the OutsideIn(X) paper.* I'm not that familiar with the algorithm. But what happens is something like this When GHC goes to infer the type of 'f x' where it knows that f's argument is expected to be polymorphic, this triggers a different code path that will check that x can be given a type that is at least as general as is necessary for the argument. However, flip one 'x' id gives flip a type like (alpha - beta - gamma) - beta - alpha - gamma. Then, we probably get some constraints collected up like: alpha ~ (forall a. a - a) alpha ~ (delta - delta) That is, it does not compute the higher-rank type of flip one 'x' and then decide how the application of that to id should be checked; it decides how all the arguments should be checked based only on flip's type, and flip does not have a higher-rank type on its own. And solving the above constraints cannot trigger the alternate path. However, when you factor out or annotate flip one 'x', it knows that it's applying something with a higher-rank type (whether because it inferred it separately, or you gave it), and that does trigger the alternate code path. If that's still too vague, you'll have to refer to the paper. -- Dan * http://research.microsoft.com/en-us/um/people/simonpj/papers/constraints/jfp-outsidein.pdf Thanks again for the answer. I understood more or less what was going on with the constraints - what I was wondering is how that alternate code path you cite works. I guess I’ll have to attack that epic paper sooner or later :). Francesco ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Object Oriented programming for Functional Programmers
On Jan 2, 2013, at 4:24 PM, Никитин Лев leon.v.niki...@pravmail.ru wrote: Well, we can say concepts in place of theory. And I'm comparing Eiffel with other OOP lang, not with some langs based on a solid math theory (lambda calcules for FP langs, for example). ok? I agree that there are certain concepts, or ideas, that Eiffel is built on. If that is what you meant, sure, I have no problem with that. Of course, there are plenty of languages based on some specific ideas. For example, take the following concepts: 1) it's better to do something instead of failing, even if it doesn't make any sense; 2) global is better then local; 3) for every feature that can be implemented in two ways there should be a switch that the user can set as xe wishes. Implement these as fully as possible — and you'll get PHP. So, somehow I doubt that being based on some set of ideas is a very strong selling point. BTW. Why you think that Eiffel type system is unsafe? Well, if I remember correctly, if you call some method of a certain object, and this call compiles, you can't be certain that this object actually has this method. Could be that this object belongs to some subclass which removes this method. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Object Oriented programming for Functional Programmers
2) prepost conditions and class invariants have defined behaviour in cases of inheritance, even/especially multiple inheritance. They are combined non-trivially in subclasses. Without this I don't think you have DbC. Yes, I forgot about that. Thanks. Feel free to enlighten me about these obvious and extremely unsafe aspects of Eiffel's type system. Personally, I can't say I ever noticed. Correct me if I'm wrong, but isn't it true that methods can be removed in subclasses? If that's not extreme, I don't know what is. 2) The contracts part does a very poor job. Instead of really improving the inherent unsafety, it resorts to testing. And… What constitutes a 'good' job? Well, a sound type system would certainly help. 'Resorts' to testing. I have to admit to resorting to testing on occasion myself. Frequent occasion. Routinely even. :-) You routinely try to overcome language weakness with tests? 2') ...not even the real, thorough testing — contracts system would be quite happy if the program works on the developer's machine. Which is the works for me approach certain languages gets rightfully blamed for. Really? You believe that automated testing and contracts are why software bugs *are not* found? Is that what I said? I believe that testing means a lot more than just making sure the program works on the developer's computer. I believe that system that encourages the works for me approach is one of the reasons software bugs are not found. Seems to me you're ignoring everything that happens between an empty directory and a working program. Contracts help in that process (I say but can't prove). I agree. They do help — but there are lots of things that help in this transition. Versioning systems. Collaboration tools. Bug tracking software. Text editors. Even debuggers. You should read OOSC2. You'll find that this is completely consistent with it. I've never said it's not. But all of these tools are external to the language, which means that they can be easily replaced if a better alternative surfaces. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Object Oriented programming for Functional Programmers
On 1/2/13 4:29 PM, MigMit wrote: BTW. Why you think that Eiffel type system is unsafe? Well, if I remember correctly, if you call some method of a certain object, and this call compiles, you can't be certain that this object actually has this method. Could be that this object belongs to some subclass which removes this method. Eiffel doesn't handle the relationship of co- and contra-variance of arguments with subtyping in a principled way. This is apparently known as the catcall problem. See, e.g., this article: http://www.eiffelroom.org/node/517 --Gershom ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Object Oriented programming for Functional Programmers
On Jan 3, 2013, at 2:09 AM, Gershom Bazerman gersh...@gmail.com wrote: On 1/2/13 4:29 PM, MigMit wrote: BTW. Why you think that Eiffel type system is unsafe? Well, if I remember correctly, if you call some method of a certain object, and this call compiles, you can't be certain that this object actually has this method. Could be that this object belongs to some subclass which removes this method. Eiffel doesn't handle the relationship of co- and contra-variance of arguments with subtyping in a principled way. This is apparently known as the catcall problem. See, e.g., this article: http://www.eiffelroom.org/node/517 Yes, variance is another big source of unsafety, that's for sure. And another reason I think there is no real theory behind Eiffel, just a bunch of features (or concepts) boiled together. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] [Announcement] New SBV release
I'm happy to announce v2.9 release of the Haskell SBV library: http://leventerkok.github.com/sbv/ SBV (SMT Based Verification) is a library that allows Haskell programs to take advantage of modern SMT solvers, by providing a symbolic simulation engine that can invoke 3rd party SMT solvers to prove/falsify properties about (a certain class of) Haskell programs. New in this release is the support for the CVC4 SMT solver: http://cvc4.cs.nyu.edu/web/ If you were planning to use SMT solvers before, but were worried about the not-so-commercial-friendly licenses of Yices and Z3, then this is a great opportunity: *CVC4 comes with essentially no limit on its use for research or commercial purposes*! Feedback, patches and bug reports are always welcome. -Levent. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Proving programs
On Wed, Jan 2, 2013 at 12:22 PM, Simon Thompson s.j.thomp...@kent.ac.uk wrote: Christopher, there's an introduction to proof for functional programs at http://www.cs.kent.ac.uk/people/staff/sjt/Pubs/ProofChapter.pdf Simon, is it possible to get the list of the bibliographic references used in the chapter? Best regards, -- Andrés ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Safe 'chr' function?
Hello, I'm working on a general text-processing library [1] and one of my quickcheck tests is designed to make sure that my library doesn't throw exceptions (it returns an Either type on failure). However, there are some inputs that cause me to pass bogus values to the 'chr' function (such as 1208914), which causes it to throw an exception. Is there a version of that function that is safe? (I'm hoping for something like Int - Maybe Char). Alternatively, is there a way to know ahead of time whether or not an Int will cause 'chr' to throw an exception? Thanks, Myles C. Maxfield [1] http://hackage.haskell.org/package/punycode ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
