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.
