On Mon, Mar 22, 2010 at 12:33 PM, Sjoerd Visscher <sjoerd@w3future.com> wrote:

Of course the are still a lot of things missing, especially in the details. And I'm a category theory beginner, so there will probably be some mistakes in there as well. F.e. Edward Kmett doesn't like () being the terminal object in Hask, which I thought I understood, but after thinking about it a bit more I don't.

I love the library. Don't get me wrong. =)

As for (), consider:

data Unit

unit :: Unit
unit = undefined

is ever so slightly more anally retentive about being a true terminal object.

There is only one canonical morphism from every object in Hask to Unit:

terminate :: a -> Unit
terminate = const unit

-- as long as you're ignoring 'seq'
terminateSeq :: a -> Unit
terminateSeq a = a `seq` unit

-- And of course with runtime exception catching you can distinguish a whole lot more and the category theoretic viewpoint becomes mostly useless. ;)

Regardless, continuing to ignore seq there are two morphisms of type a -> ().

terminate1 :: a -> ()
terminate1 _ = ()

terminate2 :: a -> ()
terminate2 _ = undefined

-- discounting the extraneous
terminateUnitSeq a = a `seq` undefined

So taking the definition of a terminal object being that there exists one canonical arrow to the object from every object in Hask, Unit seems to fit the bill.

This is as opposed to the pleasant fiction of an initial object:

data Void
-- or
newtype Void = Void Void
-- or
newtype Void = Void { void :: forall a. a }

which should have a morphism

Void -> a

for every type, but which should never be inhabited, but alas, bottom infects every type in Haskell, so ultimately each of these is Unit with an additional unsafe morphism.

If it could exist then Right undefined :: Either a Void should fail to typecheck and Either a Void -> a should be a total function. Welcome to Coq or Adga. ;)

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.

But in the sea of ideas that don't quite map onto Haskell, I can at least go out of my way to make sure that my terminal object is terminal. =)