[waps]

This is the mathematician's argument. It boils down to the unfairness of having to execute programs on real hardware with real constraints. Well, that doesn't work in the real world obviously. Especially memory allocations WILL fail, so, frankly, deal with it. Haskell makes this impossible, and therefore throws real-world correctness out of the window because it makes mathematical correctness so much messier.

Your assertion that this can't be caught at the language level is wrong : checking malloc'ed pointers for NULLness will do it. In java, catch OOM exceptions. This error doesn't have to cause your programs to crash. Neither does an infinite loop ("easy" to catch in Java). Given more tools, you can write programs that are safe from some measure of memory corruption.

The real world is messy. Pretending it's not doesn't fix that, and nobody but mathematicians are surprised at all. End result is simple : your programs will crash after you've "proven" it can't crash. Running everything in "just-large-enough" VMs has massively exacerbated CPU and OOM error conditions, at least from where I'm sitting. I'd expect further cloud developments to make it worse.

So the type system only guarantees correctness if the following conditions hold, amongst other things:

1) infinite available memory (infinite in the sense that it is larger than any amount the program requests, haskell provides zero guarantees that limit memory usage, so ...)

2) infinite available time for program execution (again, for the normal definition of infinite)

3) no infinite loops anywhere in your program (more problematic in haskell because every haskell tutorial starts with "look, lazy programming means infinite loops terminate in special case X", and of course it only works in special cases)

Note that this is only the list of "hard" failures. There are factors that can blow up the minimum execution time of your program (e.g. VM thrashing, stupid disk access patterns) that I'm not even considering. In practice, these "soft" failures, if bad enough, cause failure of the program as well.

And only then do we get to the conditions that people keep claiming are the only conditions for haskell to work:

4) no hardware malfunctions

[jdmichal]

... And all this has what to do with having non-nullable references be the default, with a wrapping Option or Maybe type for otherwise?

[waps]

The point was that there is no real-word type system that can guarantee non-null pointers (not even Haskell's). You cannot do allocation reliably in the real world, and if your type system guarantees that, it is simply wrong.

[jdmichal]

You are arguing a useless point. Yes, in a real computer, memory can be randomly flipped by solar radiation and viola, your pointer is now actually NIL. Or any other various failure modes you've mentioned. The point being that those are failure modes, not normal operations. Once a system reaches a failure mode, nothing can be guaranteed, not even that it adds 1 and 1 correctly, because who's to say that the instructions you think you're writing are being written, read, and processed correctly? The only solution is to down the box, reset the hardware, and hope that whatever happened wasn't permanent damage.

My point being, you cannot invoke catastrophic system failure as an argument against a static-time type system and call it an argument, simply because that's an argument against any programming construct at all. Linked lists? But what if you can't allocate the next node... Better to not use them at all!

[waps]

You're trying to change the topic. I'm not talking about unreliable hardware. The two main things I contend WILL happen to production haskell programs are :

1) OOM (both kinds : stack and heap). 2) functions taking longer than the time they effectively have (ie. to prevent DOS conditions).

Both of these are guaranteed by the Haskell type system to never happen, and you will hit them in practice. (guaranteed may be the wrong word, maybe required would be better).

The C, or C++ type system does not guarantee allocation will succeed on the heap, and has deterministic results if it does fail, meaning you can react to that in a clean manner (and make sure it doesn't interfere with transactions, for example). With extra work you can guarantee the availability of stack space for critical methods too. Java guarantees both stack and heap allocation failures will result in deterministic progress through your program.

These are not serious enough to merit being called "catastrophic system failure". They are not. Don't tell me you haven't hit both these conditions in the last month.

That's all I'm saying.