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 _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
