[<<][compsci][>>][..]

Functors

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[1].

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
of (4).

There's a clear pattern here.  I'm missing some language to talk about
it.  Probably category theory.  Is this a natural transformation[2]?

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.


[1] http://hackage.haskell.org/packages/archive/fclabels/0.4.2/doc/html/Data-Record-Label.html#3
[2] http://en.wikipedia.org/wiki/Natural_transformation




[Reply][About]
[<<][compsci][>>][..]