5 ms·

> And that's exactly what can be said about the difference between Haskell's and Java's type systems. This is a little bit disingenuous, for reasons exposed be

> And that's exactly what can be said about the difference between Haskell's and Java's type systems. This is a little bit disingenuous, for reasons exposed below. > do in fact result in cheaper development. I.e. you haven't shown that Haskell's rich type system solves a real problem. That requires empirical evidence. No disagreement here. I don't recall ever making any statements myself to the tone of «Haskell makes writing correct programs cheaper». But if someone else told you that, you're right - it requires empirical evidence. > But you said "perform your proofs in the same term language in which your program is written". And it is. Equational reasoning about Haskell programs is just using Haskell's existing reduction relation, extended with additional assumed identifications that can be used as reductions in either direction (given `a = b`, replacing either `a` for `b` or vice versa, though more often than not, only one direction is needed). Only at the last step do we need a check that two Haskell terms are syntactically equal, which, as you say, is not doable in Haskell itself (since judgmental term equality isn't first-class), although it is trivial to do by visual inspection. The fact remains that the bulk of the work of verifying non-IO Haskell code is really just evaluating Haskell code. > If the actual interesting verification is done by other tools why is your approach better than Amazon's (write in Java, verify in TLA+)? I can't comment on what's best for Amazon's needs, since I've never worked there. And, obviously, there's a lot more software engineering talent working for Amazon than sitting in front of my keyboard. That being said, I think the amount of effort required to evaluate Haskell[0] by hand is significantly less than the amount of effort required to translate back and forth between Java and TLA+. And, for my needs (mainly implementing compilers and libraries of data structures and algorithms), Haskell is a significantly better language than Java (or Lisp, Python, C++, what have you). Precisely because I can reason about Haskell programs by just evaluating Haskell[0] by hand, whereas doing the same in Java would require me to constantly translate back and forth between Java and an external logic. --- [0] Plus propositional equalities.

pron 11y ago
> Only at the last step do we need a check that two Haskell terms are syntactically equal I'm sorry, but that's just not true, or, more precisely, it's not necessarily doable in practice. For one, there's bounded recursion which may not be so easy to substitute, and that recursion interacts with equality to yield much richer properties. For example, if you pick a recursive QuickSort implementation (just picked sorting because that's a classical verification example) and wanted to verify it in Haskell, you'll need to prove much more than equality at each recursive step (or unwind the entire computation and then prove equality, but that's not a very convenient proof). Second, most interesting algorithms make use of time and state, so you'd need to prove past the semantics of the effect monad (STM, threads, whatever), and that also requires much more than simple equality (TLA+ and Esterel use temoporal logic, which is awesome, and I think Coq et al. use dependent types to encode modal logic, but I don't know how it's done or whether that's the approach). Haskell's logic is only marginally helpful in these scenarios and I don't know if translating from TLA+ to Java is harder or more error-prone than translating to Haskell, and even if it were, the difference (again, conjecture and gut feeling) seems to be marginal to offset the many other benefits of using Java. There are some interesting uses of Haskell's logic, such as session types (also possible in Java, BTW), but they are too underpowered to prove any distributed algorithm of interest (AFAICT, they are exactly as powerful as regular expressions). What bothers me most about Haskell's approach -- and correct me if I'm wrong -- is that the strength of the type system is pretty much defined to be "anything that's inferrable by an extended HM algorithm", which means that the strength is arbitrarily chosen to match a "convenience point" arbitrarily defined to be "full program inference", rather than an analysis of what strength is needed, and then tweaking it to trade off some strength for convenience. So it is the features of a certain algorithm which determines the language's semantics rather than an analysis of what's helpful. Good examples of the latter approach would be Java, Erlang and Clojure. (BTW, a good explanation of Java's design decision is in the first 17 minutes or so of this talk: https://www.youtube.com/watch?v=Dq2WQuWVrgQ https://www.youtube.com/watch?v=Dq2WQuWVrgQ) That is somehow (if you squint) similar to Prolog, whose utility was determined by the quality of it search algorithms. Such approach makes for great research, but its industrial applicability is very brittle. > Haskell is a significantly better language than Java ... Precisely because I can reason about Haskell programs by just evaluating Haskell by hand, whereas doing the same in Java would require me to constantly translate back and forth between Java and an external logic. Even if I were to accept that premise, that only shows Haskell is better in some aspects (which I gladly acknowledge; Haskell is awesome![1]). A programming language is much more than that. In fact, I believe extra-linguistic features of the runtime -- e.g. GC, threading, performance, monitorability, hackability, profilability -- are a much bigger contributors to productivity (and cost) than syntax-level abstractions. But again, I have no proof, but some (strong) evidence (namely, the incredible productivity gain when the industry switched from C/C++ to Java -- which are intentionally syntactically similar but with drastic extra-linguistic changes -- and the difficulty achieving similar gains by other JVM languages (different syntax, same-or-similar extra-linguistic features). EDIT: Also, you kind of describe reduction as "just" substitution, but if Mr. Church has taught us anything it is that "just substitution" is computation, and is as powerful (well, not quite, but in some respects) as a Turing machine. So there's no reason to assume that "just substituting" is any easier for a human than simulating state, be it in the mind, on a piece of paper or in a debugger (or, better yet, one of Java's awesome time-travelling debuggers). I tend to think (without proof) that the human mind is actually better suited to state simulation than to substitution (we simulate stuff all the time; lambda substitution is a very mathematical concept). To make this more concrete, recursion is limited assignment, and recursion combined with a continuation (or, in Haskell, a continuation monad) is imperative assignment (imperative state can be fully implemented in a pure language with continuations and recursion). So substituting across the cont monads is directly more complicated (computationally -- it requires lots of reductions) than state simulation of the very same computation. [1]: But, forgive me, so is Java.
- tel 11y ago
  Many things I could respond to, but out of convenience I'll just note that there's a reason why nobody programs in Haskell in the Cont monad unless they really can't avoid it!
  - pron 11y ago
    Sure, just as there are reasons people write simple pure functions in Java when that's the best approach, and they generally try to keep things simple and tractable. Obviously, there's plenty of terrible Java code out there, but there would be plenty of terrible Haskell code out there too if Haskell had similar levels of usage. In any case, I was responding to the general statement that Haskell's purity makes reasoning easy by mere virtue of being pure. Well, LC is pure and it can be just as messy as Turing machines. Haskell code -- like Java, C, and Python code -- is simple to reason about when it is written with care (yes, I know that there are differences, but as a general rule). Now, don't get me wrong: I'm all for Clojure-style, ML-style or Rust-style immutability-by-default (each, of course, is different as they all have different tradeoffs), but that's completely separate from purity.
    - tel 11y ago
      That's one nice thing provable in Haskell's type/effect system, though, that the ambient effects available are no stronger than X for various descriptions of X. I know you dislike that whole regime, but it at least in this specific case explicitly circumscribes situations where, e.g., Cont is too strong.
- catnaroek 11y ago
  > I'm sorry, but that's just not true, or, more precisely, it's not necessarily doable in practice. For one, there's bounded recursion which may not be so easy to substitute, and that recursion interacts with equality to yield much richer properties. In those cases, one possible strategy is to take a detour via auxiliary data types, which aren't declared in the program, but are isomorphic to types that do. For example, lately I've been working quite a lot with data structures based on skew-binomial numbers (zippers, lenses and traversals for skew-binomial trees and heaps). Their usual implementation is as linked lists of increasingly weighted trees, except for the first two ones, which may have the same weight. In my proofs, however, I work with an isomorphic type with two constructors: one for the case where the weights are all strictly increasing, another for the case where the first two trees have equal weights. This is no different from performing mathematical induction on Peano naturals, but using machine integers or big integers for actually performing arithmetic operations. > Second, most interesting algorithms make use of time and state, so you'd need to prove past the semantics of the effect monad (STM, threads, whatever), and that also requires much more than simple equality (TLA+ and Esterel use temoporal logic, which is awesome, and I think Coq et al. use dependent types to encode modal logic, but I don't know how it's done or whether that's the approach). Most algorithms that interest me are data transformations - some sequential, some parallel, but almost never concurrent. And, even in those few cases where the interleaving of concurrent computations actually matters to me (e.g., implementing serializable transaction support in a RDBMS that works for any valid schema), I highly doubt that the tools you mention have anything useful to offer, although I would love to be wrong here. > Haskell's logic is only marginally helpful in these scenarios and I don't know if translating from TLA+ to Java is harder or more error-prone than translating to Haskell and even if it were, the difference (again, conjecture and gut feeling) seems to be marginal to offset the many other benefits of using Java. For things like protocol verification, I'll take a substructural type system, like those of Rust and ATS, where non-forgeable, non-duplicable tokens are used to reify the states and transitions concurrent computations may undergo. This still offers an easier, more integrated workflow than translating between two different languages. > What bothers me most about Haskell's approach -- and correct me if I'm wrong -- is that the strength of the type system is pretty much defined to be "anything that's inferrable by an extended HM algorithm", which means that the strength is arbitrarily chosen to match a "convenience point" arbitrarily defined to be "full program inference", rather than an analysis of what strength is needed, and then tweaking it to trade off some strength for convenience. My analysis of what strength is needed is very simple: If the computer can do something perfectly, let it do it. If the computer can't do it perfectly, I'll do it myself. I have no taste for automated mistakes that have to be manually rolled back, such as program analyses whose results I can't fully trust. HM-style (or, more generally, ML^F-style) type reconstruction just happens to be something that a computer can do perfectly. > Even if I were to accept that premise, [that equational reasoning about Haskell programs is just normal Haskell term reduction] What part is hard to accept? > that only shows Haskell is better in some aspects (which I gladly acknowledge; Haskell is awesome![1]). Yep, only some aspects. Exactly the ones I happen to need to write correct programs - and prove them so. > A programming language is much more than that. In fact, I believe extra-linguistic features of the runtime -- e.g. GC, threading, performance, monitorability, hackability, profilability -- are a much bigger contributors to productivity (and cost) than syntax-level abstractions. Perhaps I'm just too noob, but I'm really happy that I don't need to care about tuning the behavior of a managed language's runtime system. It's too much of a black art for me to want to have anything to do with it. If performance ever becomes that much of a problem, I'll just call Rust or C++. > But again, I have no proof, but some (strong) evidence (namely, the incredible productivity gain when the industry switched from C/C++ to Java -- which are intentionally syntactically similar but with drastic extra-linguistic changes -- and the difficulty achieving similar gains by other JVM languages (different syntax, same-or-similar extra-linguistic features). I find my productivity when using Java even lower than when using C++, which is a really impressive achievement, considering that C++ is such an unproductive language. C++ supports (to a limited extent) and encourages (to an even more limited extent) a programming style where variables actually stand for legitimate values inhabiting your problem domain (varying between assignments or member function calls, of course). These values can be manipulated using equational reasoning. In Java, every non-primitively-typed variable stands for an object reference, which is effectively a reification of the time and circumstances in which the object was created, and most certainly not something I care about. So, when it comes to actually producing proofs of correctness of Java programs, I need to jump this additional layer of indirection between variables and the values I care about. Back and forth. Over and over. > Also, you kind of describe reduction as "just" substitution, but if Mr. Church has taught us anything it is that "just substitution" is computation, and is as powerful (well, not quite, but in some respects) as a Turing machine. Of course term rewriting is computation - if it weren't, it would be useless as a theoretical basis for programming languages! But «equivalent in raw power» doesn't imply «equally convenient to use». Models of computation based on term rewriting happen to be easy to reason about in a compartmentalized, divide-and-conquer manner than Turing machines. > So there's no reason to assume that "just substituting" is any easier for a human than simulating state, be it in the mind, on a piece of paper or in a debugger (or, better yet, one of Java's awesome time-travelling debuggers). I've burned way too much time in debugger sessions that could've been usefully spent doing anything else, like writing programs that don't need to be debugged, or simply enjoying life. I don't think the value I got from them justifies the cost of opportunity. Never did a debugger session give me full confidence that the program I've written is correct. Even worse, debugger sessions seldom told me where exactly my program (as in, the code, not the running process) is wrong. > I tend to think (without proof) that the human mind is actually better suited to state simulation than to substitution (we simulate stuff all the time; Speak for yourself. > lambda substitution is a very mathematical concept). What do you mean by «lambda substitution»? A bound variable (by any binder, such as lambda, mu, forall and exists) cannot be substituted - you need to extract the term under the binder first. If you mean «variable substitution», yes, of course it's a mathematical concept.

pron 11y ago

> Only at the last step do we need a check that two Haskell terms are syntactically equal I'm sorry, but that's just not true, or, more precisely, it's not necessarily doable in practice. For one, there's bounded recursion which may not be so easy to substitute, and that recursion interacts with equality to yield much richer properties. For example, if you pick a recursive QuickSort implementation (just picked sorting because that's a classical verification example) and wanted to verify it in Haskell, you'll need to prove much more than equality at each recursive step (or unwind the entire computation and then prove equality, but that's not a very convenient proof). Second, most interesting algorithms make use of time and state, so you'd need to prove past the semantics of the effect monad (STM, threads, whatever), and that also requires much more than simple equality (TLA+ and Esterel use temoporal logic, which is awesome, and I think Coq et al. use dependent types to encode modal logic, but I don't know how it's done or whether that's the approach). Haskell's logic is only marginally helpful in these scenarios and I don't know if translating from TLA+ to Java is harder or more error-prone than translating to Haskell, and even if it were, the difference (again, conjecture and gut feeling) seems to be marginal to offset the many other benefits of using Java. There are some interesting uses of Haskell's logic, such as session types (also possible in Java, BTW), but they are too underpowered to prove any distributed algorithm of interest (AFAICT, they are exactly as powerful as regular expressions). What bothers me most about Haskell's approach -- and correct me if I'm wrong -- is that the strength of the type system is pretty much defined to be "anything that's inferrable by an extended HM algorithm", which means that the strength is arbitrarily chosen to match a "convenience point" arbitrarily defined to be "full program inference", rather than an analysis of what strength is needed, and then tweaking it to trade off some strength for convenience. So it is the features of a certain algorithm which determines the language's semantics rather than an analysis of what's helpful. Good examples of the latter approach would be Java, Erlang and Clojure. (BTW, a good explanation of Java's design decision is in the first 17 minutes or so of this talk: https://www.youtube.com/watch?v=Dq2WQuWVrgQ https://www.youtube.com/watch?v=Dq2WQuWVrgQ) That is somehow (if you squint) similar to Prolog, whose utility was determined by the quality of it search algorithms. Such approach makes for great research, but its industrial applicability is very brittle. > Haskell is a significantly better language than Java ... Precisely because I can reason about Haskell programs by just evaluating Haskell by hand, whereas doing the same in Java would require me to constantly translate back and forth between Java and an external logic. Even if I were to accept that premise, that only shows Haskell is better in some aspects (which I gladly acknowledge; Haskell is awesome![1]). A programming language is much more than that. In fact, I believe extra-linguistic features of the runtime -- e.g. GC, threading, performance, monitorability, hackability, profilability -- are a much bigger contributors to productivity (and cost) than syntax-level abstractions. But again, I have no proof, but some (strong) evidence (namely, the incredible productivity gain when the industry switched from C/C++ to Java -- which are intentionally syntactically similar but with drastic extra-linguistic changes -- and the difficulty achieving similar gains by other JVM languages (different syntax, same-or-similar extra-linguistic features). EDIT: Also, you kind of describe reduction as "just" substitution, but if Mr. Church has taught us anything it is that "just substitution" is computation, and is as powerful (well, not quite, but in some respects) as a Turing machine. So there's no reason to assume that "just substituting" is any easier for a human than simulating state, be it in the mind, on a piece of paper or in a debugger (or, better yet, one of Java's awesome time-travelling debuggers). I tend to think (without proof) that the human mind is actually better suited to state simulation than to substitution (we simulate stuff all the time; lambda substitution is a very mathematical concept). To make this more concrete, recursion is limited assignment, and recursion combined with a continuation (or, in Haskell, a continuation monad) is imperative assignment (imperative state can be fully implemented in a pure language with continuations and recursion). So substituting across the cont monads is directly more complicated (computationally -- it requires lots of reductions) than state simulation of the very same computation. [1]: But, forgive me, so is Java.

tel 11y ago
Many things I could respond to, but out of convenience I'll just note that there's a reason why nobody programs in Haskell in the Cont monad unless they really can't avoid it!
- pron 11y ago
  Sure, just as there are reasons people write simple pure functions in Java when that's the best approach, and they generally try to keep things simple and tractable. Obviously, there's plenty of terrible Java code out there, but there would be plenty of terrible Haskell code out there too if Haskell had similar levels of usage. In any case, I was responding to the general statement that Haskell's purity makes reasoning easy by mere virtue of being pure. Well, LC is pure and it can be just as messy as Turing machines. Haskell code -- like Java, C, and Python code -- is simple to reason about when it is written with care (yes, I know that there are differences, but as a general rule). Now, don't get me wrong: I'm all for Clojure-style, ML-style or Rust-style immutability-by-default (each, of course, is different as they all have different tradeoffs), but that's completely separate from purity.
  - tel 11y ago
    That's one nice thing provable in Haskell's type/effect system, though, that the ambient effects available are no stronger than X for various descriptions of X. I know you dislike that whole regime, but it at least in this specific case explicitly circumscribes situations where, e.g., Cont is too strong.
catnaroek 11y ago
> I'm sorry, but that's just not true, or, more precisely, it's not necessarily doable in practice. For one, there's bounded recursion which may not be so easy to substitute, and that recursion interacts with equality to yield much richer properties. In those cases, one possible strategy is to take a detour via auxiliary data types, which aren't declared in the program, but are isomorphic to types that do. For example, lately I've been working quite a lot with data structures based on skew-binomial numbers (zippers, lenses and traversals for skew-binomial trees and heaps). Their usual implementation is as linked lists of increasingly weighted trees, except for the first two ones, which may have the same weight. In my proofs, however, I work with an isomorphic type with two constructors: one for the case where the weights are all strictly increasing, another for the case where the first two trees have equal weights. This is no different from performing mathematical induction on Peano naturals, but using machine integers or big integers for actually performing arithmetic operations. > Second, most interesting algorithms make use of time and state, so you'd need to prove past the semantics of the effect monad (STM, threads, whatever), and that also requires much more than simple equality (TLA+ and Esterel use temoporal logic, which is awesome, and I think Coq et al. use dependent types to encode modal logic, but I don't know how it's done or whether that's the approach). Most algorithms that interest me are data transformations - some sequential, some parallel, but almost never concurrent. And, even in those few cases where the interleaving of concurrent computations actually matters to me (e.g., implementing serializable transaction support in a RDBMS that works for any valid schema), I highly doubt that the tools you mention have anything useful to offer, although I would love to be wrong here. > Haskell's logic is only marginally helpful in these scenarios and I don't know if translating from TLA+ to Java is harder or more error-prone than translating to Haskell and even if it were, the difference (again, conjecture and gut feeling) seems to be marginal to offset the many other benefits of using Java. For things like protocol verification, I'll take a substructural type system, like those of Rust and ATS, where non-forgeable, non-duplicable tokens are used to reify the states and transitions concurrent computations may undergo. This still offers an easier, more integrated workflow than translating between two different languages. > What bothers me most about Haskell's approach -- and correct me if I'm wrong -- is that the strength of the type system is pretty much defined to be "anything that's inferrable by an extended HM algorithm", which means that the strength is arbitrarily chosen to match a "convenience point" arbitrarily defined to be "full program inference", rather than an analysis of what strength is needed, and then tweaking it to trade off some strength for convenience. My analysis of what strength is needed is very simple: If the computer can do something perfectly, let it do it. If the computer can't do it perfectly, I'll do it myself. I have no taste for automated mistakes that have to be manually rolled back, such as program analyses whose results I can't fully trust. HM-style (or, more generally, ML^F-style) type reconstruction just happens to be something that a computer can do perfectly. > Even if I were to accept that premise, [that equational reasoning about Haskell programs is just normal Haskell term reduction] What part is hard to accept? > that only shows Haskell is better in some aspects (which I gladly acknowledge; Haskell is awesome![1]). Yep, only some aspects. Exactly the ones I happen to need to write correct programs - and prove them so. > A programming language is much more than that. In fact, I believe extra-linguistic features of the runtime -- e.g. GC, threading, performance, monitorability, hackability, profilability -- are a much bigger contributors to productivity (and cost) than syntax-level abstractions. Perhaps I'm just too noob, but I'm really happy that I don't need to care about tuning the behavior of a managed language's runtime system. It's too much of a black art for me to want to have anything to do with it. If performance ever becomes that much of a problem, I'll just call Rust or C++. > But again, I have no proof, but some (strong) evidence (namely, the incredible productivity gain when the industry switched from C/C++ to Java -- which are intentionally syntactically similar but with drastic extra-linguistic changes -- and the difficulty achieving similar gains by other JVM languages (different syntax, same-or-similar extra-linguistic features). I find my productivity when using Java even lower than when using C++, which is a really impressive achievement, considering that C++ is such an unproductive language. C++ supports (to a limited extent) and encourages (to an even more limited extent) a programming style where variables actually stand for legitimate values inhabiting your problem domain (varying between assignments or member function calls, of course). These values can be manipulated using equational reasoning. In Java, every non-primitively-typed variable stands for an object reference, which is effectively a reification of the time and circumstances in which the object was created, and most certainly not something I care about. So, when it comes to actually producing proofs of correctness of Java programs, I need to jump this additional layer of indirection between variables and the values I care about. Back and forth. Over and over. > Also, you kind of describe reduction as "just" substitution, but if Mr. Church has taught us anything it is that "just substitution" is computation, and is as powerful (well, not quite, but in some respects) as a Turing machine. Of course term rewriting is computation - if it weren't, it would be useless as a theoretical basis for programming languages! But «equivalent in raw power» doesn't imply «equally convenient to use». Models of computation based on term rewriting happen to be easy to reason about in a compartmentalized, divide-and-conquer manner than Turing machines. > So there's no reason to assume that "just substituting" is any easier for a human than simulating state, be it in the mind, on a piece of paper or in a debugger (or, better yet, one of Java's awesome time-travelling debuggers). I've burned way too much time in debugger sessions that could've been usefully spent doing anything else, like writing programs that don't need to be debugged, or simply enjoying life. I don't think the value I got from them justifies the cost of opportunity. Never did a debugger session give me full confidence that the program I've written is correct. Even worse, debugger sessions seldom told me where exactly my program (as in, the code, not the running process) is wrong. > I tend to think (without proof) that the human mind is actually better suited to state simulation than to substitution (we simulate stuff all the time; Speak for yourself. > lambda substitution is a very mathematical concept). What do you mean by «lambda substitution»? A bound variable (by any binder, such as lambda, mu, forall and exists) cannot be substituted - you need to extract the term under the binder first. If you mean «variable substitution», yes, of course it's a mathematical concept.