Brandon Allbery
The reason _|_ is significant is that a type that admits it as a value can be computed lazily. If your type does not allow for _|_ then it is strict;
That's actually not quite right. Strictness and bottom are only loosely related in that strictness is defined in terms of bottom. You get a concept of strictness once you have functions (value constructors with arguments are functions), otherwise it doesn't make much sense. They are related in that some expressions can yield defined values in nonstrict semantics, where they would give you bottom in strict ones, namely in this specific case: f ⊥ ≠ ⊥ In strict semantics this is impossible, because this is definitely a nonstrict function. Bottom arises, as soon as a language is total. This is related to the halting problem. Bottom is the value, which is never computed in the sense that it never results. Only nontotal languages (like Agda) can prevent bottom values from appearing. In other words, every type in Haskell is lifted and there is no way around that. The type of 'undefined' proves that. In fact you cannot express the undefined value in Agda. On the other hand in Haskell it's trivial to express: undefined :: a undefined = undefined Greets, Ertugrul -- nightmare = unsafePerformIO (getWrongWife >>= sex) http://ertes.de/