September 20th, 2012

beartato phd

(no subject)

Went to "traditional thursday D's" at a non-D's bar (as is apparently now traditional) down in the South Side. Met a few of the newer grad students. chrisamaphone mentioned an interesting types puzzle.

It goes like this: the quantified "double-negation" type ∀R.(A→R)→R is essentially* isomorphic to A, yeah? Okay, so what type is ∀R.Monoid R⇒(A→R)→R isomorphic to?

Collapse )

*wellllll I thought I understood in what sense they were isomorphic, but it turned out to be a little trickier than I remembered after we talked about it for a while. It seems evident there's a bijection between the canonical forms of the two types, but if you try to internalize it as a pair of back-and-forth terms, one of the compositions that you want to reduce to the identity does so reduce, and the other doesn't. I forget what this is supposed to mean.