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
data Nothing
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 "()".
--
Ashley Yakeley
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
