我将从明显与编程相关的内容开始，然后添加一些数学内容，以使其尽可能具体和实际。

---

让我们引用一些计算机科学家的归纳法……

http://www.cs.umd.edu/~micinski/posts/2012-09-04-on-understanding-coinduction.html

归纳是关于有限数据的，共归纳是关于无限数据的。 无限数据的典型例子是惰性列表类型(a 流)。例如，假设我们有以下对象 记忆:

 let (pi : int list) = (* some function which computes the digits of
 π. *)

计算机无法保存所有π，因为它只有有限的数量 的内存!但它能做的是保存一个有限的程序 求任意长的π展开式。只要 因为你只使用列表的有限部分，你可以用它来计算 无限的列表，只要你需要。 但是，考虑下面的程序:

let print_third_element (k : int list) =   match k with
     | _ :: _ :: thd :: tl -> print thd


 print_third_element pi

This program should print the third digit of pi. But in some languages, any argument to a function is evaluated before being passed into a function (strict, not lazy, evaluation). If we use this reduction order, then our above program will run forever computing the digits of pi before it can be passed to our printer function (which never happens). Since the machine does not have infinite memory, the program will eventually run out of memory and crash. This might not be the best evaluation order.

http://adam.chlipala.net/cpdt/html/Coinductive.html

在Haskell这样的惰性函数式编程语言中，无限的数据结构 到处都是。无限的列表和更奇特的数据类型提供了方便 程序各部分之间通信的抽象。实现类似的 在许多情况下，没有无限惰性结构的便利性是必需的 控制流的杂技式反转。

http://www.alexandrasilva.org/#/talks.html

---

将环境数学上下文与通常的编程任务联系起来

什么是代数?

代数结构通常是这样的:

的东西 这东西能做什么

这听起来应该像带有1的对象。属性和2。方法。或者更好的是，它听起来应该像类型签名。

标准的数学例子包括单类⊃群⊃向量空间⊃“一个代数”。monooid类似于自动机:动词的序列(例如，f.g.h.h.nothing.f.g.f)。一个总是添加历史记录而从不删除它的git日志将是一个单类而不是一个组。如果你加上反函数(如负数、分数、根、删除累积的历史记录、修复破碎的镜子)，你会得到一个组。

组包含可以一起添加或减去的内容。例如，持续时间可以加在一起。(但《日期》不能。)持续时间存在于向量空间中(不仅仅是一个组)，因为它们也可以通过外部数字缩放。(伸缩类型签名:(数字，持续时间)→持续时间。)

代数向量空间还可以做另一件事:存在一些m::(T,T)→T。称它为“乘法”或不称它为“乘法”，因为一旦你离开整数，“乘法”(或“幂”)应该是什么就不那么明显了。

(这就是为什么人们期待(范畴论)普遍性质:告诉他们乘法应该做什么或像什么:

)

---

代数→代数

与乘法相比，用一种非任意的方式定义乘法更容易，因为从T→(T,T)你可以重复相同的元素。(“对角线映射”-类似于谱理论中的对角线矩阵/算子)

Counit通常是trace(对角线项的和)，尽管同样重要的是你的Counit做什么;Trace是矩阵的一个很好的答案。

一般来说，考虑对偶空间的原因是，在那个空间里思考更容易。例如，有时考虑法向量比考虑它的法向平面更容易，但你可以用向量控制平面(包括超平面)(现在我说的是熟悉的几何向量，就像在射线示踪器中)。

---

驯服(非)结构化数据

数学家可能会建模一些有趣的东西，比如TQFT，而程序员必须与之搏斗

dates/times (+ :: (Date,Duration) → Date), places (Paris ≠ (+48.8567,+2.3508)! It's a shape, not a point.), unstructured JSON which is supposed to be consistent in some sense, wrong-but-close XML, incredibly complex GIS data which should satisfy loads of sensible relations, regular expressions which meant something to you, but mean considerably less to perl. CRM that should hold all the executive's phone numbers and villa locations, his (now ex-) wife and kids' names, birthday and all the previous gifts, each of which should satisfy "obvious" relations (obvious to the customer) which are incredibly hard to code up, .....

计算机科学家在谈论共代数时，通常会想到集合运算，比如笛卡尔积。我相信这就是人们说“代数在Haskell中是共代数”的意思。但是在某种程度上，程序员必须建模复杂的数据类型，如地点、日期/时间和客户，并使这些模型尽可能地像真实世界(或至少是最终用户对真实世界的看法)，我相信对偶除了集合世界之外还可以有用。

关于(co)代数和(co)归纳法的教程应该会让你对计算机科学中的协同代数有一些了解。

下面是它的引用，以说服你，

In general terms, a program in some programming language manipulates data. During the development of computer science over the past few decades it became clear that an abstract description of these data is desirable, for example to ensure that one's program does not depend on the particular representation of the data on which it operates. Also, such abstractness facilitates correctness proofs. This desire led to the use of algebraic methods in computer science, in a branch called algebraic specification or abstract data type theory. The object of study are data types in themselves, using notions of techniques which are familiar from algebra. The data types used by computer scientists are often generated from a given collection of (constructor) operations,and it is for this reason that "initiality" of algebras plays such an important role. Standard algebraic techniques have proved useful in capturing various essential aspects of data structures used in computer science. But it turned out to be difficult to algebraically describe some of the inherently dynamical structures occurring in computing. Such structures usually involve a notion of state, which can be transformed in various ways. Formal approaches to such state-based dynamical systems generally make use of automata or transition systems, as classical early references. During the last decade the insight gradually grew that such state-based systems should not be described as algebras, but as so-called co-algebras. These are the formal dual of algebras, in a way which will be made precise in this tutorial. The dual property of "initiality" for algebras, namely finality turned out to be crucial for such co-algebras. And the logical reasoning principle that is needed for such final co-algebras is not induction but co-induction.

---

前奏，关于范畴论。 范畴论应该改名为函子论。 As范畴是定义函子时必须定义的。 (此外，为了定义自然变换，必须定义函子。)

什么是函子? 这是一种从一个集合到另一个集合的转换，保持了它们的结构。 (要了解更多细节，网上有很多很好的描述)。

什么是f代数? 这是函子的代数。 它只是关于函子的普遍适当性的研究。

它如何与计算机科学联系起来? 程序可以看作是一组结构化的信息。 程序的执行对应于对这一结构化信息集的修改。 执行时应该保留程序结构，这听起来不错。 然后，执行可以被看作是对这组信息的函子应用。 (定义程序的人)。

为什么是f -协代数? 程序在本质上是二元的，因为它们是由信息描述的，并且它们对信息起作用。 然后主要从两种方式查看组成程序和使程序发生变化的信息。

可以定义为程序正在处理的信息的数据。 状态，可以定义为程序共享的信息。

在这个阶段，我想说，

f -代数是对作用于数据宇宙(如这里所定义的)的函式变换的研究。 f -协代数是作用于状态宇宙(如这里所定义)的函子变换的研究。

在程序的生命周期中，数据和状态共存，它们相互完善。 它们是对偶的。

代数

我认为首先要理解代数的概念。这只是代数结构的一种推广，比如群，环，monooid等等。大多数情况下，这些东西是以集合的形式介绍的，但由于我们是在朋友之间，所以我将讨论Haskell类型。(不过我忍不住要用一些希腊字母——它们让一切看起来更酷!)

因此，代数只是一个类型τ，具有一些函数和恒等式。这些函数采用不同数量的τ类型参数，并产生一个τ:未加curry的，它们看起来都像(τ， τ，…，τ)→τ。它们还可以具有“恒等式”——τ元素，这些元素与某些函数具有特殊行为。

最简单的例子是单类。monoid是任何类型的τ，具有函数mappend∷(τ， τ)→τ和标识mzero∷τ。其他例子包括组(就像monoids一样，只是多了一个反向∷τ→τ函数)、环、格等。

所有的函数都作用于τ，但可能有不同的稀缺性。我们可以把它们写成τⁿ→τ，其中τⁿ映射到n τ的元组。这样，将恒等式视为τ⁰→τ是有意义的，其中τ⁰只是空元组()。所以我们现在可以简化代数的概念:它只是一些类型，上面有一些函数。

代数只是数学中被“分解”出来的一种常见模式，就像我们处理代码一样。人们注意到一大堆有趣的东西——前面提到的单点、群、格等等——都遵循类似的模式，所以他们把它抽象了出来。这样做的好处和编程一样:它创建了可重用的证明，并使某些类型的推理更容易。

F-Algebras

然而，我们还没有完全完成因式分解。到目前为止，我们有一堆函数τⁿ→τ。实际上，我们可以做一个巧妙的技巧，把它们组合成一个函数。具体来说，让我们看看monooid:我们有mappend∷(τ， τ)→τ和mempty∷()→τ。我们可以使用和类型- either将这些函数转换为单个函数。它看起来是这样的:

op ∷ Monoid τ ⇒ Either (τ, τ) () → τ
op (Left (a, b)) = mappend (a, b)
op (Right ())    = mempty

实际上，对于任何代数，我们都可以重复使用这个转换来将所有的τⁿ→τ函数组合成一个函数。(事实上，我们可以对任意数量的函数a→τ， b→τ等等任意a, b，....)

This lets us talk about algebras as a type τ with a single function from some mess of Eithers to a single τ. For monoids, this mess is: Either (τ, τ) (); for groups (which have an extra τ → τ operation), it's: Either (Either (τ, τ) τ) (). It's a different type for every different structure. So what do all these types have in common? The most obvious thing is that they are all just sums of products—algebraic data types. For example, for monoids, we could create a monoid argument type that works for any monoid τ:

data MonoidArgument τ = Mappend τ τ -- here τ τ is the same as (τ, τ)
                      | Mempty      -- here we can just leave the () out

我们可以对基团，环，晶格以及其他可能的结构做同样的事情。

这些类型还有什么特别之处呢?它们都是函子!例如:

instance Functor MonoidArgument where
  fmap f (Mappend τ τ) = Mappend (f τ) (f τ)
  fmap f Mempty        = Mempty

所以我们可以进一步推广代数的概念。它只是某个类型τ，对于某个函子f，它是一个函数f τ→τ。事实上，我们可以把它写成一个类型类:

class Functor f ⇒ Algebra f τ where
  op ∷ f τ → τ

这通常被称为“f -代数”，因为它由函子f决定。如果我们可以部分应用类型类，我们可以定义类似class Monoid = Algebra MonoidArgument的东西。

煤代数

现在，希望你们已经很好地掌握了代数是什么以及它如何只是普通代数结构的推广。那么什么是f -协代数呢?好吧，余数意味着它是一个代数的“对偶”——也就是说，我们取一个代数，翻转一些箭头。我在上面的定义中只看到一个箭头，所以我将翻转它:

class Functor f ⇒ CoAlgebra f τ where
  coop ∷ τ → f τ

就是这样!现在，这个结论可能看起来有点轻率。它告诉你什么是协代数，但并没有真正告诉你它是如何有用的，或者为什么我们关心它。一旦我找到或想出一两个很好的例子，我就会稍微谈到这一点:P。

类和对象

在阅读了一些内容之后，我认为我已经很好地了解了如何使用共代数来表示类和对象。我们有一个类型C，它包含类中对象的所有可能的内部状态;类本身是C语言上的协代数，它指定对象的方法和属性。

如代数例子所示，如果我们有一堆函数，比如a→τ和b→τ，对于任意a, b，…，我们可以使用和类型Either将它们组合成一个函数。对偶“概念”将结合一堆类型为τ→a， τ→b等的函数。我们可以使用和类型的对偶——一种乘积类型。因此，给定上面的两个函数(称为f和g)，我们可以创建一个单独的函数，如下所示:

both ∷ τ → (a, b)
both x = (f x, g x)

类型(a, a)是一个简单的函子，所以它当然符合我们关于f -协代数的概念。这个特殊的技巧让我们可以将一堆不同的函数(对于OOP来说是方法)打包成一个类型为τ→f τ的函数。

类型C的元素表示对象的内部状态。如果对象具有一些可读属性，那么它们必须能够依赖于状态。最明显的方法是使它们成为C的函数。因此，如果我们想要一个长度属性(例如object.length)，我们将有一个函数C→Int。

我们需要能够接受参数并修改状态的方法。为此，我们需要获取所有的参数并生成一个新的c。让我们想象一个setPosition方法，它接受一个x坐标和一个y坐标:object。setPosition(1,2)。它看起来像这样:C→((Int, Int)→C)。

这里的重要模式是对象的“方法”和“属性”将对象本身作为它们的第一个参数。这就像Python中的self形参，也像许多其他语言中的隐式This。协代数本质上只是封装了取自参数的行为:这就是C→F C中的第一个C。

让我们把它们放在一起。让我们想象一个有position属性，name属性和setPosition函数的类:

class C
  private
    x, y  : Int
    _name : String
  public
    name        : String
    position    : (Int, Int)
    setPosition : (Int, Int) → C

我们需要两个部分来表示这个类。首先，我们需要表示对象的内部状态;在这种情况下，它只保存两个int和一个String。(这是我们的c型)然后我们需要用协代数来表示这个类。

data C = Obj { x, y  ∷ Int
             , _name ∷ String }

我们有两个性质要写。它们非常琐碎:

position ∷ C → (Int, Int)
position self = (x self, y self)

name ∷ C → String
name self = _name self

现在我们只需要能够更新位置:

setPosition ∷ C → (Int, Int) → C
setPosition self (newX, newY) = self { x = newX, y = newY }

这就像一个带有显式self变量的Python类。现在我们有了一堆self→函数，我们需要将它们组合成一个用于协代数的函数。我们可以用一个简单的元组来实现:

coop ∷ C → ((Int, Int), String, (Int, Int) → C)
coop self = (position self, name self, setPosition self)

类型((Int, Int)， String， (Int, Int)→c) -对于任何c -都是函子，因此coop确实有我们想要的形式:函子f⇒c→f c。

给定这个，C和coop形成了一个协代数，它指定了我上面给出的类。您可以看到如何使用相同的技术为对象指定任意数量的方法和属性。

这让我们可以使用共代数推理来处理类。例如，我们可以引入“f -协代数同态”的概念来表示类之间的转换。这是一个听起来很可怕的术语它的意思是在保持结构的共代数之间的变换。这使得考虑将类映射到其他类要容易得多。

简而言之，f -协代数通过一堆属性和方法来表示一个类，这些属性和方法都依赖于包含每个对象内部状态的self参数。

其他类别

到目前为止，我们已经讨论了Haskell类型的代数和共代数。代数只是一个类型τ和一个函数f τ→τ，协代数只是一个类型τ和一个函数τ→f τ。

然而，没有什么能真正将这些想法与Haskell本身联系起来。事实上，它们通常是以集合和数学函数的形式引入的，而不是类型和Haskell函数。事实上，我们可以将这些概念推广到任何类别!

首先，我们需要一个函子F: C→C，即一个内函子。(所有Haskell函子实际上都是Hask→Hask的内函子。)那么，一个代数就是C中的一个对象A，具有态射F A→A。一个协代数除了A→F A之外是相同的。

考虑其他类别我们能得到什么?我们可以在不同的语境中使用相同的概念。喜欢了单体。在Haskell中，monad是某种类型的M∷★→★，有三种操作:

map      ∷ (α → β) → (M α → M β)
return   ∷ α → M α
join     ∷ M (M α) → M α

map函数只是证明了M是一个函子。所以我们可以说一个单子只是一个带有两个操作的函子:返回和连接。

函子本身形成一个范畴，它们之间的态射就是所谓的“自然变换”。自然变换是一种将一个函子变换为另一个函子同时保持其结构的方法。这里有一篇很好的文章来解释这个想法。它讲的是concat，也就是对列表的连接。

对于Haskell函子，两个函子的组合本身就是一个函子。在伪代码中，我们可以这样写:

instance (Functor f, Functor g) ⇒ Functor (f ∘ g) where
  fmap fun x = fmap (fmap fun) x

这有助于我们把接合看作是f·f→f的映射。接合的类型是∀α。F (F α)→F α。直观地，我们可以看到对所有类型α都有效的函数如何被认为是f的变换。

Return是一个类似的转换。其类型为∀α。α→f α。这看起来不同——第一个α不在函子中!幸运的是，我们可以通过在那里添加一个单位函子来解决这个问题:∀α。恒等α→f α。返回的是一个变换Identity→f。

现在我们可以把单子看成是基于某个函子f的代数，并进行f·f→f和恒等式→f的操作。这是不是很眼熟?它非常类似于一个单类，它只是某种类型的τ，带有操作τ × τ→τ和()→τ。

单子和单类很像，只是没有类型，而是有函子。这是同样的代数，只是类别不同而已。(据我所知，这就是“单子只是内函子范畴中的一个单子”这句话的来源。)

现在，我们有这两种操作:f·f→f和恒等式→f。要得到相应的余代数，我们只需翻转箭头。这就给了我们两种新的操作:f→f重重f和f→恒等式。我们可以通过添加如上所述的类型变量将它们转换为Haskell类型，从而得到∀α。F α→F (F α)和∀α。F α→α。这看起来就像一个comonad的定义:

class Functor f ⇒ Comonad f where
  coreturn ∷ f α → α
  cojoin   ∷ f α → f (f α)

所以共数就是内函子范畴中的共代数。

f -代数和f -共代数是用于推理归纳类型(或递归类型)的数学结构。

F-algebras

我们先从f代数开始。我会尽量讲得简单些。

我猜你们知道什么是递归类型。例如，这是一个整数列表的类型:

data IntList = Nil | Cons (Int, IntList)

很明显，它是递归的——事实上，它的定义是指它自己。它的定义由两个数据构造函数组成，它们有以下类型:

Nil  :: () -> IntList
Cons :: (Int, IntList) -> IntList

注意，我已经写了Nil类型as () -> IntList，而不是简单的IntList。从理论的角度来看，这实际上是等价的类型，因为()类型只有一个居住者。

如果我们用更集论的方式来写这些函数的签名，我们会得到

Nil  :: 1 -> IntList
Cons :: Int × IntList -> IntList

其中1是一个单位集(只有一个元素的集合)，a × B操作是两个集合a和B的叉乘(即对(a, B)的集合，其中a经过a的所有元素，B经过B的所有元素)。

两个集合A和B的不相交并集是集合A | B，它是集合{(A, 1): A在A}和{(B, 2): B在B}的并集。从本质上讲，它是a和B中所有元素的集合，但每个元素都“标记”为属于a或B，所以当我们从a | B中选择任何元素时，我们马上就能知道这个元素是来自a还是来自B。

我们可以“联接”Nil和Cons函数，因此它们将形成一个单独的函数，在集合1 | (Int × IntList)上工作:

Nil|Cons :: 1 | (Int × IntList) -> IntList

实际上，如果Nil|Cons函数应用于()值(显然，属于1 | (Int × IntList)集)，那么它的行为就好像它是Nil;如果Nil|Cons应用于任何类型(Int, IntList)的值(这些值也在集合1 | (Int × IntList)中)，则表现为Cons。

现在考虑另一种数据类型:

data IntTree = Leaf Int | Branch (IntTree, IntTree)

它有以下构造函数:

Leaf   :: Int -> IntTree
Branch :: (IntTree, IntTree) -> IntTree

也可以连接到一个函数:

Leaf|Branch :: Int | (IntTree × IntTree) -> IntTree

可以看出，这两个连接函数都有相似的类型:它们看起来都像

f :: F T -> T

其中F是一种转换，它采用我们的类型，并给出更复杂的类型，它由x和|操作组成，T的用法，可能还有其他类型。例如，对于IntList和intreree, F看起来如下所示:

F1 T = 1 | (Int × T)
F2 T = Int | (T × T)

我们可以马上注意到任何代数类型都可以这样写。事实上，这就是为什么它们被称为“代数的”:它们由许多其他类型的“和”(并)和“积”(叉积)组成。

现在我们可以定义f -代数。f -代数只是一对(T, f)，其中T是某种类型，f是类型f:: f T -> T的函数。在我们的例子中，f -代数是(IntList, Nil|Cons)和(IntTree, Leaf|Branch)。但是请注意，尽管f函数的类型对每个f都是一样的，T和f本身可以是任意的。例如，对于某些g和h， (String, g:: 1 | (Int x String) -> String)或(Double, h:: Int | (Double, Double) -> Double)对于相应的F也是F代数。

然后我们可以引入f代数同态和初始f代数，它们有非常有用的性质。事实上，(IntList, Nil|Cons)是一个初始的f1代数，(IntTree, Leaf|Branch)是一个初始的f2代数。我不会给出这些术语和属性的确切定义，因为它们比需要的更加复杂和抽象。

尽管如此，(IntList, Nil|Cons)是f -代数的事实允许我们在这种类型上定义类折叠函数。如你所知，fold是一种将一些递归数据类型转换为一个有限值的操作。例如，我们可以将一个整数列表折叠成一个值，这个值是列表中所有元素的和:

foldr (+) 0 [1, 2, 3, 4] -> 1 + 2 + 3 + 4 = 10

可以在任何递归数据类型上泛化这种操作。

下面是foldr函数的签名:

foldr :: ((a -> b -> b), b) -> [a] -> b

注意，我使用大括号将前两个参数与最后一个参数分开。这不是真正的foldr函数，但它与它是同构的(也就是说，您可以很容易地从一个得到另一个，反之亦然)。部分应用的foldr将具有以下签名:

foldr ((+), 0) :: [Int] -> Int

我们可以看到，这是一个函数，它接受一个整数列表并返回一个整数。让我们根据IntList类型定义这样的函数。

sumFold :: IntList -> Int
sumFold Nil         = 0
sumFold (Cons x xs) = x + sumFold xs

我们看到这个函数由两部分组成:第一部分定义了这个函数在IntList的Nil部分的行为，第二部分定义了这个函数在Cons部分的行为。

现在假设我们不是用Haskell编程，而是用某种语言编程，这种语言允许在类型签名中直接使用代数类型(好吧，技术上Haskell允许通过元组和b数据类型使用代数类型，但这会导致不必要的冗长)。考虑一个函数:

reductor :: () | (Int × Int) -> Int
reductor ()     = 0
reductor (x, s) = x + s

可以看出，约简器是类型F1 Int -> Int的函数，就像F-algebra的定义一样!的确，这个pair (Int, reductor)是一个f1代数。

Because IntList is an initial F1-algebra, for each type T and for each function r :: F1 T -> T there exist a function, called catamorphism for r, which converts IntList to T, and such function is unique. Indeed, in our example a catamorphism for reductor is sumFold. Note how reductor and sumFold are similar: they have almost the same structure! In reductor definition s parameter usage (type of which corresponds to T) corresponds to usage of the result of computation of sumFold xs in sumFold definition.

为了让它更清晰，帮助你看到模式，这里有另一个例子，我们再次从产生的折叠函数开始。考虑将第一个参数附加到第二个参数的appappfunction:

(append [4, 5, 6]) [1, 2, 3] = (foldr (:) [4, 5, 6]) [1, 2, 3] -> [1, 2, 3, 4, 5, 6]

这是它在IntList中的样子:

appendFold :: IntList -> IntList -> IntList
appendFold ys ()          = ys
appendFold ys (Cons x xs) = x : appendFold ys xs

同样，让我们试着写出约简式:

appendReductor :: IntList -> () | (Int × IntList) -> IntList
appendReductor ys ()      = ys
appendReductor ys (x, rs) = x : rs

appendFold是appendReductor的变形，它将IntList转换为IntList。

因此，本质上，f代数允许我们在递归数据结构上定义“折叠”，即将结构减少到某个值的操作。

F-煤代数

f -共代数是f -代数的对偶项。它们允许我们为递归数据类型定义展开，也就是说，一种从某些值构造递归结构的方法。

假设你有以下类型:

data IntStream = Cons (Int, IntStream)

这是一个无限的整数流。它唯一的构造函数类型如下:

Cons :: (Int, IntStream) -> IntStream

或者用集合来表示

Cons :: Int × IntStream -> IntStream

Haskell允许你在数据构造函数上进行模式匹配，所以你可以在IntStreams上定义以下函数:

head :: IntStream -> Int
head (Cons (x, xs)) = x

tail :: IntStream -> IntStream
tail (Cons (x, xs)) = xs

你可以自然地将这些函数“连接”成IntStream类型的单个函数-> Int × IntStream:

head&tail :: IntStream -> Int × IntStream
head&tail (Cons (x, xs)) = (x, xs)

请注意函数的结果与IntStream类型的代数表示是如何一致的。类似的事情也可以用于其他递归数据类型。也许你已经注意到了这个模式。我指的是类型函数族

g :: T -> F T

其中T是某种类型。从现在开始，我们将定义

F1 T = Int × T

现在，F-协代数是一对(T, g)，其中T是类型，g是类型g:: T -> F T的函数。例如，(IntStream, head&tail)是f1 -协代数。同样，就像在f代数中一样，g和T可以是任意的，例如，(String, h:: String -> Int x String)也是某个h的f1共代数。

在所有的f -共代数中，有所谓的终端f -共代数，它与初始f -代数对偶。例如，IntStream是一个终端f -协代数。这意味着对于每个类型T和每个函数p:: T -> F1 T都存在一个函数，称为变形，它将T转换为IntStream，并且这个函数是唯一的。

考虑下面的函数，它从给定的整数开始生成一个连续的整数流:

nats :: Int -> IntStream
nats n = Cons (n, nats (n+1))

现在让我们检查一个函数natsBuilder:: Int -> F1 Int，即natsBuilder:: Int -> Int × Int:

natsBuilder :: Int -> Int × Int
natsBuilder n = (n, n+1)

同样，我们可以看到nats和natsBuilder之间的一些相似之处。这与我们之前观察到的还原率和折线之间的联系非常相似。nats是natsBuilder的变形。

另一个例子，一个函数接受一个值和一个函数，并返回该函数对该值的连续应用的流:

iterate :: (Int -> Int) -> Int -> IntStream
iterate f n = Cons (n, iterate f (f n))

它的构造函数如下:

iterateBuilder :: (Int -> Int) -> Int -> Int × Int
iterateBuilder f n = (n, f n)

那么iterate是iterateBuilder的变形。

结论

因此，简而言之，f -代数允许定义折叠，也就是说，将递归结构减少到单个值的操作，而f -共代数允许做相反的事情:从单个值构造一个[潜在的]无限结构。

事实上在Haskell中f -代数和f -共代数是重合的。这是一个非常好的属性，它是每个类型中存在“底部”值的结果。因此，在Haskell中，可以为每个递归类型创建折叠和展开。然而，这背后的理论模型比我上面所介绍的要复杂得多，所以我刻意回避了它。

我将从明显与编程相关的内容开始，然后添加一些数学内容，以使其尽可能具体和实际。

---

让我们引用一些计算机科学家的归纳法……

http://www.cs.umd.edu/~micinski/posts/2012-09-04-on-understanding-coinduction.html

归纳是关于有限数据的，共归纳是关于无限数据的。 无限数据的典型例子是惰性列表类型(a 流)。例如，假设我们有以下对象 记忆:

 let (pi : int list) = (* some function which computes the digits of
 π. *)

计算机无法保存所有π，因为它只有有限的数量 的内存!但它能做的是保存一个有限的程序 求任意长的π展开式。只要 因为你只使用列表的有限部分，你可以用它来计算 无限的列表，只要你需要。 但是，考虑下面的程序:

let print_third_element (k : int list) =   match k with
     | _ :: _ :: thd :: tl -> print thd


 print_third_element pi

This program should print the third digit of pi. But in some languages, any argument to a function is evaluated before being passed into a function (strict, not lazy, evaluation). If we use this reduction order, then our above program will run forever computing the digits of pi before it can be passed to our printer function (which never happens). Since the machine does not have infinite memory, the program will eventually run out of memory and crash. This might not be the best evaluation order.

http://adam.chlipala.net/cpdt/html/Coinductive.html

在Haskell这样的惰性函数式编程语言中，无限的数据结构 到处都是。无限的列表和更奇特的数据类型提供了方便 程序各部分之间通信的抽象。实现类似的 在许多情况下，没有无限惰性结构的便利性是必需的 控制流的杂技式反转。

http://www.alexandrasilva.org/#/talks.html

---

将环境数学上下文与通常的编程任务联系起来

什么是代数?

代数结构通常是这样的:

的东西 这东西能做什么

这听起来应该像带有1的对象。属性和2。方法。或者更好的是，它听起来应该像类型签名。

标准的数学例子包括单类⊃群⊃向量空间⊃“一个代数”。monooid类似于自动机:动词的序列(例如，f.g.h.h.nothing.f.g.f)。一个总是添加历史记录而从不删除它的git日志将是一个单类而不是一个组。如果你加上反函数(如负数、分数、根、删除累积的历史记录、修复破碎的镜子)，你会得到一个组。

组包含可以一起添加或减去的内容。例如，持续时间可以加在一起。(但《日期》不能。)持续时间存在于向量空间中(不仅仅是一个组)，因为它们也可以通过外部数字缩放。(伸缩类型签名:(数字，持续时间)→持续时间。)

代数向量空间还可以做另一件事:存在一些m::(T,T)→T。称它为“乘法”或不称它为“乘法”，因为一旦你离开整数，“乘法”(或“幂”)应该是什么就不那么明显了。

(这就是为什么人们期待(范畴论)普遍性质:告诉他们乘法应该做什么或像什么:

)

---

代数→代数

与乘法相比，用一种非任意的方式定义乘法更容易，因为从T→(T,T)你可以重复相同的元素。(“对角线映射”-类似于谱理论中的对角线矩阵/算子)

Counit通常是trace(对角线项的和)，尽管同样重要的是你的Counit做什么;Trace是矩阵的一个很好的答案。

一般来说，考虑对偶空间的原因是，在那个空间里思考更容易。例如，有时考虑法向量比考虑它的法向平面更容易，但你可以用向量控制平面(包括超平面)(现在我说的是熟悉的几何向量，就像在射线示踪器中)。

---

驯服(非)结构化数据

数学家可能会建模一些有趣的东西，比如TQFT，而程序员必须与之搏斗

dates/times (+ :: (Date,Duration) → Date), places (Paris ≠ (+48.8567,+2.3508)! It's a shape, not a point.), unstructured JSON which is supposed to be consistent in some sense, wrong-but-close XML, incredibly complex GIS data which should satisfy loads of sensible relations, regular expressions which meant something to you, but mean considerably less to perl. CRM that should hold all the executive's phone numbers and villa locations, his (now ex-) wife and kids' names, birthday and all the previous gifts, each of which should satisfy "obvious" relations (obvious to the customer) which are incredibly hard to code up, .....

计算机科学家在谈论共代数时，通常会想到集合运算，比如笛卡尔积。我相信这就是人们说“代数在Haskell中是共代数”的意思。但是在某种程度上，程序员必须建模复杂的数据类型，如地点、日期/时间和客户，并使这些模型尽可能地像真实世界(或至少是最终用户对真实世界的看法)，我相信对偶除了集合世界之外还可以有用。