An Apologia of Lazy Evaluation

Re:An Apologia of Lazy Evaluation by throwaway81523 on Sunday March 26, 2023 @04:41AM (#35312398)

I would say in an exaggerated version of the Haskell mindset, the most important thing is to prevent the program from giving wrong answers. The archetypal Haskell program is a compiler, and having it generate wrong code that gets deployed on a space mission is disastrous. Having the compiler crash with a memory leak is merely an annoyance. You would not write realtime code in idiomatic Haskell, if you would write such code in Haskell at all.

[ Parent | on HN ]

Re:An Apologia of Lazy Evaluation by murdoze on Sunday March 26, 2023 @10:15AM (#35314676)

Real-time code has high requirements for correctness and execution deadlines.

Which means, w/o deterministic execution Haskell not suitable for a whole niche, where its safety properties are in a high demand. Which is a pity.

[ Parent | on HN ]

Re:An Apologia of Lazy Evaluation by hexane360 on Sunday March 26, 2023 @11:59AM (#35315902)

Sure, but currently almost all of the most popular languages are also not suitable for that niche.

If you exclude any garbage-collected language, you're basically left with Ada, C, C++, some of the "C/C++ successors" (Zig, D, Carbon, maybe Nim), and Rust.

[ Parent | on HN ]

Re:An Apologia of Lazy Evaluation by throwaway81523 on Sunday March 26, 2023 @02:45PM (#35317946)

That's fine, those applications are why Ada was invented. Languages get pulled in too many directions when they try to be everything to everyone.

[ Parent | on HN ]

Re:An Apologia of Lazy Evaluation by ummonk on Sunday March 26, 2023 @03:30PM (#35318569)

"OOM exception" is a wrong answer. If your code terminates on a space mission because lazy evaluation runs out of memory, it's disastrous.

[ Parent | on HN ]

Re:An Apologia of Lazy Evaluation by throwaway81523 on Sunday March 26, 2023 @04:48PM (#35319424)

The code on the space mission wouldn't use Haskell or lazy evaluation. It would be written in something like Ada. In this picture, the Ada compiler would be written in Haskell. If the Ada compiler crashes with OOM, there is a disruption while you fix the leak, or run on a bigger machine as a stopgap. But if the output code crashes, that can ruin the space mission.

So the main concern is that if the compiler doesn't crash, the generated code should be correct. Haskell's type system helps you write compilers that don't generate wrong code.

As an even more extreme example, look at CompCert (compcert.inria.fr), which is a C compiler written in Coq. You can think of Coq as a dependently typed dialect of ML. For much of the backend, there are formal proofs that the output assembly code does the same thing as the input C code. The compiler is guaranteed to be free of a wide class of code generation bugs. But, AFAIK it is not guaranteed to be free of memory leaks or other crashes. Its reliability in that regard is just like any other software that has passed a reasonable amount of testing and has worked ok in production.

[ Parent | on HN ]