Reasoning with representable functors
A couple weeks ago I was working on a project using Conal Elliott’s uniform-pair library and noticed it had a curious
Monad instance, which I’ve reproduced below.
I was especially curious about why
joinP chose the first element of the first pair and the second element of the second pair. My initial guess was that it was determined by the
Functor instance which would’ve looked something like..
Monad to be consistent with
Functor the follow equation should hold..
..but this didn’t really help.
Taking either element of the outer pair would’ve been consistent with the
Functor instance, as would taking the first element of the first pair and the second element of the second pair.
A couple days later I was talking with Conal about it and he hinted at using the fact that uniform pairs are representable functors. For a functor to be representable in Haskell1 means it is isomorphic to the set of functions from
X, for some fixed
X (this “set of functions from X” is also known as the reader monad). For uniform pairs,
X = Bool. Indeed, the following functions are mutual inverses.
To prove that a functor
f is representable in Haskell is to implement the
Representable type class. The following is reproduced from the representable-functors package.
Key f refers to the fixed
X mentioned above, so
Key Pair = Bool. Substituing
Key f reveals signatures matching the
As it turns out every
Representable has a canonical monadic return and bind, defined as:
Let’s see what this looks like for
Pair. First let’s do some substitution on
That matches our
return definition above. Now let’s do the same for
True into the lambda:
The same as
This is awesome. By starting with the meaning of his data type, Conal discovered the only natural type class instance consistent with the meaning. While in this case I started with the instance and worked my way back, I believe the more useful and consistent approach is to think hard about your data type’s denotation and work your way forward.