[Haskell-cafe] is proof by testing possible?

[Derek Elkins]

On Mon, Oct 12, 2009 at 8:15 PM, Joe Fredette <jfredett at gmail.com> wrote:
> 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.)