3 ms·

Isn't that a bit like saying that it "can outperform equivalent assembly"? No; as shown in the link, this work allows idiomatic Haskell to outperform idiomatic

Isn't that a bit like saying that it "can outperform equivalent assembly"? No; as shown in the link, this work allows idiomatic Haskell to outperform idiomatic C. Obviously it's possible to write C which is a direct translation of the generated assembly, but such code would be nearly unmaintainable, and certainly very difficult to reason about. And why can you not prove the equivalent C correct? Proving the correctness of C code is possible, but (in my experience) significantly more difficult than for Haskell. After all, you're doing that proof by hand either way. A Haskell compiler will only help you prove that your program is well-typed. If you're mutating buffers then you're in a monad like IO or ST and the the compiler will throw it's hands up and tell you that correctness is entirely your problem. I don't mean that the compiler will automatically generate a proof for me, but that authoring a proof will be possible in practice -- as opposed to C, where it's possible in theory but nobody actually can. I'm a bit confused about why you think operating within a monad causes problems for proving correctness; to my knowledge, verifying code which uses monads is no more difficult than code using any other data types.

jrockway 17y ago
as shown in the link, this work allows idiomatic Haskell to outperform idiomatic C Interesting that you mention this. I know when I am writing C, I usually "malloc" dynamic data structures, whereas in Haskell, I usually "alloca" dynamic data structures (when talking to C libraries, obviously). Same end result, but alloca is actually faster, which makes allocation-heavy libraries faster when used from Haskell. (I guess I should use alloca in C, too. But I've never seen this anywhere.) I noticed that this was especially helpful in a library I recently used that never allocated any of its own memory; it was always the responsibility of the caller. Haskell idioms worked much better than C idioms here. I'm a bit confused about why you think operating within a monad causes problems for proving correctness; to my knowledge, verifying code which uses monads is no more difficult than code using any other data types. Wait, are you saying that calling a function called "(>>=)" is no different than calling any other function? Shocking. :)

jrockway 17y ago

as shown in the link, this work allows idiomatic Haskell to outperform idiomatic C Interesting that you mention this. I know when I am writing C, I usually "malloc" dynamic data structures, whereas in Haskell, I usually "alloca" dynamic data structures (when talking to C libraries, obviously). Same end result, but alloca is actually faster, which makes allocation-heavy libraries faster when used from Haskell. (I guess I should use alloca in C, too. But I've never seen this anywhere.) I noticed that this was especially helpful in a library I recently used that never allocated any of its own memory; it was always the responsibility of the caller. Haskell idioms worked much better than C idioms here. I'm a bit confused about why you think operating within a monad causes problems for proving correctness; to my knowledge, verifying code which uses monads is no more difficult than code using any other data types. Wait, are you saying that calling a function called "(>>=)" is no different than calling any other function? Shocking. :)