Menu
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?
817
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 .
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.
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.
In mathematics, particularly category theory, a representable functor is a certain functor from an arbitrary category into the category of sets.
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:
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
145
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With
