[Haskell-beginners] Constrained polymorphic functions as natural transformations

[Brent Yorgey]

Hi Matt,

You have some cool ideas here --- though I think there are a few
places what you say doesn't quite make sense, but I think you're on
the right track.

One thing to note first is that the formalism of natural
transformations only covers *some* but not *all* polymorphic
functions.  For example, there is no way to view

  fix :: (a -> a) -> a

as a natural transformation, because (a -> a) does not correspond to a
functor over a.  In general one must consider what are called
*di*natural transformations.  (I ought to write a blog post about
this.)  In any case, this is a bit of a digression---simple natural
transformations suffice for a great many "real world" examples---but I
thought I would mention it in case you want to look it up later.

On Wed, Oct 30, 2013 at 09:50:03AM +0000, Matt R wrote:
> I read this excellent blog article on natural transformations[1], which
> helped me gain one intuition as to what they are: "functions that don't
> make too many assumptions about their arguments". In the article, natural
> transformations make "no assumptions at all" about their arguments.
> However, it's often the case that a Haskell function will require a type
> argument constrained by a type class, e.g. show :: Show a => a -> String. I
> wondered if it was possible to characterise these functions using category
> theory too. Below is my attempt, and I'm hoping people can tell me whether
> I'm in the right ballpark (or point me in the direction of a better
> ball-park...)
> 
> For a particular type class T, we can form a subcategory Hask_T of Hask
> consisting of all the instances of the type class as objects, with the
> arrows just those functions that "commute" with the signature of the type
> class. For example, in Hask_Show, the arrows would be all the functions f:
> A -> B such that:
> 
>   show == show . f
> 
> Or for Data.Monoid, all the monoid homomorphisms f:
> 
>   mappend (f x) (f y) == f (mappend x y)
>   mempty == f mempty

Sounds good so far.  This seems like a reasonable definition of a
category, and an interesting one to study.

> In general, for any type class, we can formulate two functors f and g and a
> function sig :: f a -> g a that captures the operations in the type class,
> and then the condition is that:
> 
>   fmap f . sig == sig . fmap f.

Note that you can't always characterize a type class by a single
function like this.  For example, consider

  class Foo a where
    bar :: Int -> a
    baz :: a -> Int

There is no way to pick functors f and g such that a Foo dictionary is
equivalent to  f a -> g a.

I would be willing to believe that there is something interesting to
say about those type classes which one *can* characterize in this way,
but I don't know what it might be.

> Then we have that the polymorphic functions with a type class constraint of
> T are just the same thing as natural transformations in this subcategory
> Hask_T.

This doesn't really make sense.  If a natural transformation
consists of a family of arrows which all live in Hask_T, then all
those arrows must (by definition) commute with the type class
signature.  But consider, for example, the function

  data Foo = Foo | Bar   -- no Show instance!
  f :: Show a => a -> Foo
  f a | show a == "woz" = Foo
      | otherwise       = Bar

This f certainly does not satisfy  show == show . f  -- that isn't
even well-typed as Foo doesn't have a Show instance; and if it did it
would be easy to make a Show instance for which that equation didn't
hold.

Interpreting a type class constraint as determining what category we
are living in is quite appealing, and I have seen this approach taken
informally especially when talking about classes such as Eq and Ord.
However, I have never seen it spelled out and I am not sure what the
right way to do it is in general.

Another approach would be to simply consider a type class constraint
equivalent to a dictionary argument, as in

      Show a => a -> Foo
  === Show a -> a -> Foo
  === (a -> String) -> (a -> Foo)

which we can see as a natural transformation between the
(contravariant) functors (_ -> String) and (_ -> Foo).

-Brent

> Is the above correct / along the right lines?
> 
> Thanks,
> 
> -- Matt
> 
> [1] "You Could Have Defined Natural Transformations",
> http://blog.sigfpe.com/2008/05/you-could-have-defined-natural.html

> _______________________________________________
> Beginners mailing list
> Beginners at haskell.org
> http://www.haskell.org/mailman/listinfo/beginners