scala - 在编程的上下文中，“代数”是什么意思？

Question

我在函数式编程和 PLT 圈子中多次听到“代数”这个词，尤其是在讨论对象、共单子、透镜等时。谷歌搜索这个术语会给出对这些结构进行数学描述的页面，这对我来说非常难以理解。任何人都可以解释一下余代数在编程环境中的含义，它们的意义是什么，以及它们与对象和共子的关系？

Answer 1

Answer 2

F-algebras and F-coalgebras are mathematical structures which are instrumental in reasoning about inductive types (or recursive types).

F-algebras

We'll start first with F-algebras. I will try to be as simple as possible.

I guess you know what is a recursive type. For example, this is a type for a list of integers:

data IntList = Nil | Cons (Int, IntList)

It is obvious that it is recursive - indeed, its definition refers to itself. Its definition consists of two data constructors, which have the following types:

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

Note that I have written type of Nil as () -> IntList, not simply IntList. These are in fact equivalent types from the theoretical point of view, because () type has only one inhabitant.

If we write signatures of these functions in a more set-theoretical way, we will get

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

where 1 is a unit set (set with one element) and A × B operation is a cross product of two sets A and B (that is, set of pairs (a, b) where a goes through all elements of A and b goes through all elements of B).

Disjoint union of two sets A and B is a set A | B which is a union of sets {(a, 1) : a in A} and {(b, 2) : b in B}. Essentially it is a set of all elements from both A and B, but with each of this elements 'marked' as belonging to either A or B, so when we pick any element from A | B we will immediately know whether this element came from A or from B.

We can 'join' Nil and Cons functions, so they will form a single function working on a set 1 | (Int × IntList):

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

Indeed, if Nil|Cons function is applied to () value (which, obviously, belongs to 1 | (Int × IntList) set), then it behaves as if it was Nil; if Nil|Cons is applied to any value of type (Int, IntList) (such values are also in the set 1 | (Int × IntList), it behaves as Cons.

Now consider another datatype:

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

It has the following constructors:

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

which also can be joined into one function:

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

It can be seen that both of this joined functions have similar type: they both look like

f :: F T -> T

where F is a kind of transformation which takes our type and gives more complex type, which consists of x and | operations, usages of T and possibly other types. For example, for IntList and IntTree F looks as follows:

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

We can immediately notice that any algebraic type can be written in this way. Indeed, that is why they are called 'algebraic': they consist of a number of 'sums' (unions) and 'products' (cross products) of other types.

Now we can define F-algebra. F-algebra is just a pair (T, f), where T is some type and f is a function of type f :: F T -> T. In our examples F-algebras are (IntList, Nil|Cons) and (IntTree, Leaf|Branch). Note, however, that despite that type of f function is the same for each F, T and f themselves can be arbitrary. For example, (String, g :: 1 | (Int x String) -> String) or (Double, h :: Int | (Double, Double) -> Double) for some g and h are also F-algebras for corresponding F.

Afterwards we can introduce F-algebra homomorphisms and then initial F-algebras, which have very useful properties. In fact, (IntList, Nil|Cons) is an initial F1-algebra, and (IntTree, Leaf|Branch) is an initial F2-algebra. I will not present exact definitions of these terms and properties since they are more complex and abstract than needed.

Nonetheless, the fact that, say, (IntList, Nil|Cons) is F-algebra allows us to define fold-like function on this type. As you know, fold is a kind of operation which transforms some recursive datatype in one finite value. For example, we can fold a list of integer into a single value which is a sum of all elements in the list:

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

It is possible to generalize such operation on any recursive datatype.

The following is a signature of foldr function:

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

Note that I have used braces to separate first two arguments from the last one. This is not real foldr function, but it is isomorphic to it (that is, you can easily get one from the other and vice versa). Partially applied foldr will have the following signature:

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

We can see that this is a function which takes a list of integers and returns a single integer. Let's define such function in terms of our IntList type.

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

We see that this function consists of two parts: first part defines this function's behavior on Nil part of IntList, and second part defines function's behavior on Cons part.

Now suppose that we are programming not in Haskell but in some language which allows usage of algebraic types directly in type signatures (well, technically Haskell allows usage of algebraic types via tuples and Either a b datatype, but this will lead to unnecessary verbosity). Consider a function:

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

It can be seen that reductor is a function of type F1 Int -> Int, just as in definition of F-algebra! Indeed, the pair (Int, reductor) is an F1-algebra.

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.

Just to make it more clear and help you see the pattern, here is another example, and we again begin from the resulting folding function. Consider append function which appends its first argument to second one:

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

This how it looks on our IntList:

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

Again, let's try to write out the reductor:

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

appendFold is a catamorphism for appendReductor which transforms IntList into IntList.

So, essentially, F-algebras allow us to define 'folds' on recursive datastructures, that is, operations which reduce our structures to some value.

F-coalgebras

F-coalgebras are so-called 'dual' term for F-algebras. They allow us to define unfolds for recursive datatypes, that is, a way to construct recursive structures from some value.

Suppose you have the following type:

data IntStream = Cons (Int, IntStream)

This is an infinite stream of integers. Its only constructor has the following type:

Cons :: (Int, IntStream) -> IntStream

Or, in terms of sets

Cons :: Int × IntStream -> IntStream

Haskell allows you to pattern match on data constructors, so you can define the following functions working on IntStreams:

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

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

You can naturally 'join' these functions into single function of type IntStream -> Int × IntStream:

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

Notice how the result of the function coincides with algebraic representation of our IntStream type. Similar thing can also be done for other recursive data types. Maybe you already have noticed the pattern. I'm referring to a family of functions of type

g :: T -> F T

where T is some type. From now on we will define

F1 T = Int × T

Now, F-coalgebra is a pair (T, g), where T is a type and g is a function of type g :: T -> F T. For example, (IntStream, head&tail) is an F1-coalgebra. Again, just as in F-algebras, g and T can be arbitrary, for example,(String, h :: String -> Int x String) is also an F1-coalgebra for some h.

Among all F-coalgebras there are so-called terminal F-coalgebras, which are dual to initial F-algebras. For example, IntStream is a terminal F-coalgebra. This means that for every type T and for every function p :: T -> F1 T there exist a function, called anamorphism, which converts T to IntStream, and such function is unique.

Consider the following function, which generates a stream of successive integers starting from the given one:

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

Now let's inspect a function natsBuilder :: Int -> F1 Int, that is, natsBuilder :: Int -> Int × Int:

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

Again, we can see some similarity between nats and natsBuilder. It is very similar to the connection we have observed with reductors and folds earlier. nats is an anamorphism for natsBuilder.

Another example, a function which takes a value and a function and returns a stream of successive applications of the function to the value:

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

Its builder function is the following one:

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

Then iterate is an anamorphism for iterateBuilder.

Conclusion

So, in short, F-algebras allow to define folds, that is, operations which reduce recursive structure down into a single value, and F-coalgebras allow to do the opposite: construct a [potentially] infinite structure from a single value.

In fact in Haskell F-algebras and F-coalgebras coincide. This is a very nice property which is a consequence of presence of 'bottom' value in each type. So in Haskell both folds and unfolds can be created for every recursive type. However, theoretical model behind this is more complex than the one I have presented above, so I deliberately have avoided it.

Hope this helps.

Answer 3

阅读教程论文A tutorial on (co)algebras and (co)induction应该让您对计算机科学中的 co-algebra 有所了解。

下面引用它来说服你，

一般而言，某种编程语言中的程序操作数据。在过去几十年计算机科学的发展过程中，很明显需要对这些数据进行抽象描述，例如，以确保一个程序不依赖于它所操作的数据的特定表示。此外，这种抽象性有助于正确性证明。
这种愿望导致在计算机科学中使用代数方法，在一个称为代数规范或抽象数据类型理论的分支中。研究的对象是数据类型本身，使用代数中熟悉的技术概念。计算机科学家使用的数据类型通常是从​​给定的（构造函数）操作集合中生成的，正因为如此，代数的“初始性”发挥了如此重要的作用。
标准代数技术已被证明可用于捕获计算机科学中使用的数据结构的各个基本方面。但事实证明，用代数方式描述计算中出现的一些固有的动态结构是很困难的。这种结构通常涉及状态的概念，它可以通过各种方式进行转换。这种基于状态的动态系统的正式方法通常使用自动机或转换系统，作为经典的早期参考。
在过去的十年中，这种基于状态的系统不应被描述为代数，而应被描述为所谓的余代数，这一观点逐渐加深。这些是代数的形式对偶，在本教程中将更加精确。代数的“初始性”的双重性质，即最终性，对于这种协代数来说是至关重要的。这种最终的协代数所需要的逻辑推理原则不是归纳而是协归纳。

---

前奏，关于范畴论。 范畴论应该是函子的重命名论。因为类别是定义函子必须定义的。（此外，为了定义自然变换，必须定义函子。）

什么是函子？ 这是从一组到另一组的转换，保留了它们的结构。（有关更多详细信息，网上有很多很好的描述）。

什么是 F 代数？ 这是函子的代数。这只是对函子的普遍适用性的研究。

它如何与计算机科学联系起来？ 程序可以被视为一组结构化的信息。程序的执行对应于对这组结构化信息的修改。执行应该保留程序结构听起来不错。然后可以将执行视为函子在这组信息上的应用。（定义程序的那个）。

为什么是 F-协代数？ 程序本质上是双重的，因为它们是由信息描述的，并且它们会根据信息采取行动。那么主要是编写程序并使其更改的信息可以通过两种方式查看。

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

那么在这个阶段，我想说的是，

• F-代数是研究作用于数据宇宙（定义在这里）的函子变换。
• F-协代数是研究作用于状态宇宙的泛函变换（如这里定义的那样）。

在程序的生命周期中，数据和状态共存，它们相互补充。他们是双重的。

Answer 4

I'll start with stuff that is obviously programming-related and then add on some mathematics stuff, to keep it as concrete and down-to-earth as I can.

---

Let's quote some computer-scientists on coinduction…</h2>

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

Induction is about finite data, co-induction is about infinite data.

The typical example of infinite data is the type of a lazy list (a stream). For example, lets say that we have the following object in memory:

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

The computer can’t hold all of π, because it only has a finite amount of memory! But what it can do is hold a finite program, which will produce any arbitrarily long expansion of π that you desire. As long as you only use finite pieces of the list, you can compute with that infinite list as much as you need.

However, consider the following program:

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

In lazy functional programming languages like Haskell, infinite data structures are everywhere. Infinite lists and more exotic datatypes provide convenient abstractions for communication between parts of a program. Achieving similar convenience without infinite lazy structures would, in many cases, require acrobatic inversions of control flow.

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

---

Relating the ambient mathematical context to usual programming tasks

What is "an algebra"?

Algebraic structures generally look like:

1. Stuff
2. What the stuff can do

This should sound like objects with 1. properties and 2. methods. Or even better, it should sound like type signatures.

Standard mathematical examples include monoid ⊃ group ⊃ vector-space ⊃ "an algebra". Monoids are like automata: sequences of verbs (eg, f.g.h.h.nothing.f.g.f). A git log that always adds history and never deletes it would be a monoid but not a group. If you add inverses (eg negative numbers, fractions, roots, deleting accumulated history, un-shattering a broken mirror) you get a group.

Groups contain things that can be added or subtracted together. For example Durations can be added together. (But Dates cannot.) Durations live in a vector-space (not just a group) because they can also be scaled by outside numbers. (A type signature of scaling :: (Number,Duration) → Duration.)

Algebras ⊂ vector-spaces can do yet another thing: there’s some m :: (T,T) → T. Call this "multiplication" or don't, because once you leave Integers it’s less obvious what "multiplication" (or "exponentiation") should be.

(This is why people look to (category-theoretic) universal properties: to tell them what multiplication should do or be like:

)

---

Algebras → Coalgebras

Comultiplication is easier to define in a way that feels non-arbitrary, than is multiplication, because to go from T → (T,T) you can just repeat the same element. ("diagonal map" – like diagonal matrices/operators in spectral theory)

Counit is usually the trace (sum of diagonal entries), although again what's important is what your counit does; trace is just a good answer for matrices.

The reason to look at a dual space, in general, is because it's easier to think in that space. For example it's sometimes easier to think about a normal vector than about the plane it's normal to, but you can control planes (including hyperplanes) with vectors (and now I'm speaking of the familiar geometric vector, like in a ray-tracer).

---

Taming (un)structured data

Mathematicians might be modelling something fun like TQFT's, whereas programmers have to wrestle with

• 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,
• .....

Computer scientists, when talking about coalgebras, usually have set-ish operations in mind, like Cartesian product. I believe this is what people mean when they say like "Algebras are coalgebras in Haskell". But to the extent that programmers have to model complex data-types like Place, Date/Time, and Customer—and make those models look as much like the real world (or at least the end-user's view of the real world) as possible—I believe duals, could be useful beyond only set-world.