简短的问题：同构函数在编程（即函数式编程）中的重要性是什么？
长问题：我试图根据我不时听到的一些术语，在函数式编程和类别理论中的概念之间进行一些类比。本质上，我试图将这些术语“解包”成具体的东西，然后我可以扩展。然后，我将能够使用术语，了解我在说什么。这总是很好。
我一直听到的这些术语之一是Isomorphism，我认为这是关于函数或函数组合之间等价的推理。我想知道是否有人可以提供一些关于同构属性派上用场的常见模式（在函数式编程中）的一些见解，以及获得的任何副产品，例如对同构函数进行推理的编译器优化。
我对同构的赞成答案提出了一点问题，因为同构的范畴论定义对对象没有任何说明。要了解原因，让我们回顾一下定义。
同构是一对态射（即函数）f和g，这样：
f . g = id
g . f = id
这些态射然后被称为“iso”态射。很多人没有注意到同构中的“态射”是指函数而不是对象。但是，您会说它们连接的对象是“同构的”，这就是另一个答案所描述的。
请注意，同构的定义并没有说明 ( .) id、 或=必须是什么。唯一的要求是，无论它们是什么，它们也满足类别法则：
f . id = f
id . f = f
(f . g) . h = f . (g . h)
组合（即 ( .)）将两个态射连接成一个态射，并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 编码为函数。例如，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-encoding 是连续传递样式），并且它们可以用甚至根本不支持代数数据类型的语言来实现。
有时有人试图将一个库的某些功能实现与另一个库的实现进行比较，如果你能证明它们是同构的，那么你就可以证明它们同样强大。此外，同构描述了如何将一个库转换为另一个库。
例如，有两种方法可以提供从函子的签名定义单子的能力。一个是免费的 monad，由free包提供，另一个是操作语义，由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类型 (from 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
这意味着如果我们组合两个镜头，结果应该与那个身份镜头没有区别。
同构 是一个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。
每当我们使用新类型声明时，我们都会利用同构。例如，state monad 的底层类型s -> (a,s)可能有点令人困惑。通过使用新类型声明：
newtype State s a = State { runState :: s -> (a,s) }
我们生成了一个新类型State s a，它同构s -> (a,s)并且在我们使用它时很清楚，我们正在考虑具有可修改状态的函数。我们还为新类型获得了一个方便的构造函数State和一个 getter runState。
对于更高级的观点，请考虑使用curry和uncurry我上面使用的同构。该Reader r a类型具有 newtype 声明
newType Reader r a = Reader { runReader :: r -> a }
在 monad 的上下文中，f产生 reader 的函数因此具有类型签名
f :: a -> Reader r b
这相当于
f :: a -> r -> b
这是咖喱/非咖喱同构的一半。我们还可以定义CoReader r a类型：
newtype CoReader r a = CoReader { runCoReader :: (a,r) }
可以制成comonad。我们有一个函数 cobind，或者=>>它接受一个函数，该函数接受一个 coreader 并产生一个原始类型：
g :: CoReader r a -> b
这是同构的
g :: (a,r) -> b
但是我们已经看到a -> r -> b并且(a,r) -> b是同构的，这给了我们一个重要的事实：reader monad（具有 monadic 绑定）和 coreader comonad（具有 comonadic cobind）也是同构的！特别是，它们都可以用于相同的目的——提供一个贯穿每个函数调用的全局环境。
考虑数据类型。例如，在 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那么这两个函数是这两种类型（对象）之间的同构。