Comment by Nokinside | Hacker News Reader

Comment by Nokinside | Hacker News Reader

As a someone who don't use Haskell: Pandoc and Detexify.

As someone who has written safety critical software where you are willing to pay big buck for verification tools and software, Haskell has done nothing. I would love to use Haskell type FP but people who work with Haskell are thinking about correctness abstractly and real world (and earning lots of money) is not their priority.

All talk about correctness, absence of runtime errors are futile when you limit your definition to errors you want to deal with and ingonre the rest.

Having sound type system means nothing if you can have runtime memory errors, can run out of stack, pause for GC too long, don't know how much memory you may use in the worst case, can't detect divisions by 0, or float/fixexd point range errors ... etc.

Writing MISRA C and using verification tools like Astree, or SPARK + verification tools are not as elegant, but their weakest point is stronger than Haskell's.

If I sound salty, it's not because I think FP is bad idea, it's because I think the potential is wasted.

For your world, I think FP is a bad idea. GC is a bad idea. (Allocations after startup are a bad idea, too, and a language that allocates without being asked is a terrible idea.) Recursion is a bad idea. (Yes, tail-call-optimization can essentially turn it into recursion. Mis-write one TCO in the whole program, though, and your stack just became extremely unpredictable.) And considering Haskell specifically, in your world lazy is a terrible idea.

FP is a tool. It has potential to solve some problems. That potential won't be wasted, but the problems it will solve aren't the problems you have in your world.

On the other hand, FP could be just fine for writing the tools that will help you in your world.

> Recursion is a bad idea

Raw recursion or recursion using recursive schemes?

Any recursion. The problem is that, without tail call optimization, you create one stack frame per recursion. In Nokinside's world, you have to prove that you will never exceed the stack size. To prove that, you have to prove an upper bound on the number of recursion calls, and multiply by the size of a call's stack frame. Proving it for iteration is much easier, partly because (under the MISRA C rules or similar) iterations must have fixed bounds, but mostly because you don't create a stack frame for each iteration.

My turn: What's a recursive scheme?

FP is good idea for safety critical systems. It just has to be designed differently.

You want uniqueness typing that allows you to have functions that modify the variables without breaking the functional abstraction in straight forward manner. You could also reason about the memory use and have fixed amount of memory. Ordered typing would be nice feature to have. You also want hooks in the compiler for a additional tools for static analysis and proof assistants.

Recursion itself is not bad idea. It's strictly forbidden in safety critical code today for reasons that can go away. If you allow recursion, compiler must be able to reason and define the limits. Recursion is not good idea in safety critical code when it obfuscates the execution, but that is not always the case.

If I understood what you said correctly, you could have FP that allowed (controlled) mutation of the existing variable rather than allocating a new one. I suppose that could be done. But it seems to me that many people regard immutability as an essential part of FP, because without immutability, composability is no longer guaranteed. So to get what you'd like FP to be, you may have to step outside the existing FP community.

The essential part of what makes FP FP is referential transparency not immutability. Having referential transparency with mutation is what the uniqueness typing provides.

> Writing MISRA C and using verification tools like Astree, or SPARK + verification tools are not as elegant, but their weakest point is stronger than Haskell's.

That's why we need more Haskell-hosted system programming DSLs - with fancy sound types, proofs, extraction and stuff.

Reply on news.ycombinator.com