If you want to be able to return "pointer or null", any decent language will let you do that, sure. But it's good to have the option of saying "this function will never return null".

Think of it this way: functions should document whether (and under what conditions) they return null, right? What if the compiler could check the accuracy of that documentation, so it would be an error to return null from a function that said it didn't return null, and a warning to document a function as possibly-returning-null when it never did? (And once you had that, surely you'd want a warning when you accessed a possibly-null thing without checking whether it was actually null?)

So basically you want the compiler to solve the halting problem for every function it compiles.

Ideally yes. But keeping track of nullability is not impossible, it's not even hard, as any number of existing languages with such checking prove (some of which have very performant compilers).

With a Maybe/Option type, you are forced to always deal with the possibility of Nothing/None.

And even better, you can use monadic bind to chain together several actions on possibly-nullable things and get either a value or a null at the end.

An argument can be made that this merely masks the problem : it is certainly possible for a Haskell function to crash (and therefore not return anything), no matter it's declared type :

reallyfun xs = reallyfun xs ++ [ 1 ]

Note that this will OOM, not just run infinitely long. There are plenty of ways you can cause this sorts of issues. So you can't trust Haskell functions to always return their declared type either.

The million-dollar-question : should your program be ready for this ? (in the case of a database : ideally, yes it should, and it's in fact possible to do just that)

That's the problem with abstractions, like the "always-correct-or-null" pointers of java : they're leaky. A type system, unless reduced to pointlessness, can't really be enforced fully. Haskell ignores failure modes, like memory and stack allocation, jumping to other parts of the program, reading the program, ... all of which can in fact fail.

Thinking about this gives one new appreciation for try ... except: (catching an unspecified exception). It's not necessarily worse than a pure function. Good luck defending that position to mathematicians though.

That misses the point, I think.

Of course functions can cause a program to crash, and there are all sorts of bad things that happen that cannot be caught at the language level; Haskell doesn't save you from memory corruption, for example.

But those things don't violate the language's guarantees about type correctness. A crashing program simply ceases to run; it's not like an Int-returning function can somehow crash and return a bogus Int value.

In this sense, Haskell is no different from languages like Java or Go. It's completely orthogonal to the null problem.

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

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

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.

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!

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.