Kan Extensions for Functional Programmers

October 28th, 2006 by Mauro Jaskelioff

Neil talked about his forthcoming book

Here is the summary:

Inductive types have a well understood theory in terms of initial algebra semantics on a category of types. When it comes to advanced types, like nested datatypes and GADTs, the key idea seems to be that types should be indexed but there is disagreement about what these indexes are.

In the functional world, the Haskell community has swallowed the “practical” benefits of GADTs where indexes are elements of $\star$, eg:

 $$Lam\colon \star \rightarrow \star$$
The theoretical advantages of using the dependently typed approach, where $Lam\colon \mathbb{N} \rightarrow \star, are seen as just “academic”. The semantics here is in terms of slice categories where the key constructions are reindexing, dependent sum & product.

Their equivalents in the functional world are functor composition and left and right Kan extensions. So all the practical Haskellers are buying into MacLane’s chapter X.

3 Responses to “Kan Extensions for Functional Programmers”

  1. Jon Says:

    I’ve put in an order for that book with amazon already – had to cancel my order of Graham’s book to pay for it!

  2. Sebastian Says:

    I’ve suggested it for acquisition to our local library – that might pop Graham’s book out of the queue.

  3. Graham Hutton Says:

    Don’t worry, I’ve ordered 15,000 copies of my book for the library anyway.

Leave a Reply