On 27 June 2010 22:20, Edward Kmett <
ekmett@gmail.com> wrote:
> I've pointed out the Codensity Set monad on the Haskell channel.
> 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
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