Natural Transformations and fmap

[Ryan Ingram]

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

[Daniel Fischer]

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

[Ryan Ingram]

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. 

 

> 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

[Eugene Kirpichov]

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 <[hidden email]> написал(а):

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. 

 

> 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

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Brent Yorgey-2]

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

[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 <[hidden email]> 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 <
> [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

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe

[wren ng thornton]

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

[Ryan Ingram]

I know a bit of category theory, but I'm trying to look at it from a fundamental perspective; I know that I intend (m :-> n) to mean "natural transformation from functor m to functor n", but the type itself (forall x. m x -> n x) doesn't necessarily enforce that.

However, the type of natural transformations comes with a free theorem, for example

   concat :: [[a]] -> [a]

has the free theorem

   forall f :: a -> b, f strict and total, fmap f . concat = concat . fmap (fmap f)

The strictness condition is needed; consider

   broken_concat :: [[a]] -> [a]
   broken_concat _ = [undefined]
   f = const ()

   fmap f (broken_concat []) = fmap f [undefined] = [()]
   broken_concat (fmap (fmap f) []) = broken_concat [] = [undefined]

The 'taming selective strictness' version of the free theorem generator[1] allows removing the totality condition on f, but not the strictness condition.

But in the case of concat, you can prove a stronger theorem:

   forall f :: a -> b, fmap f . concat = concat . fmap (fmap f)

My suspicion is that this stronger theorem holds for all strict and total natural transformations, but I don't know how to go about proving that suspicion.  I'm a hobbyist mathematician and a professional programmer, not the other way around :)

I think it's probably easy to prove that the monoid laws imply that mult' and one' are strict and total.

> 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:

fmap g . f = f . fmap g

   M A --fmap_M g--> M B
    |                 |
   f_A               f_B
    |                 |
    v                 v
   N A --fmap_N g--> N B

You can have n = m, of course, but that just means f :: M :-> M.

  -- ryan

[1] http://www-ps.iai.uni-bonn.de/cgi-bin/polyseq.cgi
Use this term:
/\a. let flipappend =(\xs :: [a]. fix (\rec :: [a] -> [a]. \ys :: [a].
                      case ys of { [] -> xs; y:zs -> y : rec zs })) in
     let concat = fix (\rec :: [[a]] -> [a]. \xss :: [[a]].
                       case xss of { [] -> []_{a}; xs:yss -> flipappend (rec yss) xs}) in
     concat

[2] See http://hpaste.org/56903  Summary:

-- both of these types have obvious Functor instances
newtype (f :. g) x = O (f (g x))
data Id x = Id x

class Functor m => Monad m where
   one'  :: Id       :-> m
   mult' :: (m :. m) :-> m

-- instances are required to satisfy monoid laws:
--    one' is a left/right identity for mult':
--        forall x :: m a
--            mult' . O . one' . Id $ x = x = mult' . O . fmap (one' . Id) $ x
--    mult' is associative:
--        forall x :: m (m (m a))).
--            mult' . O . mult' . O $ x = mult' . O . fmap (mult' . O) $ x

On Thu, Jan 26, 2012 at 9:30 PM, wren ng thornton <[hidden email]> wrote:

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

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe

[wren ng thornton]

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

[Janis Voigtländer]

Ryan Ingram wrote:

> However, the type of natural transformations comes with a free theorem, for
> example
>
>     concat :: [[a]] ->  [a]
>
> has the free theorem
>
>     forall f :: a ->  b, f strict and total, fmap f . concat = concat . fmap
> (fmap f)
>
> The strictness condition is needed; consider
>
>     broken_concat :: [[a]] ->  [a]
>     broken_concat _ = [undefined]
>     f = const ()
>
>     fmap f (broken_concat []) = fmap f [undefined] = [()]
>     broken_concat (fmap (fmap f) []) = broken_concat [] = [undefined]
>
> The 'taming selective strictness' version of the free theorem generator[1]
> allows removing the totality condition on f, but not the strictness
> condition.
>
> But in the case of concat, you can prove a stronger theorem:
>
>     forall f :: a ->  b, fmap f . concat = concat . fmap (fmap f)
>
> My suspicion is that this stronger theorem holds for all strict and total
> natural transformations, but I don't know how to go about proving that
> suspicion.  I'm a hobbyist mathematician and a professional programmer, not
> the other way around:)
>
> ...
>
> [1]http://www-ps.iai.uni-bonn.de/cgi-bin/polyseq.cgi

There is an analogous approach to the "taming selective strictness"
version of the free theorem generator where it is general recursion that
is tamed. In that setting, you then get free theorems like that for
concat without either strictness or totality side conditions. It is
really very similar, indeed the "taming selective strictness" work takes
over and develops further the much earlier "taming general recursion"
ideas. The original source for the latter is:

http://dblp.uni-trier.de/rec/bibtex/conf/esop/LaunchburyP96

Just nobody ever bothered to implement it in a tool. (Well, actually,
such an implementation is essentially hidden inside the counterexample
generator http://www-ps.iai.uni-bonn.de/cgi-bin/exfind.cgi)

Best,
Janis.

--
Jun.-Prof. Dr. Janis Voigtländer
http://www.iai.uni-bonn.de/~jv/
mailto:[hidden email]

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe