3 ms·

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.

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
    GHCi defaults to numerical operations on Int by default, so we have to specify what type we would like. Before you convince yourself that that's an obvious loss for Haskell bear in mind that you have to specify the type at only one single place in your whole program and it will propagate everywhere else, even if your program is 10m lines. Prelude> add_ x y = x + y + 1 Prelude> add_ <$> readLn <*> readLn :: IO Float 3 40.1 44.1
    - wellpast 9y ago
      But this is the point. My Clojure program is valuable/effective/per-spec without the type burden. So the type burden has slowed my delivery. And that "one single place" is for this trivial toy program. Now imagine the impedance across the delivery of a real business app.
      - danwilsonthomas 9y ago
        I was thinking about this sentiment: And that "one single place" is for this trivial toy program. Now imagine the impedance across the delivery of a real business app. That seemed very incongruous with my experience. I think the problem is that in my experience the number of types necessary scales sub-linearly with the amount of code. This is because Haskell (and other languages with what one might consider pleasant type systems) generally have full type inference. So while you might need the explicit type for the toy example, scaling that example up means only a handful, and possibly a net negative, other necessary explicit types. This comes up in a concrete manner in your example. The add function is almost too small to be typed appropriately. There isn't enough information for GHC to constrain the choice of numeric representation so it picks one. If you were to embed that in a larger program with more specific operators no types are necessary. Prelude> let add = (+) <$> readLn <*> readLn Prelude> let foo = (/) <$> add <*> add Prelude> foo 3 30.1 40 10.2 0.6593625498007968 So it's quite possible that the "type burden" becomes smaller as your system grows.
        tome 9y ago
        Really nice observation! Thanks.

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
  GHCi defaults to numerical operations on Int by default, so we have to specify what type we would like. Before you convince yourself that that's an obvious loss for Haskell bear in mind that you have to specify the type at only one single place in your whole program and it will propagate everywhere else, even if your program is 10m lines. Prelude> add_ x y = x + y + 1 Prelude> add_ <$> readLn <*> readLn :: IO Float 3 40.1 44.1
  - wellpast 9y ago
    But this is the point. My Clojure program is valuable/effective/per-spec without the type burden. So the type burden has slowed my delivery. And that "one single place" is for this trivial toy program. Now imagine the impedance across the delivery of a real business app.
    - danwilsonthomas 9y ago
      I was thinking about this sentiment: And that "one single place" is for this trivial toy program. Now imagine the impedance across the delivery of a real business app. That seemed very incongruous with my experience. I think the problem is that in my experience the number of types necessary scales sub-linearly with the amount of code. This is because Haskell (and other languages with what one might consider pleasant type systems) generally have full type inference. So while you might need the explicit type for the toy example, scaling that example up means only a handful, and possibly a net negative, other necessary explicit types. This comes up in a concrete manner in your example. The add function is almost too small to be typed appropriately. There isn't enough information for GHC to constrain the choice of numeric representation so it picks one. If you were to embed that in a larger program with more specific operators no types are necessary. Prelude> let add = (+) <$> readLn <*> readLn Prelude> let foo = (/) <$> add <*> add Prelude> foo 3 30.1 40 10.2 0.6593625498007968 So it's quite possible that the "type burden" becomes smaller as your system grows.
      - tome 9y ago
        Really nice observation! Thanks.