4 ms·

insert x [] = [x] insert x (y:ys) = if x > y then y:(insert x ys) else x:y:ys insertSort xs = foldr insert [] xs Three lines of Haskell, fully statical

insert x [] = [x] insert x (y:ys) = if x > y then y:(insert x ys) else x:y:ys insertSort xs = foldr insert [] xs Three lines of Haskell, fully statically typed. Yes, Idris' proofs are verbose. They're also a perfect validation of the properties that need to be proven, better than any test case in the world.

yogthos 7y ago
Your version doesn't provide the same guarantees. It doesn't even guarantee that the same items are returned as the ones that were provided as arguments. So, you appear to be agreeing that relaxing static typing constraints results in code that's easier to understand. Unfortunately, Haskell type system can result in baroque code in many cases as well. The whole reason monads are so prevalent in Haskell is due to the fact that the type system tracks side effects. Here's an example of a problem this introduces from the core.async library. https://groups.google.com/forum/#!topic/clojure/wccacRJIXvg https://groups.google.com/forum/#!topic/clojure/wccacRJIXvg When I first wrote the core.async go macro I based it on the state monad. It seemed like a good idea; keep everything purely functional. However, over time I've realized that this actually introduces a lot of incidental complexity. And let me explain that thought. What are we concerned about when we use the state monad, we are shunning mutability. Where do the problems surface with mutability? Mostly around backtracking (getting old data or getting back to an old state), and concurrency. In the go macro transformation, I never need old state, and the transformer isn't concurrent. So what's the point? Recently I did an experiment that ripped out the state monad and replaced it with mutable lists and lots of atoms. The end result was code that was about 1/3rd the size of the original code, and much more readable. So more and more, I'm trying to see mutability through those eyes: I should reach for immutable data first, but if that makes the code less readable and harder to reason about, why am I using it? If Clojure had Haskell type system, the monad approach would be the only option resulting in code that's harder to reason about.

yogthos 7y ago

Your version doesn't provide the same guarantees. It doesn't even guarantee that the same items are returned as the ones that were provided as arguments. So, you appear to be agreeing that relaxing static typing constraints results in code that's easier to understand. Unfortunately, Haskell type system can result in baroque code in many cases as well. The whole reason monads are so prevalent in Haskell is due to the fact that the type system tracks side effects. Here's an example of a problem this introduces from the core.async library. https://groups.google.com/forum/#!topic/clojure/wccacRJIXvg https://groups.google.com/forum/#!topic/clojure/wccacRJIXvg When I first wrote the core.async go macro I based it on the state monad. It seemed like a good idea; keep everything purely functional. However, over time I've realized that this actually introduces a lot of incidental complexity. And let me explain that thought. What are we concerned about when we use the state monad, we are shunning mutability. Where do the problems surface with mutability? Mostly around backtracking (getting old data or getting back to an old state), and concurrency. In the go macro transformation, I never need old state, and the transformer isn't concurrent. So what's the point? Recently I did an experiment that ripped out the state monad and replaced it with mutable lists and lots of atoms. The end result was code that was about 1/3rd the size of the original code, and much more readable. So more and more, I'm trying to see mutability through those eyes: I should reach for immutable data first, but if that makes the code less readable and harder to reason about, why am I using it? If Clojure had Haskell type system, the monad approach would be the only option resulting in code that's harder to reason about.