[Haskell-cafe] Natural Transformations and fmap

[Ryan Ingram]

I tried the free theorem generator (
http://www-ps.iai.uni-bonn.de/cgi-bin/free-theorems-webui.cgi) and it
wouldn't let me use generic functors, but playing with [] and Maybe leads
me to believe that the free theorem for :-> is

forall f :: m :-> n, forall g :: a -> b, g strict and total
fmap g . f = f . fmap g

This implies that the monad laws don't necessarily hold in situations like
"\m -> m >>= const Nothing", which seems wrong to me.  The counterexamples (
http://www-ps.iai.uni-bonn.de/cgi-bin/exfind.cgi), however, all rely on
"odd" natural transformations like (\_ -> Just undefined).  My guess is
that there is a side condition we can put on f that is implied by the
monoid laws which doesn't require g to be strict or total.

  -- ryan

On Mon, Jan 23, 2012 at 10:23 PM, Brent Yorgey <byorgey at seas.upenn.edu>wrote:

> On Mon, Jan 23, 2012 at 09:06:52PM -0800, Ryan Ingram wrote:
> > On Mon, Jan 23, 2012 at 8:05 PM, Daniel Fischer <
> > daniel.is.fischer at googlemail.com> wrote:
> >
> > > On Tuesday 24 January 2012, 04:39:03, Ryan Ingram wrote:
> > > > At the end of that paste, I prove the three Haskell monad laws from
> the
> > > > functor laws and "monoid"-ish versions of the monad laws, but my
> proofs
> > > > all rely on a property of natural transformations that I'm not sure
> how
> > > > to prove; given
> > > >
> > > >     type m :-> n = (forall x. m x -> n x)
> > > >     class Functor f where fmap :: forall a b. (a -> b) -> f a -> f b
> > > >     -- Functor identity law: fmap id = id
> > > >     -- Functor composition law fmap (f . g) = fmap f . fmap g
> > > >
> > > > Given Functors m and n, natural transformation f :: m :-> n, and g
> :: a
> > > > -> b, how can I prove (f . fmap_m g) = (fmap_n g . f)?
> > >
> > > Unless I'm utterly confused, that's (part of) the definition of a
> natural
> > > transformation (for non-category-theorists).
> > >
> >
> > Alright, let's pretend I know nothing about natural transformations and
> > just have the type declaration
> >
> > type m :-> n = (forall x. m x -> n x)
> >
> > And I have
> > f :: M :-> N
> > g :: A -> B
> > instance Functor M -- with proofs of functor laws
> > instance Functor N -- with proofs of functor laws
> >
> > How can I prove
> >   fmap g. f :: M A -> N B
> >   =
> >   f . fmap g :: M A -> N B
> >
> > I assume I need to make some sort of appeal to the parametricity of
> > M :-> N.
>
> This is in fact precisely the "free theorem" you get from the
> parametricity of f.  Parametricity means that f must act "uniformly"
> for all x -- which is an intuitive way of saying that f really is a
> natural transformation.
>
> -Brent
>
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20120126/89b6ed16/attachment.htm>