[Haskell-cafe] question about "singletons"

[TP]

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