Thanks Richard, now I have my answers. Richard Eisenberg wrote:
- The type system of Haskell is based on theoretical work that resolutely assumes that types of non-* kind are uninhabited. While it is possible to stretch imagination to allow types like 'Zero to be inhabited, the designers of Haskell would have a lot of work to do to prove that the new language is actually type-safe. [...] Technically, yes, we could have a different definition of undefined, but it would fly in the face of a lot of theory about type-safe programming languages. This is not to say that such a thing is impossible, but just perhaps imprudent.
Ok, this is a convincing reason to admit that non-* kinded types must be uninhabited, even by undefined.
Bottom is inherently uninteresting, because you never see bottom in running code, and you can never know where bottom is lurking (other than after your program has crashed). [...] So, all of this is to say that undefined is entirely uninteresting, as your program can never know when it encounters one without dying.
Ok: Haskell refuses to show "undefined" for a type of kind * if it has not another inhabitant, because the type is deemed uninteresting.
Technically, bottom should have this definition (which is perfectly valid Haskell):
bottom :: a bottom = bottom
In other words, bottom is infinite recursion -- a term that never finishes evaluating. Let's say a show method tried to print its argument and its argument is bottom. Well, that method would have to examine its argument and would immediately fall into an infinite loop. Bottom is a little like Medusa when you have no mirrors around. Once you look at it, it's too late.
In Haskell, we don't usually use bottom in this way; we use undefined. undefined masquerades as bottom, but instead of forcing a running program into an infinite loop, looking at undefined causes a running program to instantly terminate. This is generally much nicer than an infinite loop, but this niceness is simply a convenience that the compiler gives us. From a theoretical point of view, a hung program is much cleaner. To recover the consistency of the theory, Haskell provides no way to recover from a discovery of undefined in a running program. (GHC has implemented an exception that allows exception-handling code, written in the IO monad, to catch a use of undefined, but I would be highly suspicious of code that used this feature.)
Interesting, I will remember that. Thanks TP