同构函数的重要性

Question

简短问题：编程中（特别是函数式编程），同构函数的重要性是什么？

详细问题：我试图在范畴论的概念和函数式编程之间进行一些类比，基于我从时间到时间听到的术语。本质上，我正在尝试将这种术语 "拆包 "为具体的内容，然后再扩展。然后，我将能够使用术语，并理解自己在说些啥。这总是不错的。

其中一个我经常听到的术语是同构（Isomorphism），我了解这是关于推理函数或函数组合之间等价性的术语。我想知道是否有人可以提供一些常见模式的见解，在这些模式中同构属性非常方便（在函数式编程中），以及由此获得的任何副产品，例如通过推理同构函数获得的编译器优化。

- ThaDon

---

这是一个很好的问题。你是否正在创建一系列相关问题？如果是这样，你应该把链接收集到某个地方，并在你的个人资料中链接到该系列。 - Marcin

@Marcin 我确实是，我会在所有编译完成后通知你。 - ThaDon

不仅是一个好问题，而且对StackOverflow的运用很好！ - Jörg W Mittag

iso- 表示相等/等价：http://en.wiktionary.org/wiki/iso-#Etymology，而 -morph- 表示形状/形式：http://www.thefreedictionary.com/morph。因此，同构(isomorphism)是指两种类型之间的等价关系/函数，如何定义已经在下面非常好地解释了。 - Cetin Sert

Answer 1

我对isomorphism的顶级答案有一些异议，因为范畴论对isomorphism的定义并没有涉及到对象。为了理解这点，让我们回顾一下它的定义。

定义

isomorphism是一对态射（即函数）f和g，满足以下条件：

f . g = id
g . f = id

这些态射被称为“同构” 。很多人没有意识到同构中的“态射”指的是函数而不是对象。但是，你会说它们连接的对象是“同构”的，这就是另一个回答所描述的内容。

请注意，同构的定义并没有说明(.), id, 或=必须是什么。唯一的要求是，无论它们是什么，它们也必须满足范畴定律：

f . id = f
id . f = f
(f . g) . h = f . (g . h)

Composition（即（ . ））将两个态射合并为一个态射，而 id 表示某种“恒等”转换。这意味着，如果我们的同构被取消成恒等态射 id ，那么您可以将它们视为彼此的逆。

对于态射是函数的特定情况， id 被定义为恒等函数：

id x = x

...并且组合被定义为：

(f . g) x = f (g x)

如果两个函数在组合后得到恒等函数id，那么它们就是同构的。

态射与对象

然而，有多种方式可以使两个对象同构。例如，给定以下两种类型：

data T1 = A | B
data T2 = C | D

它们之间有两个同构：

f1 t1 = case t1 of
    A -> C
    B -> D
g1 t2 = case t2 of
    C -> A
    D -> B

(f1 . g1) t2 = case t2 of
    C -> C
    D -> D
(f1 . g1) t2 = t2
f1 . g1 = id :: T2 -> T2

(g1 . f1) t1 = case t1 of
    A -> A
    B -> B
(g1 . f1) t1 = t1
g1 . f1 = id :: T1 -> T1

f2 t1 = case t1 of
    A -> D
    B -> C
g2 t2 = case t2 of
    C -> B
    D -> A

f2 . g2 = id :: T2 -> T2
g2 . f2 = id :: T1 -> T1

因此，更好地描述同构应该是基于将两个对象相关的具体函数而不是两个对象，因为可能不存在一对唯一的函数满足同构定律。

另外，请注意函数可逆并不足够。例如，以下函数对不是同构：

f1 . g2 :: T2 -> T2
f2 . g1 :: T2 -> T2

尽管在组合 f1 . g2 时不会丢失任何信息，但即使最终状态具有相同的类型，也不会返回到原始状态。

此外，同构不一定是在具体数据类型之间。下面是两个经典同构示例，它们并不是在具体代数数据类型之间，而只是关联函数：curry 和 uncurry。

curry . uncurry = id :: (a -> b -> c) -> (a -> b -> c)
uncurry . curry = id :: ((a, b) -> c) -> ((a, b) -> c)

同构的用途

Church编码

同构的一个用途是将数据类型编码为函数，这称为Church编码。例如，Bool与forall a . a -> a -> a是同构的：

f :: Bool -> (forall a . a -> a -> a)
f True  = \a b -> a
f False = \a b -> b

g :: (forall a . a -> a -> a) -> Bool
g b = b True False

验证f.g=id和g.f=id。

使用Church编码数据类型的好处是它们有时运行更快（因为Church编码是延续传递风格），并且可以在根本没有对代数数据类型提供语言支持的语言中实现。

翻译实现

有时候人们会尝试比较一个库的某个特性的实现与另一个库的实现，如果你能证明它们是同构的，那么就可以证明它们同样强大。此外，同构描述了如何将一个库转换为另一个库。

例如，有两种方法可以从functor的签名定义monad。一种是由free包提供的自由monad，另一种是由operational包提供的操作语义。

如果您查看这两个核心数据类型，它们看起来不同，尤其是它们的第二个构造器：

-- modified from the original to not be a monad transformer
data Program instr a where
    Lift   :: a -> Program instr a
    Bind   :: Program instr b -> (b -> Program instr a) -> Program instr a
    Instr  :: instr a -> Program instr a

data Free f r = Pure r | Free (f (Free f r))

...但实际上它们是同构的！这意味着两种方法同样强大，任何用一种方法编写的代码都可以使用同构机械地转换为另一种方法。

不是函数的同构

此外，同构并不仅限于函数。它们实际上是为任何Category定义的，而Haskell有很多类别。这就是为什么以态射而不是数据类型来思考更有用的原因。

例如，Lens类型（来自data-lens）形成了一个范畴，您可以组合镜头并具有标识镜头。因此，使用我们上面的数据类型，我们可以定义两个同构的镜头：

lens1 = iso f1 g1 :: Lens T1 T2
lens2 = iso g1 f1 :: Lens T2 T1

lens1 . lens2 = id :: Lens T1 T1
lens2 . lens1 = id :: Lens T2 T2

请注意有两个同构在起作用。其中一个是用于构建每个镜头（即f1和g1）的同构（这也是为什么该构造函数被称为iso的原因），然后镜头本身也是同构。请注意，在上述公式中，使用的组合符号（.）不是函数组合而是镜头组合，而id不是标识函数，而是标识镜头：

id = iso id id

这意味着，如果我们组合这两个镜头，结果应该与恒等镜头无法区分。

- Gabriella Gonzalez

---

展示 Program 和 Free 之间的同构关系会有所帮助；我不能一眼看出它们之间的关系。 - Heatsink

我希望我能理解程序正在发生什么。作为它目前的定义有效吗？instr的作用是什么？我猜这可能需要编辑来纠正令人困惑的打字错误，我很高兴看到这一点，但我自己无法完全弄清楚如何编辑。 - pigworker

@pigworker 我从 operational 中复制粘贴了这段代码，但是去掉了基本单子使其成为普通单子而不是单子变换器。在这个过程中，我忘记从构造函数中删除 T，但我已经修复了它。 - Gabriella Gonzalez

@GabrielGonzalez instr有什么作用？ - pigworker

@pigworker的instr是自由单子基函子的“操作”定义。 operational包的教程详细介绍了它。 它基本上是使用Coyoneda构造变换的自由单子基函子，使用我在GADTs博客文章中描述的相同原理。 - Gabriella Gonzalez

Answer 2

同构映射u :: a -> b是一种具有逆映射的函数，即存在另一个函数v :: b -> a，满足以下关系：

u . v = id
v . u = id

如果两种类型之间存在同构映射，则它们是同构的。这基本上意味着您可以将它们视为相同的类型 - 您可以对其中任何一个执行的操作也可以对另一个执行。

函数的同构

这两个函数类型：

(a,b) -> c
a -> b -> c

它们同构，因为我们可以写成

u :: ((a,b) -> c) -> a -> b -> c
u f = \x y -> f (x,y)

v :: (a -> b -> c) -> (a,b) -> c
v g = \(x,y) -> g x y

你可以检查u . v和v . u都是id。事实上，函数u和v更常被称为curry和uncurry。

同构和 Newtypes

每当我们使用新类型声明时，我们就利用了同构性。例如，状态单子的基础类型是s -> (a,s)，这可能有点令人困惑。通过使用一个新类型声明：

newtype State s a = State { runState :: s -> (a,s) }

我们生成了一个新类型State s a，它与s -> (a,s)同构，并且清楚地表明我们在使用它时，正在考虑具有可修改状态的函数。我们还获得了方便的State构造函数和runState获取器来操作这个新类型。

Monad和Comonad

对于更高级的视角，请考虑使用curry和uncurry进行的同构。Reader r a类型具有新类型声明。

newType Reader r a = Reader { runReader :: r -> a }

在单子（monads）的背景下，产生一个reader的函数f，因此具有类型签名。

f :: a -> Reader r b

等同于

f :: a -> r -> b

这是curry/uncurry同构的其中一半。我们还可以定义CoReader r a类型：

newtype CoReader r a = CoReader { runCoReader :: (a,r) }

它可以转换为一个共同子类别，这里有一个 =>> 函数，可以将一个接受 coreader 并返回原始类型的函数传入：

g :: CoReader r a -> b

与...同构

g :: (a,r) -> b

但我们已经看到a -> r -> b和(a,r) -> b是同构的，这给我们带来了一个非平凡的事实：Reader Monad（通过单子绑定）和Coreader Comonad（通过共单子协同绑定）也是同构的！特别地，它们都可以用于相同的目的——提供贯穿每个函数调用的全局环境。

- Chris Taylor

Answer 3

以数据类型为基础进行思考。例如，在Haskell中，如果存在一对函数能够在两个数据类型之间唯一地转换数据，则可以将它们视为同构。以下三种类型彼此同构：

data Type1 a = Ax | Ay a
data Type2 a = Blah a | Blubb
data Maybe a = Just a | Nothing

你可以将转换它们之间的函数看作同构。这符合同构的范畴学概念。如果在Type1和Type2之间存在两个函数f和g，使得f.g=g.f=id，则这两个函数是这两个类型（对象）之间的同构。

- ertes

---

补充一点：像 f 和 g 这样的技术术语是“双射”。 - huon

使用 map，您还可以构建不同类型列表之间的同构；对于 fmap 和应用类型也是如此。 - Riccardo T.

那么，如果它们之间存在双射关系，数据类型就是同构的吗？ - Marcin

在下面的情况下，@ertes，id将是x吗？ func = f . g ... func x - ThaDon