什么是“余代数”?在编程的背景下是什么意思? [英] What does "coalgebra" mean in the context of programming?

查看:137
本文介绍了什么是“余代数”?在编程的背景下是什么意思?的处理方法,对大家解决问题具有一定的参考价值,需要的朋友们下面随着小编来一起学习吧!

问题描述

在函数式编程和PLT圈子中,我几次听到过coalgebras这个术语,特别是当讨论关于物体,共同体,镜头等时。谷歌搜索这个术语给出了这些结构的数学描述,这对我来说是非常难以理解的。任何人都可以解释一下编程语境中的什么是因果关系,它们的意义是什么,以及它们如何与对象和连接器相关联?解析方案

h1>代数

我认为开始的地方应该是理解代数的概念。这只是代数结构的一般化,比如组,环,monids等等。大多数时候,这些东西都是以集合的形式介绍的,但由于我们是朋友之间的关系,所以我会讨论一下Haskell类型。 (尽管我忍不住用了一些希腊字母 - 它们让一切看起来都更酷!)

然后,代数只是一个类型τ 带有一些功能和身份。这些函数采用不同数量的τ类型的参数,并产生一个τ:uncurried,它们看起来都像(τ,τ,...,τ)→τ。他们也可以拥有身份 - 元素τ,这些元素具有某些功能的特殊行为。



最简单的例子就是monoid。一个幺半群是任何类型的τ函数 mappend∷(τ,τ)→τ和一个标识 mzero∷τ。其他例子包括像群组(它们就像monoids除外有一个额外的 invert∷τ→τ函数),戒指,格子等等。



所有函数都在τ上运行,但可以有不同的arities。我们可以将它们写成τⁿ→τ,其中τⁿ映射到 n的元组 τ。这样,把身份认为是τ⁰→τ其中τ⁰只是空元组()。所以我们实际上可以简化一个代数的概念:它只是一些类型,它有一些函数。

代数只是数学中常见的模式分解出来,就像我们使用代码一样。人们注意到一大堆有趣的东西 - 前面提到的monoids,groups,lattice等 - 都遵循类似的模式,所以他们把它抽象出来。这样做的好处与编程相同:创建可重复使用的证明并使某些推理更容易。

F-代数



然而,我们还没有完成因子分解。到目前为止,我们有一堆函数τⁿ→τ。我们实际上可以做一个巧妙的窍门,将它们全部合并为一个功能。尤其是,我们来看看monoids:我们有 mappend∷(τ,τ)→τ mempty∷()→τ。我们可以使用总和类型 - 或者将它们变成单个函数。它看起来像这样:

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

实际上,我们可以反复使用这种转换将所有τⁿ→τ函数合并为一个函数,对于任何代数。 (事实上​​,我们可以对任何数量的函数做这个操作,例如 a→τ b→τ等等 a,b,... 。)



这让我们谈论代数从或者 s乱糟糟地将一个τ与一个 single code>τ。对于monoids,这个混乱是:或者(τ,τ)();对于组(它有一个额外的τ→τ操作),它是: Either(τither(τ,τ)τ)()。对于不同的结构来说,这是一种不同的类型。那么所有这些类型有什么共同点?最明显的是它们都是产品的代数 - 代数数据类型。例如,对于monoids,我们可以为任何 monoidτ创建一个monoid参数类型:

  data MonoidArgumentτ= Mappendττ - 此处ττ与(τ,τ)相同
| Mempty - 在这里我们可以离开()出

我们可以为组和团队做同样的事情戒指和格子以及所有其他可能的结构。

所有这些类型还有什么特别之处?那么,他们都是 Functors !例如:

pre $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ )
fmap f Mempty = Mempty

所以我们可以推广我们的代数思想,甚至更多。对于一些函子 f ,它只是一个类型τ,函数 fτ→τ code>。事实上,我们可以把它写成一个类型类:

  class Functor f⇒代数fτ其中
op∷ fτ→τ

这通常称为F-代数,因为它是由函子˚F。如果我们可以部分应用类型类,我们可以定义类似于 class Monoid = Algebra MonoidArgument

Coalgebras



现在,希望您能够很好地理解代数是什么以及它是如何泛化正常的代数结构。那么什么是F代数?那么,它意味着它是代数的双重 - 也就是说,我们需要一个代数并翻转一些箭头。我只在上面的定义中看到一个箭头,所以我只是将其翻转:

  class Functor f⇒CoAlgebra fτ其中
coop∷τ→fτ

就是这样!现在,这个结论可能看起来有些轻浮(heh)。它告诉你一个代数是什么,但并没有真正了解它是如何有用的或者我们为什么关心。一旦我找到一个或两个很好的例子,我会做一点,P。



类和对象



在阅读了一下后,我想我对如何使用代数来表示类和对象有了一个好主意。我们有一个 C 类型,它包含了该类中所有可能的对象内部状态;这个类本身是一个在 C 之上的余代数,它指定了对象的方法和属性。



代数示例,如果我们有一堆函数,如 a→τ b→τ对于任何 a,b,... ,我们可以将它们全部组合到一个函数中,使用或者,一个和类型。双概念将结合一堆类型为τ→a τ→b 的函数等等。我们可以使用总和类型(一种产品类型)的对偶来实现这一点。因此,考虑到上述两个函数(称为 f g ),我们可以像这样创建一个函数:

  both∷τ→(a,b)
both x =(fx,gx)

类型(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 一样。一个代数基本上只是封装了 self 参数的行为:这就是 C > C→FC 是。



所以我们把它放在一起。让我们设想一个类,它包含一个位置属性,一个名称属性和 setPosition







$ _ b: String
public
name:String
position:(Int,Int)
setPosition:(Int,Int)→C
pre>

我们需要两个部分来表示这个类。首先,我们需要表示对象的内部状态;在这种情况下,它只包含两个 Int s和一个 String 。 (这是我们的类型 C 。)然后我们需要拿出代表这个类的代数。

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

我们有两个属性可以编写。它们非常简单:

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

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) -for any c - 是一个函子,所以 coop 确实有我们想要的形式: Functor f⇒C→f C
$ b

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



这让我们使用代数推理来处理类。例如,我们可以引入一个F-余代数同态的概念来表示类之间的转换。这是一个令人恐惧的测试术语,它仅仅意味着保留结构的余代之间的转换。这使得考虑将类映射到其他类更容易。

简而言之,F-代数代表了一类,它拥有一系列依赖于它们的属性和方法在包含每个对象内部状态的 self 参数上。



其他类别



迄今为止,我们已经将代数和余代数描述为Haskell类型。一个代数只是一个类型τ,函数 fτ→τ,并且代数只是一个类型τ,函数为τ→fτ然而,没有什么能够将这些想法与Haskell 本身紧密结合。实际上,它们通常是以集合和数学函数的形式而不是类型和Haskell函数来介绍的。事实上,我们可以将这些概念推广到任何类别

我们可以为某个类别 C定义一个F-代数。首先,我们需要一个仿函数 F:C→C - 也就是 endofunctor 。 (所有Haskell Functor s实际上都是来自 Hask→Hask 的endofunctors。)然后,代数只是一个对象<$来自 C 的c $ c> A ,其态态 FA→A 。除了 A→F A



我们可以通过考虑其他类别获得什么?那么,我们可以在不同的情况下使用相同的想法。像单子一样。在Haskell中,monad是一种 M∷★→★三种操作类型:

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

map 函数只是 M 是一个 Functor 。所以我们可以说Monad只是一个有两个 操作的函数: return join

函子本身形成一个类别,它们之间的态射就是所谓的自然变换。自然变换只是将一个仿函数转换成另一个仿函数的一种方式,同时保留它的结构。 这里是一篇很好的文章,有助于解释这个想法。它讨论 concat ,它只是 join 列表。



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

pre code> instance(Functor f,Functor g)⇒Functor(f∘g)其中
fmap fun x = fmap(fmap fun)x

这有助于我们考虑加入作为从 f∘f→f 的映射。 join 的类型是∀α。 f(fα)→fα。直观地说,我们可以看到所有类型α有效的函数是如何被认为是 f



return 是一个类似的转换。它的类型是∀α。 α→fα。这看起来不同 - 第一个α不是在函数中!令人高兴的是,我们可以通过在其中添加一个身份仿函数来解决这个问题:∀α。身份α→fα。所以 return 是一个转换身份→f



现在我们可以将monad看作只是一个基于函数 f 的代数,其中 f f 身份→f 。这看起来不熟悉吗?它与monoid非常相似,它只是一些类型τ,其中τ×τ→τ和<$ c

因此,monad就像一个monoid,除了有一个类型,我们有一个函子。这是同一种代数,只是属于不同的类别。 (这就是我所知道的短语A monad仅仅是endofunctors类别中的一个monoid)。



现在,我们有这两个操作: f∘f→f 身份→f 。为了得到相应的余代数,我们只需要翻转箭头。这给了我们两个新的操作: f→f f→Identity 。我们可以通过添加类型变量将它们变成Haskell类型,给我们∀α。 fα→f(fα)∀α。 fα→α。这看起来就像comonad的定义:

  class Functor f⇒Comonad f其中
coreturn∷fα→ α
联合∷fα→f(fα)

coalgebra 在一个endofunctors类别中。

I have heard the term "coalgebras" several times in functional programming and PLT circles, especially when the discussion is about objects, comonads, lenses, and such. Googling this term gives pages that give mathematical description of these structures which is pretty much incomprehensible to me. Can anyone please explain what coalgebras mean in the context of programming, what is their significance, and how they relate to objects and comonads?

解决方案

Algebras

I think the place to start would be to understand the idea of an algebra. This is just a generalization of algebraic structures like groups, rings, monoids and so on. Most of the time, these things are introduced in terms of sets, but since we're among friends, I'll talk about Haskell types instead. (I can't resist using some Greek letters though—they make everything look cooler!)

An algebra, then, is just a type τ with some functions and identities. These functions take differing numbers of arguments of type τ and produce a τ: uncurried, they all look like (τ, τ,…, τ) → τ. They can also have "identities"—elements of τ that have special behavior with some of the functions.

The simplest example of this is the monoid. A monoid is any type τ with a function mappend ∷ (τ, τ) → τ and an identity mzero ∷ τ. Other examples include things like groups (which are just like monoids except with an extra invert ∷ τ → τ function), rings, lattices and so on.

All the functions operate on τ but can have different arities. We can write these out as τⁿ → τ, where τⁿ maps to a tuple of n τ. This way, it makes sense to think of identities as τ⁰ → τ where τ⁰ is just the empty tuple (). So we can actually simplify the idea of an algebra now: it's just some type with some number of functions on it.

An algebra is just a common pattern in mathematics that's been "factored out", just like we do with code. People noticed that a whole bunch of interesting things—the aforementioned monoids, groups, lattices and so on—all follow a similar pattern, so they abstracted it out. The advantage of doing this is the same as in programming: it creates reusable proofs and makes certain kinds of reasoning easier.

F-Algebras

However, we're not quite done with factoring. So far, we have a bunch of functions τⁿ → τ. We can actually do a neat trick to combine them all into one function. In particular, let's look at monoids: we have mappend ∷ (τ, τ) → τ and mempty ∷ () → τ. We can turn these into a single function using a sum type—Either. It would look like this:

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

We can actually use this transformation repeatedly to combine all the τⁿ → τ functions into a single one, for any algebra. (In fact, we can do this for any number of functions a → τ, b → τ and so on for any 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

We can do the same thing for groups and rings and lattices and all the other possible structures.

What else is special about all these types? Well, they're all Functors! E.g.:

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

So we can generalize our idea of an algebra even more. It's just some type τ with a function f τ → τ for some functor f. In fact, we could write this out as a typeclass:

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

This is often called an "F-algebra" because it's determined by the functor F. If we could partially apply typeclasses, we could define something like class Monoid = Algebra MonoidArgument.

Coalgebras

Now, hopefully you have a good grasp of what an algebra is and how it's just a generalization of normal algebraic structures. So what is an F-coalgebra? Well, the co implies that it's the "dual" of an algebra—that is, we take an algebra and flip some arrows. I only see one arrow in the above definition, so I'll just flip that:

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

And that's all it is! Now, this conclusion may seem a little flippant (heh). It tells you what a coalgebra is, but does not really give any insight on how it's useful or why we care. I'll get to that in a bit, once I find or come up with a good example or two :P.

Classes and Objects

After reading around a bit, I think I have a good idea of how to use coalgebras to represent classes and objects. We have a type C that contains all the possible internal states of objects in the class; the class itself is a coalgebra over C which specifies the methods and properties of the objects.

As shown in the algebra example, if we have a bunch of functions like a → τ and b → τ for any a, b,…, we can combine them all into a single function using Either, a sum type. The dual "notion" would be combining a bunch of functions of type τ → a, τ → b and so on. We can do this using the dual of a sum type—a product type. So given the two functions above (called f and g), we can create a single one like so:

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

The type (a, a) is a functor in the straightforward way, so it certainly fits with our notion of an F-coalgebra. This particular trick lets us package up a bunch of different functions—or, for OOP, methods—into a single function of type τ → f τ.

The elements of our type C represent the internal state of the object. If the object has some readable properties, they have to be able to depend on the state. The most obvious way to do this is to make them a function of C. So if we want a length property (e.g. object.length), we would have a function C → Int.

We want methods that can take an argument and modify state. To do this, we need to take all the arguments and produce a new C. Let's imagine a setPosition method which takes an x and a y coordinate: object.setPosition(1, 2). It would look like this: C → ((Int, Int) → C).

The important pattern here is that the "methods" and "properties" of the object take the object itself as their first argument. This is just like the self parameter in Python and like the implicit this of many other languages. A coalgebra essentially just encapsulates the behavior of taking a self parameter: that's what the first C in C → F C is.

So let's put it all together. Let's imagine a class with a position property, a name property and setPosition function:

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

We need two parts to represent this class. First, we need to represent the internal state of the object; in this case it just holds two Ints and a String. (This is our type C.) Then we need to come up with the coalgebra representing the class.

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

We have two properties to write. They're pretty trivial:

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

name ∷ C → String
name self = _name self

Now we just need to be able to update the position:

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

This is just like a Python class with its explicit self variables. Now that we have a bunch of self → functions, we need to combine them into a single function for the coalgebra. We can do this with a simple tuple:

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

The type ((Int, Int), String, (Int, Int) → c)—for any c—is a functor, so coop does have the form we want: Functor f ⇒ C → f C.

Given this, C along with coop form a coalgebra which specifies the class I gave above. You can see how we can use this same technique to specify any number of methods and properties for our objects to have.

This lets us use coalgebraic reasoning to deal with classes. For example, we can bring in the notion of an "F-coalgebra homomorphism" to represent transformations between classes. This is a scary sounding term that just means a transformation between coalgebras that preserves structure. This makes it much easier to think about mapping classes onto other classes.

In short, an F-coalgebra represents a class by having a bunch of properties and methods that all depend on a self parameter containing each object's internal state.

Other Categories

So far, we've talked about algebras and coalgebras as Haskell types. An algebra is just a type τ with a function f τ → τ and a coalgebra is just a type τ with a function τ → f τ.

However, nothing really ties these ideas to Haskell per se. In fact, they're usually introduced in terms of sets and mathematical functions rather than types and Haskell functions. Indeed,we can generalize these concepts to any categories!

We can define an F-algebra for some category C. First, we need a functor F : C → C—that is, an endofunctor. (All Haskell Functors are actually endofunctors from Hask → Hask.) Then, an algebra is just an object A from C with a morphism F A → A. A coalgebra is the same except with A → F A.

What do we gain by considering other categories? Well, we can use the same ideas in different contexts. Like monads. In Haskell, a monad is some type M ∷ ★ → ★ with three operations:

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

The map function is just a proof of the fact that M is a Functor. So we can say that a monad is just a functor with two operations: return and join.

Functors form a category themselves, with morphisms between them being so-called "natural transformations". A natural transformation is just a way to transform one functor into another while preserving its structure. Here's a nice article helping explain the idea. It talks about concat, which is just join for lists.

With Haskell functors, the composition of two functors is a functor itself. In pseudocode, we could write this:

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

This helps us think about join as a mapping from f ∘ f → f. The type of join is ∀α. f (f α) → f α. Intuitively, we can see how a function valid for all types α can be thought of as a transformation of f.

return is a similar transformation. Its type is ∀α. α → f α. This looks different—the first α is not "in" a functor! Happily, we can fix this by adding an identity functor there: ∀α. Identity α → f α. So return is a transformation Identity → f.

Now we can think about a monad as just an algebra based around some functor f with operations f ∘ f → f and Identity → f. Doesn't this look familiar? It's very similar to a monoid, which was just some type τ with operations τ × τ → τ and () → τ.

So a monad is just like a monoid, except instead of having a type we have a functor. It's the same sort of algebra, just in a different category. (This is where the phrase "A monad is just a monoid in the category of endofunctors" comes from as far as I know.)

Now, we have these two operations: f ∘ f → f and Identity → f. To get the corresponding coalgebra, we just flip the arrows. This gives us two new operations: f → f ∘ f and f → Identity. We can turn them into Haskell types by adding type variables as above, giving us ∀α. f α → f (f α) and ∀α. f α → α. This looks just like the definition of a comonad:

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

So a comonad is then a coalgebra in a category of endofunctors.

这篇关于什么是“余代数”?在编程的背景下是什么意思?的文章就介绍到这了,希望我们推荐的答案对大家有所帮助,也希望大家多多支持IT屋!

查看全文
登录 关闭
扫码关注1秒登录
发送“验证码”获取 | 15天全站免登陆