On Sun, Jun 27, 2010 at 6:45 PM, Max Bolingbroke wrote: On 27 June 2010 22:20, Edward Kmett I've pointed out the Codensity Set monad on the Haskell channel. I spend no time on #haskell but clearly I should :) It is an
interesting novelty, but it unfortunately has somewhat funny semantics in
that the intermediate sets that you obtain are based on what you would
get
if you reparenthesized all of your binds and associating them to the
right. But by the monad laws this is a totally fine thing to do, so this
shouldn't lead to any unfortunate behaviour in practice, I hope. Actually the resulting behavior _is_ rather unfortunate because it never
collapses the contained values until you go through the 'normalization by
evaluation' phase and lower it back down. So even even if you only generate
2 elements at each step, (which are already present in the set!), and run
the calculation for 100 operations or so you can take longer that the life
expectancy of the universe to terminate. ;)
Can you cast any light on the connection with NBE? It seems like a deep and powerful connection, so I'm sure it must correspond to some
interesting categorical principal. You're looking at initial objects in various categories, effectively these
are given rise to by colimits, and as initial objects, there exist morphisms
from them to all other objects in their respective categories. The trick is
learning to see the category you're asking for in the right terms.
For instance Mendler-style catamorphisms, can serve as the "mother of all
folds"
type MendlerAlgebra f c = forall a. (a -> c) -> f a -> c
mcata :: MendlerAlgebra f c -> Mu f -> c
mcata phi = phi (mcata phi) . outF
http://knol.google.com/k/catamorphisms#
and like many of these constructs in Haskell, is built around a Kan
extension (or in this case, you can see it more directly as the
contravariant Yoneda lemma in negative position).
-Edward Kmett