[Haskell-cafe] question about "singletons"
paratribulations at free.fr
Sun Jun 2 12:58:27 CEST 2013
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
> 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.
More information about the Haskell-Cafe