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

[Edward Kmett]

On Mon, Mar 22, 2010 at 12:33 PM, Sjoerd Visscher <sjoerd at 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. =)
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-cafe/attachments/20100326/a752ee66/attachment.html