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 <[email protected]>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 < > > [email protected]> 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 > [email protected] > http://www.haskell.org/mailman/listinfo/haskell-cafe >
_______________________________________________ Haskell-Cafe mailing list [email protected] http://www.haskell.org/mailman/listinfo/haskell-cafe
