How to it is a natural transformation?

user_1743843 0
Viewed 786

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?

parametric-polymorphism category-theory scala functional-programming haskell
1 Answers

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

user_52496210
Related