How to it is a natural transformation?

Question

I am going to use the wonderful library https://tpolecat.github.io/doobie/ and it is fully functional.

I was going through the first example and I have recognized:

A Transactor is a data type that knows how to connect to a database, hand out connections, and clean them up; and with this knowledge it can transform ConnectionIO ~> IO, which gives us a program we can run.

ConnectionIO ~> IO is a natural transformation in category theory but have never fully understood, what exactly a natural transformation is.

However, I know it is transformation from one category into other category. For example:

F[A] ~> G[A]

is a natural transformation from category F to G without changing the content.

Not everything can be naturally transformed and the question is, how do the author of library doobie know, that he can do the natural transformation from ConnectionIO ~> IO?

*However, I know it is transformation from one category into other category.* No. Transformation from category to category is functor (it maps objects to objects and morphisms to morphisms). Natural transformation is transformation from functor to functor (i.e. it's a morphism in category of functors). — Dmytro Mitin, May 22 '20 at 17:14
If `F` and `G` are `Functor`s, any `forall a. F a -> G a` function is a natural transformation from `F` to `G`. (I'm using Haskell notation, but that is just as valid in Scala-Cats.) — duplode, May 22 '20 at 17:19
@duplode is right and that's the way I think of it too, it's quite simple. If you look up the category theoretic definition you will see a lot of extra stuff, but that's all a formal way of expressing that "it must treat the type `a` as *opaque* and cannot, for example, make an exception when `a` is `Int`". This is also known as parametricity, or (gasp!) naturality — luqui, May 22 '20 at 18:51
@luqui Actually natural transformation **can** treat `Int` ... specially as long as naturality (commutative diagram from the [definition](https://en.wikipedia.org/wiki/Natural_transformation#Definition)) still holds. Just in such case naturality doesn't follow from parametricity *for free* and has to be checked manually. — Dmytro Mitin, May 22 '20 at 19:00
I don't know about Scala, but in Haskell `~>` is defined something like `type f ~> g = forall a. f a -> g a`. It just lets you write `[] ~> Maybe` instead of `[a] -> Maybe a`. — chepner, May 22 '20 at 19:04
I'm not sure if this is too much a simplification but if there is a function `nt` which is polymorphic in the type parameter of the involved functors `F` and `G` and which does not violate commutativity (pseudo code) `nt(mapOfF(f) (functorF)) == mapOfG(f) (nt(functorG))` then `nt` is a homomorphism or natural transformation between `F` and `G`. — , May 22 '20 at 19:16
@DmytroMitin, ok fine, I meant it cannot treat `a` specially, "extensionally" speaking. You can implement however you like as long as it ends up behaving that way. In any case, is there an example of a nontrivial such special treatment where commutativity still holds (I have my doubts...)? — luqui, May 22 '20 at 19:33
@luqui https://www.janis-voigtlaender.eu/papers/AutomaticallyGeneratingCounterexamplesToNaiveFreeTheorems.pdf — Dmytro Mitin, May 23 '20 at 02:40
@DmytroMitin I didn't read the whole paper but it looks like those counterexamples are in the wrong direction: they give definable functions which violate (naive) parametricity. To defend that n.t.s can treat types specially, I would need a function that *conforms* to parametricity but does not treat its type variable opaquely. (And something like `f_Int x = x + 0; f_a x = x` wouldn't count because it's the same function as `f x = x`). — luqui, May 23 '20 at 03:41
@DmytroMitin and you shan't find one. Here is [a proof](https://gist.github.com/luqui/cd4dffc6908c7eeace3da91ec470327f) — luqui, May 23 '20 at 05:10

Dmytro Mitin · Accepted Answer · 2020-05-23T02:32:15.980

I know it [natural transformation] is transformation from one category into other category.

Actually no. Transformation from category to category is functor (it maps objects to objects and morphisms to morphisms). Natural transformation is transformation from functor to functor (i.e. it's a morphism in category of functors).

Category of types in Scala is a category. Its objects are types, its morphisms are functions (not function types).

For example List and Option are functors. They map objects to objects (type A to type List[A], type A to type Option[A]) and morphisms to morphisms (function f: A => B to function _.map(f) : List[A] => List[B], function f: A => B to function _.map(f) : Option[A] => Option[B]).

For example headOption is a natural transformation (List ~> Option)

val headOption: (List ~> Option) = new (List ~> Option) {
  def apply[A](as: List[A]): Option[A] = as.headOption
}

or in Dotty

val headOption: [A] => List[A] => Option[A] = 
  [A] => (as: List[A]) => as.headOption

What is a natural transformation in haskell?

There is evolving sequence of abstractions:

category (with its objects and morphisms),
category of morphisms (its objects are morphisms, its morphisms are commutative squares),
category of categories (its objects are categories, its morphisms are functors),
category of functors (its objects are functors, its morphisms are natural transformations),
...

https://github.com/hmemcpy/milewski-ctfp-pdf/releases/tag/v1.3.0

https://www.youtube.com/playlist?list=PLbgaMIhjbmEnaH_LTkxLI7FMa2HsnawM_

Not everything can be naturally transformed and the question is, how do the author of library doobie know, that he can do the natural transformation from ConnectionIO ~> IO?

Actually if you have family of maps ConnectionIO[A] => IO[A] (A runs over all types) and this family is defined using parametric polymorphism (and not ad-hoc polymorphism, i.e. type classes, i.e. is defined without additional assumptions on types A) = parametricity, then naturality follows from parametricity "for free". This is one of "theorems for free"

https://bartoszmilewski.com/2014/09/22/parametricity-money-for-nothing-and-theorems-for-free/

https://www.reddit.com/r/haskellquestions/comments/6fkufo/free_theorems/

https://ttic.uchicago.edu/~dreyer/course/papers/wadler.pdf

Good introduction to free theorems