**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.