Jason (jcreed) wrote,

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?

The answer turns out to be the type that it seemed like the only type it could be, namely list-of-A.

It's worth puzzling out what the two functions are that witness the isomorphism, but the cool thing I realized on the way back is that the type expression
∀R.Monoid R⇒(A→R)→R
arises directly from thinking about the universal property for the free monoid.

It goes like this: I want the type constructor H to be the free monoid, whatever that is, because I've been living under a rock and I've never heard of lists. I know the universal property for free monoids says: if I have a monoid R, and a set A, and a function from that set A to the underlying set of R, then I can uniquely lift that set function to a monoid homomorphism from H(A) to R.

Let me say that again, only rearranged.

I know that, given an element of H(A), and also given a monoid R, and a function from A to R, I should be able to give you an element of R.

So I pull the trick of:

Defining an element of H(A) to be a function that takes a monoid R and a function from A to R and returns an element of R. Bam! That's the above type.

Of course nothing I said depends on Monoids; the type
∀R.T R⇒(A→R)→R
I guess in some sense automatically creates the free algebra for the type constructor T? That's pretty cool.

*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.
Tags: cps, logic, math, monads
  • Post a new comment


    Anonymous comments are disabled in this journal

    default userpic

    Your IP address will be recorded