5 ms·

While I fully agree that pure code is far easier to maintain than impure code, and the advantages of Haskell are numerous, I think it is a bit strong to state t

While I fully agree that pure code is far easier to maintain than impure code, and the advantages of Haskell are numerous, I think it is a bit strong to state that such claims are backed up by mathematical proofs. Ease of maintenance is a fundamentally subjective claim that cannot be proven, but must be borne out by individual experience (as it has been for you, me, and many others).

chongli 13y ago
Ease of maintenance is a fundamentally subjective claim that cannot be proven, but must be borne out by individual experience (as it has been for you, me, and many others). I disagree. You can make objective measurements of maintainability. You can look at cyclomatic complexity and reusability (both wins for pure functions). You can test how often changes lead to bugs and how often the errors are caught. There are many instances of Haskell code where there is only one sensible implementation of a function, given its type. Hell, some Haskell libraries have even been formally verified though admittedly that is done with external packages. I will agree on one thing, though: you do run into trouble when you throw around the word all (or indeed any absolute) without actually meaning it.
- bunderbunder 13y ago
  > You can look at cyclomatic complexity and reusability (both wins for pure functions). Yes, those are both wins for pure functions. But even there you need an asterisk, because side effects do have their place - the fact of the matter is, the primary task of most real-world software can be summed up as "manipulating mutable state". In light of that I don't think you can necessarily jump from the observation that there are many situations where pure functions are easier to work with than impure ones to the conclusion that pure functions are inherently more maintainable. But even if that were granted for the sake of argument, it's not much of a win for Haskell. The ability to create pure functions is a feature of every language that has been invented during the lifetime of probably every person reading this post, and therefore not really a differentiating feature of Haskell. Nor is lack of ability to create impure functions a feature that can be claimed of Haskell, because that simply isn't true. Haskell's real differentiator in that department is just that you've got to jump through hoops to do it. And if your business rules are inherently impure, then it's not clear to me how a language that tries to ghettoize impurity makes them easier to implement.
  - tmhedberg 13y ago
    The win for Haskell is that it wears its statefulness on its sleeve. Of course you can, with sufficient discipline, write pure code in any language, though it can be frustratingly difficult in languages where libraries make idiomatic use of mutation. And yes, you can also write impure code in Haskell, at least for some definitions of "impure". What you can't do in Haskell is write impure code that claims to be pure (up to the customarily and idiomatically avoided `unsafePerformIO`), or write code whose degree of statefulness is ambiguous. Reliable, explicit, and statically enforced purity holds more than just theoretical benefits. I don't have to read through library code to see if it is thread-safe. I don't have to worry about whether passing a data structure to a library function will result in that structure being mutated behind my back. I don't have to trust code comments that may not be in sync with the current state of the code. Simply by virtue of the fact that a function does not mention `IO` in its type, I can have total confidence that it won't violate my assumptions about its behavior. And I don't even have to take it on faith that the author wrote the correct type for his code; if he hadn't, the compiler would have rejected it. This is the difference between "pure by convention" and "provably pure". Every language must necessarily have an "IO monad" and interact with the inherently stateful world, or else it is useless. Haskell is different not because you can choose to avoid I/O, but because when you do so, the type system will back you up with perfect accuracy.
  - chongli 13y ago
    But even if that were granted for the sake of argument, it's not much of a win for Haskell. The ability to create pure functions is a feature of every language that has been invented during the lifetime of probably every person reading this post, and therefore not really a differentiating feature of Haskell. I already dealt with this three posts above: And no, it's not the case that Haskell is the only language which allows you to write pure functions. People who try to claim that are being silly and dishonest. Haskell's advantage is that its type system allows you to know at a glance whether or not a function is pure. Nor is lack of ability to create impure functions a feature that can be claimed of Haskell, because that simply isn't true. Haskell's real differentiator in that department is just that you've got to jump through hoops to do it. And if your business rules are inherently impure, then it's not clear to me how a language that tries to ghettoize impurity makes them easier to implement. That's only the case for beginners who don't understand monads and their associated libraries. For an experienced programmer, Haskell offers much more powerful and expressive (not to mention safe) means of combining effectful computations than typical imperative languages.
jroesch 13y ago
It is not a "strong" statement to say that some Haskell code is backed by proofs. There is Wadler's Theorems for free![1] which allows one to reason about pure function's behavior purely from type signatures. As well GHC supports various features that enables one to encode some dependent typing[2] constructs. Allowing the type of value to to depend on the value itself. A common example being a list that can expresses whether it is empty or not in its type. These types allow one to write functions with signatures like: `safeHead :: SafeList a NonEmpty -> a`. Uses of this function will fail to compile if I can not prove that my list will always be non-empty. Combine this with the well known Curry-Howard Correspondence [3] which shows that types have a direct correspondence to proofs. The logical extension of this is computer theorem proving languages like Coq, Agda, Epigram, Idris. For example Coq[4] uses a dependently typed lambda calculus as its proof term language, and sees wide spread use in the formal verification of software. It is not a stretch to say that less powerful types systems like Haskell's allow us to encode some forms of proof. If you view the type checker as an proof checker, one provides propositions to it (in the form of types) and then supplies proof (in the form of terms). These can be trivial propositions like `a :: Int`, which in Haskell there are 2^31 correct answers. [1] (http://ttic.uchicago.edu/~dreyer/course/papers/wadler.pdf http://ttic.uchicago.edu/~dreyer/course/papers/wadler.pdf) [2] (http://en.wikipedia.org/wiki/Dependent_type http://en.wikipedia.org/wiki/Dependent_type) [3] (http://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence http://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspond...) [4] (http://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence http://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspond...)
- tmhedberg 13y ago
  I'm aware of dependent types and, more generally, the strong undercurrent of emphasis on provable correctness in the Haskell community at large. I don't disagree at all with what you wrote, but it's not what I was referring to with my comment. My disagreement was specifically with the implied claim that it can be mathematically proven that Haskell code is easier to maintain than code written in other languages. That has indeed been my experience with Haskell, but I do not think it is directly provable. What seems easy for me may be stupefyingly difficult or confusing for someone else. "How easy something is" is not really a quantifiable measurement; it is a subjective experience. As chongli points out, however, there are related measurements that can be taken, such as cyclomatic complexity, and those at least seem to be correlated with ease of maintenance. So perhaps I'm just being overly pedantic!

chongli 13y ago

Ease of maintenance is a fundamentally subjective claim that cannot be proven, but must be borne out by individual experience (as it has been for you, me, and many others). I disagree. You can make objective measurements of maintainability. You can look at cyclomatic complexity and reusability (both wins for pure functions). You can test how often changes lead to bugs and how often the errors are caught. There are many instances of Haskell code where there is only one sensible implementation of a function, given its type. Hell, some Haskell libraries have even been formally verified though admittedly that is done with external packages. I will agree on one thing, though: you do run into trouble when you throw around the word all (or indeed any absolute) without actually meaning it.

bunderbunder 13y ago
> You can look at cyclomatic complexity and reusability (both wins for pure functions). Yes, those are both wins for pure functions. But even there you need an asterisk, because side effects do have their place - the fact of the matter is, the primary task of most real-world software can be summed up as "manipulating mutable state". In light of that I don't think you can necessarily jump from the observation that there are many situations where pure functions are easier to work with than impure ones to the conclusion that pure functions are inherently more maintainable. But even if that were granted for the sake of argument, it's not much of a win for Haskell. The ability to create pure functions is a feature of every language that has been invented during the lifetime of probably every person reading this post, and therefore not really a differentiating feature of Haskell. Nor is lack of ability to create impure functions a feature that can be claimed of Haskell, because that simply isn't true. Haskell's real differentiator in that department is just that you've got to jump through hoops to do it. And if your business rules are inherently impure, then it's not clear to me how a language that tries to ghettoize impurity makes them easier to implement.
- tmhedberg 13y ago
  The win for Haskell is that it wears its statefulness on its sleeve. Of course you can, with sufficient discipline, write pure code in any language, though it can be frustratingly difficult in languages where libraries make idiomatic use of mutation. And yes, you can also write impure code in Haskell, at least for some definitions of "impure". What you can't do in Haskell is write impure code that claims to be pure (up to the customarily and idiomatically avoided `unsafePerformIO`), or write code whose degree of statefulness is ambiguous. Reliable, explicit, and statically enforced purity holds more than just theoretical benefits. I don't have to read through library code to see if it is thread-safe. I don't have to worry about whether passing a data structure to a library function will result in that structure being mutated behind my back. I don't have to trust code comments that may not be in sync with the current state of the code. Simply by virtue of the fact that a function does not mention `IO` in its type, I can have total confidence that it won't violate my assumptions about its behavior. And I don't even have to take it on faith that the author wrote the correct type for his code; if he hadn't, the compiler would have rejected it. This is the difference between "pure by convention" and "provably pure". Every language must necessarily have an "IO monad" and interact with the inherently stateful world, or else it is useless. Haskell is different not because you can choose to avoid I/O, but because when you do so, the type system will back you up with perfect accuracy.
- chongli 13y ago
  But even if that were granted for the sake of argument, it's not much of a win for Haskell. The ability to create pure functions is a feature of every language that has been invented during the lifetime of probably every person reading this post, and therefore not really a differentiating feature of Haskell. I already dealt with this three posts above: And no, it's not the case that Haskell is the only language which allows you to write pure functions. People who try to claim that are being silly and dishonest. Haskell's advantage is that its type system allows you to know at a glance whether or not a function is pure. Nor is lack of ability to create impure functions a feature that can be claimed of Haskell, because that simply isn't true. Haskell's real differentiator in that department is just that you've got to jump through hoops to do it. And if your business rules are inherently impure, then it's not clear to me how a language that tries to ghettoize impurity makes them easier to implement. That's only the case for beginners who don't understand monads and their associated libraries. For an experienced programmer, Haskell offers much more powerful and expressive (not to mention safe) means of combining effectful computations than typical imperative languages.

jroesch 13y ago

It is not a "strong" statement to say that some Haskell code is backed by proofs. There is Wadler's Theorems for free![1] which allows one to reason about pure function's behavior purely from type signatures. As well GHC supports various features that enables one to encode some dependent typing[2] constructs. Allowing the type of value to to depend on the value itself. A common example being a list that can expresses whether it is empty or not in its type. These types allow one to write functions with signatures like: `safeHead :: SafeList a NonEmpty -> a`. Uses of this function will fail to compile if I can not prove that my list will always be non-empty. Combine this with the well known Curry-Howard Correspondence [3] which shows that types have a direct correspondence to proofs. The logical extension of this is computer theorem proving languages like Coq, Agda, Epigram, Idris. For example Coq[4] uses a dependently typed lambda calculus as its proof term language, and sees wide spread use in the formal verification of software. It is not a stretch to say that less powerful types systems like Haskell's allow us to encode some forms of proof. If you view the type checker as an proof checker, one provides propositions to it (in the form of types) and then supplies proof (in the form of terms). These can be trivial propositions like `a :: Int`, which in Haskell there are 2^31 correct answers. [1] (http://ttic.uchicago.edu/~dreyer/course/papers/wadler.pdf http://ttic.uchicago.edu/~dreyer/course/papers/wadler.pdf) [2] (http://en.wikipedia.org/wiki/Dependent_type http://en.wikipedia.org/wiki/Dependent_type) [3] (http://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence http://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspond...) [4] (http://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence http://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspond...)

tmhedberg 13y ago
I'm aware of dependent types and, more generally, the strong undercurrent of emphasis on provable correctness in the Haskell community at large. I don't disagree at all with what you wrote, but it's not what I was referring to with my comment. My disagreement was specifically with the implied claim that it can be mathematically proven that Haskell code is easier to maintain than code written in other languages. That has indeed been my experience with Haskell, but I do not think it is directly provable. What seems easy for me may be stupefyingly difficult or confusing for someone else. "How easy something is" is not really a quantifiable measurement; it is a subjective experience. As chongli points out, however, there are related measurements that can be taken, such as cyclomatic complexity, and those at least seem to be correlated with ease of maintenance. So perhaps I'm just being overly pedantic!