同构函数的重要性

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

长的问题：我试图从function编程和类别理论的概念之间，根据我不时听到的一些术语来做一些类比。 本质上，我试图把这个术语“解包”成具体的东西，然后我可以扩展。 那么我就可以用这个术语来理解我刚才在说什么了。 这总是很好。

我一直听到的这些术语之一是同构（Isomorphism） ，我认为这是关于function或function组合之间的等价性的推理。 我想知道是否有人能够提供一些常见模式的见解，其中同构的特性派上用场（函数式编程），以及所获得的任何副产品，例如来自同构函数推理的编译器优化。

Answer 1

我对同构的有争议的答案有一个小问题，因为同构的范畴论定义没有提及任何关于对象的东西。 为了明白为什么，让我们回顾一下这个定义。

定义

同构是一对态射（即函数）， f和g ，使得：

 f . g = id g . f = id 

这些态射被称为“iso”态射。 很多人不了解同构中的“态射”是指function而不是客体。 但是，你会说他们连接的对象是“同构的”，这是另一个答案所描述的。

请注意，同构的定义并没有说什么（ . ）， id或=必须是。 唯一的要求是，无论他们是什么，他们也满足类别法律：

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

组合（即（ . ））将两个态射连接成一个态射， id表示某种“身份”转换。 这意味着，如果我们的同构抵消了身份态度主义身份，那么你可以把它们看作彼此的逆。

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

 id x = x 

…和组成被定义为：

 (f . g) x = f (gx) 

…和两个函数是同构的，如果他们取消了身份函数id当你撰写他们。

形态与对象

然而，两个对象可以是同构的，有多种方式。 例如，给出以下两种types：

 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 

所以这就是为什么用两个物体相关的特定函数而不是两个物体来描述同构是比较好的，因为在满足同构规律的两个物体之间不一定有唯一的一对函数。

另外请注意，function是可逆的是不够的。 例如，下面的函数对不是同构的：

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

尽pipe在撰写f1 . g2时没有任何信息丢失f1 . g2 f1 . g2 ，即使最终状态具有相同的types，也不会返回到原始状态。

而且，同构不一定在具体的数据types之间。 下面是两个典型的同构不是在具体的代数数据types之间的一个例子，而是简单地把函数关联起来： curry和uncurry ：

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

用于同构

教会编码

同构的一种用法是将数据types作为函数进行编码。 例如， Bool同构于forall a . a -> a -> a forall a . a -> a -> a ：

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

确认f . g = id f . g = id和g . f = id g . f = id 。

Church编码数据types的好处在于它们有时候运行得更快（因为Church编码是continuation-passing风格的），它们可以用甚至没有代数数据types的语言支持的语言来实现。

翻译实现

有时候试图比较一个图书馆的某个function的实现与另一个图书馆的实现，如果你能certificate它们是同构的，那么你可以certificate它们同样强大。 而且，同构描述了如何将一个图书馆翻译成另一个图书馆。

例如，有两种方法可以从函子的签名中定义monad。 一个是由free软件包提供的免费monad，另一个是由operational软件包提供的操作语义。

如果你看看两个核心数据types，他们看起来不同，特别是他们的第二个构造函数：

 -- 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 fr = Pure r | Free (f (Free fr)) 

…但他们其实是同构的！ 这意味着两种方法同样强大，用一种方法编写的任何代码都可以用同构的方法机械地翻译成另一种方法。

同构不是函数

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

例如， Lenstypes（来自data-lens ）构成了一个类别，您可以在其中组合镜头并拥有镜头。 所以使用我们上面的数据types，我们可以定义两个同构的镜头：

 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 

请注意，有两个同构在玩。 一个是用于构build每个透镜（即f1和g1 ）的同构（也就是为什么构造函数被称为iso ），然后透镜本身也是同构的。 注意，在上述公式中，所使用的组合物（ . ）不是function组合物，而是透镜组合物，并且id不是身份函数，而是身份镜头：

 id = iso id id 

这意味着，如果我们构成了我们的两个镜头，结果应该与该身份镜头无法区分。

Answer 2

同构 u :: a -> b是一个具有反函数的函数 ，即另一个函数v :: b -> a这样关系

 u . v = id v . u = id 

满意。 你说如果它们之间存在同构，那么两种types是同构的。 这基本上意味着你可以认为它们是相同的types – 你可以用一个做什么，可以用另一个做。

函数的同构

两种functiontypes

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

是同构的，因为我们可以写

 u :: ((a,b) -> c) -> a -> b -> c uf = \xy -> f (x,y) v :: (a -> b -> c) -> (a,b) -> c vg = \(x,y) -> gxy 

你可以检查u . v u . v和v . u v . u都是id 。 事实上， u和v的function在curry和uncurry curry的名称中更为人所知。

同构与新型

每当我们使用一个新types的声明，我们都利用同构。 例如，状态monad的基本types是s -> (a,s) ，这可能有点混乱。 通过使用新types声明：

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

我们生成一个与s -> (a,s)同构的新types的State sa ，当我们使用它时，我们正在考虑具有可修改状态的函数。 我们还得到了一个方便的构造函数State和一个getter runState用于新types。

Monads和Comonads

对于一个更高级的观点，考虑使用上面我使用的curry和uncurry的同构。 Reader ratypes具有newtype声明

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

在monad的情况下，产生读者的函数因此具有types签名

 f :: a -> Reader rb 

相当于

 f :: a -> r -> b 

这是咖喱/同调的一半。 我们也可以定义CoReader ratypes：

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

可以做成一个comonad。 在那里，我们有一个函数cobind，或=>>它采取一个函数，采取一个coreader和产生一个原始types：

 g :: CoReader ra -> b 

这是同构的

 g :: (a,r) -> b 

但是我们已经看到a -> r -> b和(a,r) -> b是同构的，这给了我们一个不平凡的事实：读者monad（具有monadic绑定）和coreader comonad（具有comonadic cobind）是同构的以及！ 特别是，它们都可以用于相同的目的，即提供贯穿每个函数调用的全局环境。

Answer 3

考虑数据types。 例如，在Haskell中，如果存在一对以独特方式转换数据的函数，则可以将两种数据types视为同构的。 以下三种types是同构的：

 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 f . g = g . f = id f . g = g . f = id ，那么这两个函数是这两个types（对象）之间的同构。