Lambda the Ultimate

In Java you can get NullReference exceptions, which are the same thing. You could go so far as to argue that Haskell _|_ are the same thing... (I wouldn't)

I personally don't think segfaults are particularly bad, but only because there is so much tooling around C/C++ that allows you to deconstruct a segfault and figure out the cause; it's gotten so far that there are tools to allow you to play back the execution and see exactly what led to the current state.

You can almost get a segmentation fault in OCaml, even compiled in safe mode and without Magic.Obj.

It involves weak references and non-exhaustive pattern-matching to achieve such a result, of course.

I'm suprised by this, Could you post a link describing where the unsoundness lies?

#let dereference (Some x) = x;;

Warning: this pattern-matching is not exhaustive.
Here is an example of a value that is not matched:
None

val dereference : 'a option -> 'a = <fun>

#dereference None;;

Exception: Match_failure ("", 1, 16).

...
String x = null;
System.err.println(x.charAt(0));
...

Java.lang.NullPointerException at ...

In particular, you can apply this to a weak reference

let weak_array = Weak.create 1;;

let some_value = "Some value";;
let _ = Weak.set weak_array 0 (Some some_value);;

(*Do something here to trigger garbage-collection*)

let x = dereference (Weak.get weak_array 0) in
 print_endline some_value;;

I claim that failing to check whether an option is Some x or None before calling dereference is (almost) the same thing as failing to check whether a pointer is null or a valid reference in, say, Java.

This probably stems from halting problem, right?

Then may be we need to address this problem first?

Well, I'll file a bug for the OCaml team right now: "Implement a type system/model checker which can solve the halting problem".

Anyway, those were just my two pedantic cents.

Just to clarify - I am not familiar with OCaml, and don't know, whether hitting a missing branch of case matching is like a NPE in Java, or a GPF in Windows. I just suspect it cannot be both.

It is very much like a NullPointerException in Java, as it raises an exception which can easily be caught. IMO, the main difference is that OCaml's compiler is smart enough to notice the fact that a pattern matching is non-exhaustive, even with complex patterns (it can be slightly overzealous at times, although I have never seen this happen outside of toy examples made on purpose to describe this overzealousness).

In addition, since completing a pattern-matching to make it exhaustive typically entails strictly no overhead and is often the matter of one short line of code, I'd say that there is no good reason to let this case of situations happen. However, since this is not a type error, just a compiler warning, you can get away with it.

In addition, since completing a pattern-matching to make it exhaustive typically entails strictly no overhead and is often the matter of one short line of code, I'd say that there is no good reason to let this case of situations happen.

The usual trick is to use isomorphism, and instead of a sum of values (defined/undefined) use a product of continuations (return/error).

I'm not sure I understand what you mean. If you're saying that exhaustive pattern-matching does not replace exceptions, I fully agree with you. If you're not, then I'll need your help to get my head around this.

I meant following: a single potentially empty list and a single continuation that expects a head of that list cannot be composed without obtaining external aid. In light of Curry-Howard, there just is no proof for such sequent (something like True or A or (A and A) or ... |- A). You either need an additional source of value (conjuncted with original LHS), or an alternative continuation (disjuncted with original RHS). Or you can change types of the original value or continuation - either persuade client to accept also an absence of the head (add "and True" to RHS), or persuade supplier to always supply non-empty list (remove "True or" from LHS). I prefer to reason about such problems in CPS, as it makes more clear distinction between a caller of the function and a receiver of its result, and also makes exception handling and its friends more explicit.

Well, I am affraid I do not command English well enough to compensate for lack of hand waving, anyway - I don't feel my clarification clarified anything :-(

Well, now, at least it is clear that I should read more about continuations before trying to understand your previous comment :)

I should read more about continuations before trying to understand your previous comment

Also, note that I am reading this stuff only by night, so I am not sure I understand it correctly :-)

In Java you can get NullReference exceptions, which are the same thing. You could go so far as to argue that Haskell _|_ are the same thing... (I wouldn't)

I'm glad we agree on the second point, but I want to quibble on the first.

A NullPointerException is well-defined outcome (computation) defined within the appropriate sphere of the program. It can't "escape into the wild" and damage its environment or require its environment to protect against the problem.

A seg fault on the other hand, is a problem that HAS escaped the bounds of the program and had to be caught in the OS or other environment; if the latter didn't do so, "bad things" would have happened.

To equate the two situations is to confound two very different sets of system guarantees; their observable behaviour from the host environment's point of view is completely unalike.

You have to admit that use of a processor's MMU (and OS's page fault mechanism) to trap null pointer dereference is a quite useful optimization. :)

A C/C++ implemention is permitted, of course, to explicitly trap all NULL pointer dereferences; one can also write a smart pointer class in C++ which acts just like a dumb pointer, but aborts or throws if dereferenced while NULL.

For all practical purposes, and on all modern platforms (excluding a few brain-dead embedded sytems platforms like vxWorks on PowerPC, grumble grumble I have to deal with this one at work grumble grumble), deferencing NULL has the implementation defined behavior of causing a processor exception, whether its called "segmentation violation" (Unix) or "general protection fault" (Windows).

Dereferencing INVALID pointers (those which are neither NULL nor point to a valid object of the indicated type) is another kettle of fish. :(

I don't see NullPointerException handling by the JVM as being any different than segfault detection by the OS. Why is the JVM anything other than a pseudo-OS? It provides an abstracted hardware environment in which a program can run.

While throwing a NullPointerException is a perfectly valid computation, the computation that led to the condition is not at all valid. A segfault merely reports the presence of an unrecoverable error state that the program has achieved. Anyone who tries to recover from a NullPointerException should be tarred, gzipped, and cp'ed to /dev/null. Therefore, the situations are really logically equivalent in my mind.
C/C++ just don't pretend to be pretty about the crash.