3 ms·

Static types represent proofs, depending on the language they may be very weak proofs, but nevertheless, that's what they are for. I see nothing wrong with that

Static types represent proofs, depending on the language they may be very weak proofs, but nevertheless, that's what they are for. I see nothing wrong with that statement. Another way of putting it is "the compiler verifies your proofs"

tome 9y ago
Indeed, by the Curry-Howard isomorphism they are (isomorphic to) proofs. This fact is held in high regard by some in the Haskell community. But the sense in which Clojurists mean it seems to be quite different. You have to prove things to the type checker which they seem to view as some sort of authority watching over you that you must please.
- bitwalker 9y ago
  Yeah, there does seem to be an undertone of "it's such a pain to have to prove things to the compiler that I know are right", even though the vast majority of the time the compiler is right and you messed up. I never quite understand the feeling that one wants to pin the blame on the compiler when you make a mistake and get that feedback right away. I guess in some cases, like Rust, where the compiler is really particular about enforcing certain rules, that might be frustrating, but one reaches for a tool like Rust because of those rules and the guarantees they provide, so it's kind of silly.
- wellpast 9y ago
  Here is a Clojure program: (defn add [x y] (+ x y)) (add (read-string) (read-string)) Clojure doesn't compile, so I can run this program just as it is. In Haskell, this isn't sufficient. I have to say something about types, and I have to compile first. That is what is meant by I have to "prove". In at least this toy example, one of these workflows is orders of magnitude more work than the other. Now what happens in that Clojure program if I enter junk inputs when I am prompted? Well, I get an Exception, or I get NaN, or junk. But you know what? I don't care. For this particular example, my product manager doesn't care. When he cares, I'll go add in some dynamic verification. The point is, my business priorities are my choice, not some academic proof system's. I like verification, though, so I can go add it in a la carte, i.e. per my discretion.
  - tome 9y ago
    Prelude> add <$> readLn <*> readLn 3 40 43 This is in GHCi so it also doesn't "compile". It does "type check", but "prove" is not a good synonym for "type check" just like it's not a good synonym for "parse". > one of these workflows is orders of magnitude more work than the other. "Order of magnitude" generally means "factor of ten". Are you really claiming that the Haskell code is at least one hundred times more work than what you wrote? I have a question about "read-string". What sorts of objects can it return? Base numeric types I guess, plus atoms, and recursively, lists of the above. Anything else?
    - wellpast 9y ago
      Okay, before I say 'you win', can you show me this in Haskell: ; -- the program -- (defn add* [x y] (+ x y 1)) (add* (read) (read)) ; -- repl demo -- 3 40.1 44.1
      - wellpast 9y ago
        I'm going to assume that if you take 10 times longer to respond to this than it took me to respond to you, then my "orders of magnitude" claim has been proven. (...friendly joke, of course.)
        tome 9y ago
        If using Clojure means that one no longer needs sleep then I concede immediately.
      - danwilsonthomas 9y ago
        I tried this, because my first thought was that this was much the same as the first example. Certainly Haskell doesn't have a variadic addition function by default but I don't think that's the biggest concern here (variadic addition is easily just summing a list). The surprising thing was entering both an "integer" and a float to be read. You certainly can parse floats from input, but this: `(+) <$> readLn <*> readLn` doesn't do it, even though at first glance it seems like it should. If you wanted to handle fractional values, you would have to hint to the type checker that you wanted to do so. I do think that this example is perhaps too specific, and highlights only the specific topic of dynamic number conversion which is, depending on the situation, both blessed and cursed. I will concede though that if you want dynamic number conversion Haskell isn't going to give you that easily.

tome 9y ago

Indeed, by the Curry-Howard isomorphism they are (isomorphic to) proofs. This fact is held in high regard by some in the Haskell community. But the sense in which Clojurists mean it seems to be quite different. You have to prove things to the type checker which they seem to view as some sort of authority watching over you that you must please.

bitwalker 9y ago
Yeah, there does seem to be an undertone of "it's such a pain to have to prove things to the compiler that I know are right", even though the vast majority of the time the compiler is right and you messed up. I never quite understand the feeling that one wants to pin the blame on the compiler when you make a mistake and get that feedback right away. I guess in some cases, like Rust, where the compiler is really particular about enforcing certain rules, that might be frustrating, but one reaches for a tool like Rust because of those rules and the guarantees they provide, so it's kind of silly.
wellpast 9y ago
Here is a Clojure program: (defn add [x y] (+ x y)) (add (read-string) (read-string)) Clojure doesn't compile, so I can run this program just as it is. In Haskell, this isn't sufficient. I have to say something about types, and I have to compile first. That is what is meant by I have to "prove". In at least this toy example, one of these workflows is orders of magnitude more work than the other. Now what happens in that Clojure program if I enter junk inputs when I am prompted? Well, I get an Exception, or I get NaN, or junk. But you know what? I don't care. For this particular example, my product manager doesn't care. When he cares, I'll go add in some dynamic verification. The point is, my business priorities are my choice, not some academic proof system's. I like verification, though, so I can go add it in a la carte, i.e. per my discretion.
- tome 9y ago
  Prelude> add <$> readLn <*> readLn 3 40 43 This is in GHCi so it also doesn't "compile". It does "type check", but "prove" is not a good synonym for "type check" just like it's not a good synonym for "parse". > one of these workflows is orders of magnitude more work than the other. "Order of magnitude" generally means "factor of ten". Are you really claiming that the Haskell code is at least one hundred times more work than what you wrote? I have a question about "read-string". What sorts of objects can it return? Base numeric types I guess, plus atoms, and recursively, lists of the above. Anything else?
  - wellpast 9y ago
    Okay, before I say 'you win', can you show me this in Haskell: ; -- the program -- (defn add* [x y] (+ x y 1)) (add* (read) (read)) ; -- repl demo -- 3 40.1 44.1
    - wellpast 9y ago
      I'm going to assume that if you take 10 times longer to respond to this than it took me to respond to you, then my "orders of magnitude" claim has been proven. (...friendly joke, of course.)
      - tome 9y ago
        If using Clojure means that one no longer needs sleep then I concede immediately.
    - danwilsonthomas 9y ago
      I tried this, because my first thought was that this was much the same as the first example. Certainly Haskell doesn't have a variadic addition function by default but I don't think that's the biggest concern here (variadic addition is easily just summing a list). The surprising thing was entering both an "integer" and a float to be read. You certainly can parse floats from input, but this: `(+) <$> readLn <*> readLn` doesn't do it, even though at first glance it seems like it should. If you wanted to handle fractional values, you would have to hint to the type checker that you wanted to do so. I do think that this example is perhaps too specific, and highlights only the specific topic of dynamic number conversion which is, depending on the situation, both blessed and cursed. I will concede though that if you want dynamic number conversion Haskell isn't going to give you that easily.