Tue Dec 27 08:50:22 EST 2011
Writing a typed embedded language I've been running into a pattern of
why I call "type commutation", which turns up when writing
representations of functions/structures in terms of
functions/structures of representations, i.e.:
2x1D (1) r (a -> b) <-> (r a) -> (r b)
(2) r (a, b) <-> (r a, r b)
1x1D (3) r (x a) <-> x (r a)
Case (1) is almost the Functor type in Haskell, which expresses this
for functions. To be exact it is a bidirectional functor.
What is this generic pattern called? I.e. not just functions but
generic 1,2,3,... dimensional type constructors?
Also, these all seem to be commutations between * -> * (i.e. r in the
above), and * -> * or a multi-argument kind (i.e. x, (->), (,) in the
above), but never between multi-argument kinds. Or maybe it does.
This is a relation between two * -> * -> * kinds.
2x2D (4) (a -> b, c -> d) <-> ((a,c) -> (b,d))
Anyways, such a relation has many more degrees of freedom that don't
seem to make sense, like replacing c (input) and d (output) in the rhs
There's a clear pattern here. I'm missing some language to talk about
it. Probably category theory. Is this a natural transformation?
As a diagram, representing (,) tupling as =>
a -> b a b
|| || -> ||
\/ \/ \/
c -> d c d
With lots of handwaving, I guess so. A natural transformation maps
functors to functors. In the left diagram. -> is an arrow, => is a
Fuctor, and in the right diagram, => is an arrow and -> is a Functor.
Anyways... for later deconfusion.