# Natural Transformations and fmap

10 messages
Open this post in threaded view
|
Report Content as Inappropriate

## Natural Transformations and fmap

 I've been playing around with the relationship between monoids and monads (see http://www.jonmsterling.com/posts/2012-01-12-unifying-monoids-and-monads-with-polymorphic-kinds.html and http://blog.sigfpe.com/2008/11/from-monoids-to-monads.html), and I put together my own implementation which I'm quite happy with, that you can see at http://hpaste.org/56903 ; relying only on the extensions RankNTypes, TypeOperators, NoImplicitPrelude, ScopedTypeVariables; 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)?  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 [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe
Open this post in threaded view
|
Report Content as Inappropriate

## Re: Natural Transformations and fmap

 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). > 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 [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe
Open this post in threaded view
|
Report Content as Inappropriate

## Re: Natural Transformations and fmap

 On Mon, Jan 23, 2012 at 8:05 PM, Daniel Fischer 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 havef :: M :-> Ng :: A -> Binstance Functor M -- with proofs of functor laws instance Functor N -- with proofs of functor lawsHow 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 [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe
Open this post in threaded view
|
Report Content as Inappropriate

## Re: Natural Transformations and fmap

Open this post in threaded view
|
Report Content as Inappropriate

## Re: Natural Transformations and fmap

 In reply to this post by Ryan Ingram On Mon, Jan 23, 2012 at 09:06:52PM -0800, Ryan Ingram wrote: > On Mon, Jan 23, 2012 at 8:05 PM, Daniel Fischer < > [hidden email]> 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 [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe
Open this post in threaded view
|
Report Content as Inappropriate

## Re: Natural Transformations and fmap

Open this post in threaded view
|
Report Content as Inappropriate

## Re: Natural Transformations and fmap

 In reply to this post by Ryan Ingram On 1/23/12 10:39 PM, Ryan Ingram wrote: >      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)? That is the defining property of natural transformations. To prove it for polymorphic functions in Haskell you'll probably want to leverage parametricity. I assume you don't know category theory, based on other emails in this thread. But the definition of a natural transformation is that it is a family of morphisms/functions { f_X :: M X -> N X | X an object/type } such that for all g :: a -> b we have that f_b . fmap_m g == fmap_n g . f_a Thus, you can in principle define plenty of natural transformations which do not have the type f :: forall X. M X -> N X. The only requirement is that the family of morphisms obeys that equation. It's nice however that if a function has that type, then it is guaranteed to satisfy the equation (so long as it doesn't break the rules by playing with strictness or other things that make it so Hask isn't actually a category). -- Live well, ~wren _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe
Open this post in threaded view
|
Report Content as Inappropriate

## Re: Natural Transformations and fmap

Open this post in threaded view
|
Report Content as Inappropriate

## Re: Natural Transformations and fmap

 On 1/27/12 7:56 PM, Ryan Ingram wrote: >> Thus, you can in principle define plenty of natural transformations which > do not have the type f :: forall X. M X ->  N X. > > Can you suggest one?  I don't see how you can get around f needing to act > at multiple types since it can occur before and after g's fmap: Right. A natural transformation is a family of functions (one for each type). My point was, "forall" is one way of defining a family of functions, but it's not the only one. For instance, we could use a type class, or some fancy generics library, or a non-parametric forall in languages which allow type-case. Or we could use some way of defining it which is outside of the language in which the component functions exist. For example, consider the simply typed lambda calculus. STLC doesn't have quantifiers so we can't define (f :: forall X. M X -> N X) as a natural transformation from within the language, but we could still talk about the family of simply-typed functions { f_X :: M X -> N X | X <- type }. Calling a family of functions a natural transformation is an extralinguistic statement about the functions; there are, in general, more natural transformations than can be defined from within the language in question. Just as there are, in general, more endofunctors than can be defined within the language (let alone other functors). The "naturality" behind natural transformations is just the fact that (forall g, fmap g . f = f . fmap g). Satisfying the equation means that the family of fs is "parametric enough", regardless of how we've defined the family or how/whether we can implement the family as polymorphism within the language. -- Live well, ~wren _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe