[jstimpfle]

Yes. Most Haskellers will sneer at it, while personally I think it's the right thing to do because it conveys the programmer's ideas about invariants. But syntactically an explicit unwrapping function is still a lot of noise. Simple null pointers as we have in C, with an unmapped segment at address zero so that it throws a segmentation fault, are much better.

[cultus]

Replying to your lower comment (the coffee has kicked in):

The situation you describe is one where a null really is an unrecoverable error, and the program should terminate. That is the one case where it makes sense to just let a NPE happen.

However, the vast majority of time, a null is just an absence of value, and does not signify an unrecoverable error. Those are the kind of situations that an Option/Maybe helps with, since it doesn't let you forget to handle the null case.

Even if a null value returned from a function is abnormal, and the program shouldn't continue, an Option is still going to be better most of the time. After all, you probably have connections and stuff you want to cleanly terminate before shutting the program down.

[cultus]

I haven't drank all my coffee yet this morning, but are you saying that throwing a segfault can be a good thing?

Either you unwrap the Option, or you have to remember to do an manual null check. The second option is more verbose.

[jstimpfle]

> but are you saying that throwing a segfault can be a good thing?

Sure, what's bad about it? A logic bug was detected, so the program should be terminated. Or how do you intend to continue?

Segfault is not so different from what happens if you do "fromJust Nothing" in Haskell or get a NullPointerException in Java. You can even write a handler for the segfault, but I guess that's rarely a good idea.

[lmm]

> Sure, what's bad about it? A logic bug was detected, so the program should be terminated. Or how do you intend to continue?

I intend to not have the logic bug in the first place, by encoding my invariants in the type system.

If you "know" that the value is present rather than absent, you must have a reason for knowing it, so explain that reason to the compiler. E.g. maybe you took the first element of a list value that you know is non-empty - so maybe you need to change the type of that value to a non-empty list type. That way the compiler can check your reasoning for you, and will catch the cases where you thought you "knew" but were actually wrong.

[jstimpfle]

> by encoding my invariants in the type system

the way I program that is nothing but a pipe dream.

> If you "know" that the value is present rather than absent, you must have a reason for knowing it, so explain that reason to the compiler.

I might know that it exists for example because it is computed in a post-processing step after a first stage but before a second stage. So it exists in the second stage but not in the first. Relying on global data (which I won't give up) makes it practically impossible to encode that the data is not there in the first stage.

And that's not a problem at all. I simply don't access that data table in the first stage... Trying to explain my processing strategy to a compiler would amount to headaches and no benefits.

[lmm]

> I might know that it exists for example because it is computed in a post-processing step after a first stage but before a second stage. So it exists in the second stage but not in the first.

So the first stage could create a handle to it, or even just a phantom "witness" that you treat as proof that the value is present.

> And that's not a problem at all. I simply don't access that data table in the first stage... Trying to explain my processing strategy to a compiler would amount to headaches and no benefits.

Shrug. I found that errors would make it into production, because human vigilance is always fallible. And the level of testing that I needed to adopt to catch errors was a lot more effort than using a type system.

[jstimpfle]

Accesses to unallocated global data is the type of errors that you typically hit on the first test run. Another example would be function pointers loaded from DLLs.

I don't think type systems help all that much. Type + instead of -, and you're out of luck.