Ashley Yakeley wrote:
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.
Worse than that, if bottom is a value, then Hask is not a category! Note that while undefined is bottom, (id . undefined) and (undefined . id) are not. That's a fuzzy lens... -- Ashley Yakeley