January 22nd, 2010

beartato phd

(no subject)

I am still running on a significant sleep debt that I have not yet repaid, but Hot Liquid Sleep with Much Milk and Sugar is doing its job admirably.

Finally got the chance to talk to fancybred and neelk a ton today, which was nothing less than great. Neel has a talk coming up tomorrow about GUIs and monoidal closed categories that I'm looking forward to. Noam finally got through to me I think about his defunctionalization trick in Twelf, and made the useful suggestion of trying to include quotients as a way to build up new metric types --- I'm not sure I'm going to be able to accommodate them, but it's a nice idea. He also explained how the (constructively valid!) isomorphism between the "parametric double dual" ∀α.(A → α) → α and A is actually a special case of the Yoneda lemma in disguise, and he went further to talk about the more general isomorphism FA = ∀α.(A → α) → Fα which is the (not special-cased) Yoneda lemma in disguise, and the even more general isomorphism TA = ∀α.(A → Tα) → Tα, which works when T is a monad.