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@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@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@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe