[Haskell-beginners] Would you shed light on "undefined values" please?

[Ertugrul Soeylemez]

Brandon Allbery <allbery.b at gmail.com> wrote:

> 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/