
On Mon, Oct 12, 2009 at 8:15 PM, Joe Fredette
Sadly not enough, I understand the basics, but the whole "proof <=> this diagram commutes" thing still seems like voodoo to me. There is a section coming up in my Topology ISP that will be on CT. So I hope that I will be able to gain some purchase on the subject, at least enough to build up a working understanding on my own.
I have a practical understanding of Functors and Natural Transformations, so working a bit with these free theorem things is kind of fun.
Actually, another germane-if-random question, why isn't there a natural transformation class? Something like:
class Functor f, Functor g => NatTrans g f a where trans :: f a -> g a
So your flatten function becomes a `trans` a la
instance NatTrans Tree [] a where trans = flatten
In fact, I'm going to attempt to do this now... Maybe I'll figure out why before you reply. :)
Diagrams are just a graphical depiction of systems of equations. Every pair of paths with the same start and end point are equal. I don't care for diagrams that much and that graphical depiction isn't that important for CT, though it has some mnemonic value. As for a NatTrans class, your example is broken in several ways. Natural transformations, though, are trivial in Haskell. type NatTrans f g = forall a. f a -> g a flatten :: NatTrans Tree [] I.e. a natural transformation between Haskell Functors are just polymorphic functions between them. In general, a polymorphic function is a dinatural transformation and the dinaturality conditions are the free theorems (or at least, special cases of the free theorem for the type, which I believe, but haven't proven, implies the full free theorem.)