Constrained polymorphic functions as natural transformations
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 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. 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. 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
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@haskell.org http://www.haskell.org/mailman/listinfo/beginners
Hi Brent,
Many thanks for taking the time to have a look! Hope you might be able to
cope with some more amateurish fumbling as I try and expand my
understanding...
On 14 November 2013 13:59, Brent Yorgey
In general one must consider what are called *di*natural transformations. (I ought to write a blog post about this.)...but I thought I would mention it in case you want to look it up later.
Thanks -- dinatural transformations are probably a bit beyond my comfort zone right now, but I'll add it to my list of things to look at. Interesting to discover that not all polymorphic functions are natural transformations. "fix" seems rather exotic -- are there any less unusual examples? Note that you can't always characterize a type class by a single
function like this. For example, consider class Foo ... There is no way to pick functors f and g such that a Foo dictionary is equivalent to f a -> g a.
I was wondering why the following wouldn't do the trick? sig :: Foo a => Either Int a -> Either a Int sig (Left n) = Left (bar n) sig (Right a) = Right (baz a)
This doesn't really make sense. If a natural transformation consists of a family of arrows which all live in Hask_T,
In this case, I think the family of arrows lives in Hask -- we can reinterpret our Hask endofunctors as instead being functors from Hask_T -> Hask. Then there's no requirement on our constrained polymorphic functions to commute with sig. In your example function f, the two functors would be the identify functor "Id" and a constant functor "K Foo", and naturality is just saying that, for any function g: A -> B that satisfies show == show . f, then: f = f . g Which is clearly true for f. Am I still barking up the wrong tree? Apologies if so, but it *feels* like there should be something here, with the intuition that: Functions that don't "inspect" their values ==> you can substitute values without fundamentally affecting the action of the function ==> natural transformations between Hask endofunctors. Functions that don't inspect their values other than through a particular interface T ==> you can substitute values without fundamentally affecting the action of the function, providing your substitution is invisible through the interface T ==> Natural transformations between functors Hask_T -> Hask. -- Matt
On Fri, Dec 13, 2013 at 10:25 PM, Matt R
Interesting to discover that not all polymorphic functions are natural transformations. "fix" seems rather exotic -- are there any less unusual examples?
None of the church numerals of type (a -> a) -> (a -> a) are natural transformations either: zero _ = id one f = f two f = f . f three f = f . f . f etc. -- Kim-Ee
Hi Matt, On Fri, Dec 13, 2013 at 03:25:03PM +0000, Matt R wrote:
Note that you can't always characterize a type class by a single
function like this. For example, consider class Foo ... There is no way to pick functors f and g such that a Foo dictionary is equivalent to f a -> g a.
I was wondering why the following wouldn't do the trick?
sig :: Foo a => Either Int a -> Either a Int sig (Left n) = Left (bar n) sig (Right a) = Right (baz a)
You have encoded a Foo dictionary as an Either Int a -> Either a Int function, but that is very different than saying that having a Foo dictionary is *equivalent* to having an Either Int a -> Either a Int function. They are not equivalent; in particular, you could have a function which sends Left 5 to Right 6, which does not correpond to anything in Foo. Put another way, if you try to write a Foo instance given only some unknown function of type (Either Int a -> Either a Int), you will find that you cannot do it. So my point stands that it is not always possible to *characterize* a type class as a natural transformation.
This doesn't really make sense. If a natural transformation consists of a family of arrows which all live in Hask_T,
In this case, I think the family of arrows lives in Hask -- we can reinterpret our Hask endofunctors as instead being functors from Hask_T -> Hask. Then there's no requirement on our constrained polymorphic functions to commute with sig.
In your example function f, the two functors would be the identify functor "Id" and a constant functor "K Foo", and naturality is just saying that, for any function g: A -> B that satisfies show == show . f, then:
f = f . g
Which is clearly true for f.
Hmm, yes, this seems plausible.
Am I still barking up the wrong tree? Apologies if so, but it *feels* like there should be something here, with the intuition that:
Functions that don't "inspect" their values ==> you can substitute values without fundamentally affecting the action of the function ==> natural transformations between Hask endofunctors.
Functions that don't inspect their values other than through a particular interface T ==> you can substitute values without fundamentally affecting the action of the function, providing your substitution is invisible through the interface T ==> Natural transformations between functors Hask_T -> Hask.
Yes, makes sense I think. -Brent
On 22 December 2013 20:26, Brent Yorgey
You have encoded a Foo dictionary as an Either Int a -> Either a Int function, but that is very different than saying that having a Foo dictionary is *equivalent* to having an Either Int a -> Either a Int function. They are not equivalent; in particular, you could have a function which sends Left 5 to Right 6, which does not correpond to anything in Foo. Put another way, if you try to write a Foo instance given only some unknown function of type (Either Int a -> Either a Int), you will find that you cannot do it. So my point stands that it is not always possible to *characterize* a type class as a natural transformation.
OK, I think see what you're saying: while you can represent any Foo instance as an "Either Int a -> Either a Int", not every "Either Int a -> Either a Int" represents a Foo instance. I guess I was originally hoping to encode a bunch of equations into a single one, so that rather than a collection of similar equations, one for each function in the type class... fmap f . foo == foo . fmap f fmap f . bar == bar . fmap f fmap f . baz == baz . fmap f ...you could encode the typeclass signature as some function "sig" and express the same condition as a single equation (which would be true if and only if the above equations were true): fmap f . sig == sig . fmap f I don't know if that's always possible. As you pointed out, you'd need dinatural transformations in general, which I've had a look at, although I confess I find it hard to get the same intuition about them as for regular natural transformations. If you wanted to write that blog post, you'd have at least one guaranteed keen reader ;-) Cheers, -- Matt
participants (3)
-
Brent Yorgey -
Kim-Ee Yeoh -
Matt R