Have you tried generating a free theorem for :-> ? (I haven't as I'm writing from my phone)
24.01.2012, в 9:06, Ryan Ingram <[email protected]> написал(а): > 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. > > > Is there some > > more fundamental law of natural transformations that I'm not aware of > > that I need to use? Is it possible to write a natural transformation > > in Haskell that violates this law? > > > > -- ryan > > > _______________________________________________ > 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
