Jason (jcreed) wrote,
Jason
jcreed

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.
Tags: conference
Subscribe
  • Post a new comment

    Error

    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded 

  • 7 comments