它如何是自然的转变？答案

【问题标题】：How to it is a natural transformation?它如何是自然的转变？
【发布时间】：2020-05-22 17:07:10
【问题描述】：

我将使用很棒的库https://tpolecat.github.io/doobie/，它功能齐全。

我正在通过first example 并且我认出了：

Transactor 是一种知道如何连接到数据库的数据类型，分发连接，并清理它们；有了这些知识可以转换ConnectionIO ~> IO，这给了我们一个可以运行的程序。

ConnectionIO ~> IO是范畴论中的自然变换，但一直没有完全理解，究竟什么是自然变换。

但是，我知道这是从一个类别到另一个类别的转变。例如：

F[A] ~> G[A]

是从类别F 到G 的自然转换，而不更改内容。

不是所有东西都可以自然转化，问题是library doobie的作者怎么知道，他可以从ConnectionIO ~> IO进行自然转化？

【问题讨论】：

但是，我知道这是从一个类别到另一个类别的转换。 不。从类别到类别的转换是函子（它将对象映射到对象，态射到态射）。自然转换是从函子到函子的转换（即它是函子范畴中的态射）。
如果F 和G 是Functors，任何forall a. F a -> G a 函数都是从F 到G 的自然转换。（我使用的是 Haskell 表示法，但这在 Scala-Cats 中同样有效。）
@duplode 是对的，我也是这么想的，很简单。如果您查看类别理论定义，您会看到很多额外的东西，但这只是表达“它必须将类型 a 视为 opaque 并且不能，例如，当a 是Int 时例外。这也称为参数性，或（喘气！）自然性
我不确定这是否过于简化，但如果有一个函数 nt 在所涉及的仿函数 F 和 G 的类型参数中是多态的，并且它确实不违反交换律（伪代码）nt(mapOfF(f) (functorF)) == mapOfG(f) (nt(functorG)) 那么nt 是F 和G 之间的同态或自然变换。
@DmytroMitin 你找不到。这里是a proof

标签： scala haskell functional-programming category-theory parametric-polymorphism

【解决方案1】：

我知道[自然转变]是从一个类别到另一个类别的转变。

其实没有。从范畴到范畴的转换是函子（它将对象映射到对象，态射到态射）。自然转换是从函子到函子的转换（即，它是函子类别中的态射）。

Scala 中的类型类别是category。它的对象是类型，它的morphisms 是函数（不是函数类型）。

例如List 和Option 是functors。它们将对象映射到对象（类型A 到类型List[A]，类型A 到类型Option[A]）和态射到态射（函数f: A => B 到函数_.map(f) : List[A] => List[B]，函数f: A => B 到函数_.map(f) : Option[A] => Option[B] )。

例如headOption 是natural transformation (List ~> Option)

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

或在 Dotty 中

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

What is a natural transformation in haskell?

存在不断发展的抽象序列：

类别（及其对象和态射），
态射的范畴（它的对象是态射，它的态射是交换平方），
范畴的范畴（它的对象是范畴，它的态射是函子），
函子的范畴（它的对象是函子，它的态射是自然变换），
...

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

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

并非所有事物都可以自然转化，问题是，如何 library doobie 的作者知道吗，他可以做到自然从ConnectionIO ~> IO转换？

实际上，如果您有一系列映射 ConnectionIO[A] => IO[A]（A 运行在所有类型上）并且这个系列是使用参数多态性定义的（而不是临时多态性，即类型类，即在没有对类型 A) = 参数化 的额外假设的情况下定义，那么自然性从参数化“免费”得出。这是“免费定理”之一

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

【讨论】：