How to it is a natural transformation?
Asked Answered
W

1

5

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?

Words answered 22/5, 2020 at 17:7 Comment(11)
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).Cadell
@DmytroMitin could you please explain more in detail?Words
If F and G are Functors, 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.)Climatology
@Climatology 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!) naturalityJemima
@Jemima Actually natural transformation can treat Int ... specially as long as naturality (commutative diagram from the definition) still holds. Just in such case naturality doesn't follow from parametricity for free and has to be checked manually.Cadell
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.Algeria
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.Linear
@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...)?Jemima
@Jemima janis-voigtlaender.eu/papers/…Cadell
@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).Jemima
@DmytroMitin and you shan't find one. Here is a proofJemima
C
10

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

Cadell answered 22/5, 2020 at 18:15 Comment(0)

© 2022 - 2024 — McMap. All rights reserved.