What is a natural transformation in haskell?

Question

I would like to know, what is natural transformation in Haskell. The natural transformation is described with the following signature:

F[a] ~> G[a]

For example, I could transform:

Maybe a ~> List a

Right?

What about IO, it is impossible to do natural transformation right?
What is the purpose of the natural transformation?

Malapert

Answer 1

A natural transformation, without getting into the category theory behind it, is really just a polymorphic function.

Prelude> :set -XRankNTypes
Prelude> :set -XTypeOperators
Prelude> type (~>) f g = forall x. f x -> g x

The ~> operator maps a type constructor to another type constructor, in such a way that it works for any given argument to the first type constructor. The TypeOperator extension is what lets us use ~> instead of a name like NatTrans; the RankNTypes is what lets us use forall in the definition so that the caller can choose which type f and g will be applied to.

Here is an example of a natural transformation from Maybe to List, which takes a Maybe a for any type a, and produces an equivalent list (by returning either an empty list or the wrapped value as a singleton list).

Prelude> :{
Prelude| m2l :: Maybe ~> [] -- Maybe a -> [a]
Prelude| m2l Nothing = []
Prelude| m2l (Just x) = [x]
Prelude| :}
Prelude> m2l Nothing
[]
Prelude> m2l (Just 3)
[3]
Prelude> m2l (Just 'c')
"c"

An "inverse" would be l2m :: [] ~> Maybe, with l2m [] = Nothing and l2m (x:_) = Just x. ( I put inverse in quotes because m2l (l2m [1,2,3]) /= [1,2,3])

Nothing prevents you from using IO as either of the type constructors (although if IO is on the left, it must be on the right as well).

foo :: IO ~> IO
foo a = putStrLn "hi" >> a

Then

> foo (putStrLn "foo")
hi
foo
> foo (return 3)
hi
3

Another example would be to view length as a natural transformation from [] to Const Int (adapted from https://bartoszmilewski.com/2015/04/07/natural-transformations/, which I highly recommend reading):

-- Isomorphic to builtin length, as Const Int is isomorphic to Int
-- Requires importing Data.Functor.Const
length' :: [] ~> Const Int
length' [] = Const 0
length' (x:xs) = Const (1 + getConst (length' xs))

Majormajordomo

Why is the transformation from IO a to Maybe a is not possible? – Malapert

One issue I have with this answer: I think "polymorphic function" is not correct; it should something more like "mapping from one functor to another". Also, while in category theory a natural transformation is by definition a mapping of one functor to another, I don't know if that requirement really carries over to ~> as defined. – Majormajordomo

An IO is also a functor, but why is the transformation IO a to Maybe a is not possible? – Malapert

That's a restriction on the Haskell implementation of ~> (due to the implementation of IO itself) rather than a restriction on natural transformations in general. In this sense, ~> is a partial "function" of type constructors that represents most possible natural transformations. – Majormajordomo

As I understand it all functions in Haskell are endofunctors of the small category Hask. So any arguments of a polymorphic function when applied would be naturally isomorphic. – Flowered

Answer 2

It's useful to be explicit here: a natural transformation is a function of a signature

η :: ∀ a . Φ a -> Ψ a

where Φ and Ψ are functors. The ∀ is of course implied in Haskell, but that really is the crucial thing about natural transformations. That, and the commutative diagram

i.e. in Haskell,

(fmap f :: Ψ x -> Ψ y) . (η :: Φ x -> Ψ x)
           ≡ (η :: Φ y -> Ψ y) . (fmap f :: Φ x -> Φ y)

or short, fmap f . η ≡ η . fmap f. (But note well that both η have different type here!)

For example, I could transform:

Maybe a ~> List a

Mm, yyyea...ish. Again, be explicit what you mean. Concretely, the following is a natural transformation from Maybe to [] (it is not a natural transformation from Maybe a to [a], that wouldn't make sense):

maybeToList :: Maybe a -> [a]
maybeToList Nothing = []
maybeToList (Just a) = [a]

but it's not the only such transformation. In fact there are ℕ many such transformations, such as

maybeToList9 :: Maybe a -> [a]
maybeToList9 Nothing = []
maybeToList9 (Just a) = [a,a,a,a,a,a,a,a,a]

What about IO, it is impossible to do natural transformation right?

That's possible as well. For instance, here's a natural transformation from NonEmpty to IO:

import qualified Data.List.NonEmpty as NE
import System.Exit (die)

selectElem :: NonEmpty a -> IO a
selectElem l = do
   let len = NE.length l
   putStrLn $ "Which element? (Must be <"++show len++")"
   i <- readLine
   if i<len then die "Index too big!"
            else return $ l NE.! i

Fini

Answer 3

With IO you can write a natural transformation, e.g.

foo :: IO a -> IO a
foo act = act >> putStrLn "hello" >> act

You can't write [a] -> IO a or Maybe a -> IO a if you want these to be total functions. You can write Identity a -> IO a and (s,a) -> IO a.

There is no intrinsic "purpose" for a natural transformation, it's just a definition. It simply happens that in Haskell, every function f :: forall a . F a -> G a where G and F are functors enjoy the naturality property

f . fmap g = fmap g . f

which is sometimes called the "free theorem" associated to f.

Engineer

“You can't write [a] -> IO a or Maybe a -> IO a if you want these to be total functions.” Actually that's a bit debatable. I'd say const exitSuccess is a total function, and is trivially a natural transformation. – Fini

@Fini I completely agree -- that's a bit of a stretch. Even raising an exception or doing forever (print 5) could be considered "total" in the context of IO. Still, the naturality law in such case is not that useful since we would actually have f = fmap anything . f, since there is no value of type a involved. – Engineer

Ok, \case {[] -> exitSuccess; (a:_) -> return a}. – Fini

Answer 4

Awesome question. I know of no source on the Internet that would explain this accessibly. I am not sure I can explain it accessibly either. But it is, in essence, not even simple — it is trivial. So brace yourself.

 

Disclaimer

I am not a guru, so lend awhile for the elders to destroy this answer before believing anything I say.

 

Theory

This is my favourite picture from Mac Lane's tome.

It is pointless to explain in words. You need to stare at it for a while and eventually see how it tells you something about the example I presently provide. You can also read some explanations on the Internet.

 

Practice

First we will define some types. They are in essence the same as the usual [a], but Stream is always infinite, and Vector has exactly some prescribed length.

data Stream a = a :... Stream a

instance Functor Stream where
    fmap f (x :... xs) = f x :... fmap f xs

data Vector (n :: Nat) a = a ::: Vector (n - 1) a | End deriving (Show, Eq)
infixr 4 :::

instance Functor (Vector n) where
    fmap f (x ::: xs) = f x ::: fmap f xs
    fmap f End = End

Now we will create a family of functions take_ that work in the same way as the Prelude.take, but only as our more refined types allow. Particularly, we will not be providing a run-time value of n, but a compile time type level annotation n.

class Take (n :: Nat) where take_ :: Stream a -> Vector n a
instance Take 0       where take_ _ = End
instance {-# overlappable #-} ((m - 1) ~ n, Take n) => Take m
    where take_ (x :... xs) = x ::: take_ @n xs

Let us also have some example values we can use to check if anything at all works. Here I define the stream of natural numbers from 0 to infinity:

n :: Stream Integer
n = n_i 0

n_i :: Integer -> Stream Integer
n_i x = x :... n_i (x + 1)

We could not possibly observe an infinite stream, but with the take_ function we have we can take a look at an arbitrary prefix thereof. See:

λ :set -XDataKinds
λ :set -XTypeApplications
λ take_ @3 n
0 ::: (1 ::: (2 ::: End))

It really is a natural transformation. Compare this example to Mac Lane's diagram:

λ take_ @10 . fmap (^2) $ n
0 ::: (1 ::: (4 ::: (9 ::: (16 ::: (25 ::: (36 ::: (49 ::: (64 ::: (81 ::: End)))))))))
λ fmap (^2) . take_ @10 $ n
0 ::: (1 ::: (4 ::: (9 ::: (16 ::: (25 ::: (36 ::: (49 ::: (64 ::: (81 ::: End)))))))))

Can you see how (^2) is f, fmap (^2) is either S f or T f, and take_ is τ?

 

Theory, revisited

As the elders pointed out in their answers, in Haskell, thanks to the awesome parametric polymorphism we enjoy, you get some guarantees for free. Specifically, any parametrically polymorphic transformation mapping between two lawful functors is natural. It is easy to believe, but involved to prove. Here is one approach to this topic.

Notice also that a function that is not parametrically polymorphic — be it a monomorphic function or a class method — may be a transformation that is not natural. Example:

class Break (n :: Nat) a where break_ :: Stream a -> Vector n a
instance Break 0 Integer where break_ _ = End
instance {-# overlappable #-} ((m - 1) ~ n, Break n Integer) => Break m Integer
    where break_ (x :... xs) = if even x then x ::: break_ @n xs else (x + 1) ::: break_ @n xs

It really does break the law. Compare with the previous example:

λ break_ @10 . fmap (^2) $ n
0 ::: (2 ::: (4 ::: (10 ::: (16 ::: (26 ::: (36 ::: (50 ::: (64 ::: (82 ::: End)))))))))
λ fmap (^2) . break_ @10 $ n
0 ::: (4 ::: (4 ::: (16 ::: (16 ::: (36 ::: (36 ::: (64 ::: (64 ::: (100 ::: End)))))))))

The types of take_ and break_ have distinct constraints, and that is your telltale:

λ :t take_
take_ :: Take n => Stream a -> Vector n a
λ :t break_
break_ :: Break n a => Stream a -> Vector n a

— See that a in break_'s constraint? That means the free theorem does not hold, and break_ may not be natural.

Obel