Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

How to it is a natural transformation?

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?

like image 817
softshipper Avatar asked May 22 '20 17:05

softshipper


People also ask

What is meant by natural transformation?

Simply put, a natural transformation is a collection of maps from one diagram to another. And these maps are special in that they commute with the arrows in the diagrams. For example, in the picture below, the black arrows below comprise a natural transformation between two functors* F and G .

What is a natural isomorphism?

Definition 2 A natural isomorphism from F to G is an isomorphism in the functor category Funct(C,D), that is, a natural transformation η:F→G for which there exists a natural transformation ξ:G→F such that the compositions ξ∘η=1F and η∘ξ=1G are identity natural transformations.

Is a functor a category?

Functor categories serve as the hom-categories in the strict 2-category Cat. In the context of enriched category theory the functor category is generalized to the enriched functor category.

What is a representable functor?

In mathematics, particularly category theory, a representable functor is a certain functor from an arbitrary category into the category of sets.


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

like image 145
Dmytro Mitin Avatar answered Sep 18 '22 01:09

Dmytro Mitin