[Haskell-cafe] Re: ANN: data-category, restricted categories
ashley at semantic.org
Tue Mar 30 15:25:57 EDT 2010
Edward Kmett wrote:
> Of course, you can argue that we already look at products and coproducts
> through fuzzy lenses that don't see the extra bottom, and that it is
> close enough to view () as Unit and Unit as Void, or go so far as to
> unify Unit and Void, even though one is always inhabited and the other
> should never be.
The alternative is to use _consistently_ "fuzzy lenses" and not consider
bottom to be a value. I call this the "bottomless" interpretation. I
prefer it, because it's easier to reason about.
In the bottomless interpretation, laws for Functor, Monad etc. work.
Many widely-accepted instances of these classes fail these laws when
bottom is considered a value. Even reflexivity of Eq fails.
Bear in mind bottom includes non-termination. For instance:
x :: Integer
x = x + 1
n :: Nothing
n = seq x undefined
x is bottom, since calculation of it doesn't terminate, but one cannot
write a program even in IO to determine that x is bottom. And if Nothing
is inhabited with a value, does n have that value? Or does the
calculation to find which value n is not terminate, so n never gets a value?
I avoid explicit "undefined" in my programs, and also hopefully
non-termination. Then the bottomless interpretation becomes useful, for
instance, to consider Nothing as an initial object of Hask particularly
when using GADTs.
I also dislike "Void" for a type declared empty, since it reminds me of
the C/C++/C#/Java return type "void". In those languages, a function of
return type "void" may either terminate or not, exactly like Haskell's "()".
More information about the Haskell-Cafe