[Haskell-cafe] Re: ANN: data-category, restricted categories

[Ashley Yakeley]

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