Ce n' “coalgebra” signifie dans le contexte de la programmation?

Algèbres de

Je pense que l'endroit pour commencer serait de comprendre l'idée d'un algèbre. C'est juste une généralisation de structures algébriques comme les groupes, les anneaux, les monoids et ainsi de suite. La plupart du temps, ces choses sont mis en place en termes de jeux, mais puisque nous sommes entre amis, je vais vous parler d'Haskell plutôt les types de. (Je ne peux pas résister à l'aide de quelques lettres grecques cependant, ils font tout plus froid!)

Une algèbre, alors, c'est juste un type τ avec certaines fonctions et des identités. Ces fonctions prennent des nombres des arguments de type τ et de produire un τ: uncurried, elles ressemblent toutes à (τ, τ,…, τ) → τ. Ils peuvent aussi avoir des "identités"—éléments de τ qui ont un comportement particulier avec certaines fonctions.

L'exemple le plus simple de ce est le monoïde. Un monoïde est tout type τ avec une fonction mappend ∷ (τ, τ) → τ et une identité mzero ∷ τ. D'autres exemples comprennent des choses comme des groupes (qui sont comme monoids sauf avec un supplément de invert ∷ τ → τ fonction), des anneaux, des grilles et ainsi de suite.

Toutes les fonctions fonctionnent sur τ mais peut avoir différentes arities. On peut l'écrire comme τⁿ → τ, où τⁿ correspond à un tuple de n τ. De cette manière, il est logique de penser les identités τ⁰ → τ où τ⁰ est juste le vide tuple (). Alors, nous pouvons simplifier l'idée d'une algèbre de maintenant: c'est juste un type avec un certain nombre de fonctions sur elle.

Une algèbre est juste un modèle commun en mathématiques qui a été "pris en compte", tout comme nous le faisons avec le code. Les gens ont remarqué que tout un tas de choses intéressantes—la susmentionnés monoids, des groupes, des réseaux et tous ce qui suivent un schéma similaire, de sorte qu'ils abstraction de ça. L'avantage de ce mode est le même que dans la programmation: il crée réutilisables preuves et rend certains types de raisonnement plus facile.

F-Algèbres

Cependant, nous ne sommes pas tout à fait fini avec l'affacturage. Jusqu'à présent, nous avons un tas de fonctions τⁿ → τ. Nous pouvons réellement faire un truc intéressant pour les combiner en une seule fonction. En particulier, regardons monoids: nous avons mappend ∷ (τ, τ) → τ et mempty ∷ () → τ. Nous pouvons les transformer en une seule fonction à l'aide d'un type de somme—Either. Il devrait ressembler à ceci:

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

Nous pouvons utiliser cette transformation à plusieurs reprises pour combiner tous la τⁿ → τ fonctions en un seul, pour tout de l'algèbre. (En fait, nous pouvons le faire pour n'importe quel nombre de fonctions a → τ, b → τ et ainsi de suite pour tout a, b,….)

Cela nous permet de parler d'algèbres de type τ avec un unique fonction de certains désordre de Eithers à un seul τ. Pour monoids, ce gâchis est: Either (τ, τ) (); pour les groupes (qui ont un supplément de τ → τ de l'opération), c'est: Either (Either (τ, τ) τ) (). C'est un type différent pour chaque structure. Alors, que faire de tous ces types ont en commun? La chose la plus évidente est qu'ils sont tous simplement des sommes de produits—types de données algébriques. Par exemple, pour monoids, on pourrait créer un monoïde type d'argument qui fonctionne pour tout monoïde τ:

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

Nous pouvons faire la même chose pour les groupes et les anneaux et les grilles et tous les autres structures possibles.

Quoi d'autre est spécial au sujet de ces types? Eh bien, ils sont tous Functors! E. g.:

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

De sorte que nous pouvons généraliser nos idée d'une algèbre de même plus. C'est juste un type τ avec une fonction f τ → τ pour certains foncteur f. En fait, on peut écrire ceci comme un typeclass:

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

Ceci est souvent appelé un "F-algèbre" parce qu'il est déterminé par le foncteur F. Si nous pouvions appliquer partiellement typeclasses, nous pourrions définir quelque chose comme class Monoid = Algebra MonoidArgument.

Coalgebras

Maintenant, j'espère que vous avez une bonne compréhension de ce qu'est une algèbre est et comment il est juste une généralisation de la normale structures algébriques. Donc qu'est ce qu'un F-coalgebra? Eh bien, le co suppose que c'est le "double" d'une algèbre—qui est, nous prenons une algèbre de flip et quelques flèches. Je ne vois qu'une seule flèche dans la définition ci-dessus, donc je vais juste flip que:

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

Et c'est tout ce qu'il est! Maintenant, cette conclusion peut sembler un peu désinvolte (heh). Il vous dit ce un coalgebra est, mais n'a pas vraiment donner quelque indication sur la façon dont il est utile ou pourquoi nous nous occupons. Je vais obtenir dans un instant, une fois que j'ai trouver ou proposer un bon exemple ou deux :P.

Les Classes et les Objets

Après avoir lu un peu, je pense avoir une bonne idée de la façon d'utiliser coalgebras pour représenter les classes et les objets. Nous avons un type C qui contient tous les états internes des objets dans la classe; la classe elle-même est un coalgebra sur C qui spécifie les méthodes et propriétés des objets.

Comme indiqué dans l'algèbre exemple, si nous avons un tas de fonctions comme a → τ et b → τ pour tout a, b,…, nous pouvons les combiner en une seule fonction à l'aide de Either, un type somme. Le double "notion" serait combinant un tas de fonctions de type τ → a, τ → b et ainsi de suite. Nous pouvons faire cela en utilisant le dual d'un type de somme—un type de produit. Donc, étant donné que les deux fonctions ci-dessus (appelé f et g), nous pouvons créer un seul comme suit:

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

Le type (a, a) est un foncteur dans la façon simple, de sorte qu'il correspond à notre notion de F-coalgebra. Cette astuce nous permet d'empaqueter un tas de différentes fonctions—ou, pour la programmation orientée objet, les méthodes en une seule fonction de type τ → f τ.

Les éléments de notre type C représentent la interne état de l'objet. Si l'objet a une certaine lisible propriétés, ils doivent être en mesure de compter sur l'état. Le moyen le plus évident pour ce faire est de faire une fonction de C. Donc, si nous voulons une longueur de propriété (par exemple,object.length), on aurait une fonction C → Int.

Nous voulons méthodes que peut prendre un argument d'état et les modifier. Pour ce faire, nous avons besoin de tous les arguments et de produire un nouveau C. Imaginons un setPosition méthode qui prend un x et un y coordonnées: object.setPosition(1, 2). Il devrait ressembler à ceci: C → ((Int, Int) → C).

Le modèle important ici est que les "méthodes" et "propriétés" de l'objet, l'objet lui-même comme premier argument. C'est exactement comme les self paramètre en Python et comme l'implicite this de nombreuses autres langues. Un coalgebra essentiellement juste encapsule le comportement de la prise d'un self paramètre: c'est que le premier C dans C → F C est.

Donc, nous allons mettre tout cela ensemble. Imaginons une classe avec un position de la propriété, un name propriété et setPosition fonction:

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

Nous avons besoin de deux pièces de représenter cette classe. Tout d'abord, nous avons besoin de représenter l'état interne de l'objet; dans ce cas, il tient juste deux Ints et un String. (C'est notre type de C.) Ensuite, nous avons besoin de venir avec le coalgebra représentant la classe.

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

Nous avons deux propriétés à écrire. Ils sont assez trivial:

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

name ∷ C → String
name self = _name self

Maintenant nous avons juste besoin d'être en mesure de mettre à jour la position:

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

C'est juste comme un Python de classe avec ses explicite self variables. Maintenant que nous avons un tas de self → fonctions, il faut les combiner en une seule fonction pour la coalgebra. Nous pouvons faire cela avec un simple tuple:

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

Le type ((Int, Int), String, (Int, Int) → c)—pour tout c—est un foncteur, donc coop ne sont de la forme que nous voulons: Functor f ⇒ C → f C.

Compte tenu de cela, C avec coop forme d'un coalgebra qui spécifie la classe que j'ai donné ci-dessus. Vous pouvez voir comment nous pouvons utiliser cette même technique pour spécifier n'importe quel nombre de méthodes et de propriétés pour nos objets ont.

Cela nous permet d'utiliser la coalgebraic raisonnement pour traiter avec les classes. Par exemple, nous pouvons introduire dans la notion de "F-coalgebra homomorphism" pour représenter les transformations entre les classes. C'est un effrayant terme à consonance qui signifie simplement une transformation entre coalgebras qui préserve la structure. Cela le rend beaucoup plus facile de penser à la cartographie des classes sur les autres classes.

En bref, un F-coalgebra représente une classe en ayant un tas de propriétés et de méthodes reposent toutes sur un self paramètre contenant chaque objet interne de l'état.

Autres Catégories

Jusqu'à présent, nous avons parlé des algèbres et coalgebras comme Haskell types. Une algèbre est juste un type τ avec une fonction f τ → τ et un coalgebra est juste un type τ avec une fonction τ → f τ.

Cependant, rien ne relie ces idées à Haskell soi. En fait, ils sont généralement mis en place en termes d'ensembles et de fonctions mathématiques plutôt que de types et Haskell fonctions. En effet,nous pouvons généraliser ces concepts à tout catégories!

Nous pouvons définir une F-algèbre pour certaines catégorie C. Tout d'abord, nous avons besoin d'un foncteur F : C → C—qui est, un endofunctor. (Tous les Haskell Functors sont en fait endofunctors de Hask → Hask.) Ensuite, une algèbre est juste un objet A de C avec un morphism F A → A. Un coalgebra est le même, sauf avec A → F A.

Ce que nous gagnons en considérant d'autres catégories? Eh bien, nous pouvons utiliser les mêmes idées dans des contextes différents. Comme les monades. En Haskell, une monade est un certain type M ∷ ★ → ★ avec trois opérations:

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

La map fonction est juste une preuve du fait que M est un Functor. On peut donc dire qu'une monade est juste un foncteur avec deux opérations: return et join.

Foncteurs forment une catégorie eux-mêmes, avec morphisms entre eux étant soi-disant "les transformations naturelles". Une transformation naturelle est juste une façon de transformer un foncteur dans un autre, tout en préservant sa structure. Voici un bel article qui explique en partie l'idée. Il parle de concat, qui est juste join pour les listes.

Avec Haskell foncteurs, la composition de deux foncteurs est un foncteur lui-même. En pseudo-code, on pourrait écrire ceci:

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

Cela nous aide à penser join comme une cartographie de f ∘ f → f. Le type de join est ∀α. f (f α) → f α. Intuitivement, nous pouvons voir comment une fonction valide pour tous types α peut être considéré comme une transformation de f.

return est une transformation similaire. Son type est ∀α. α → f α. Cela ressemble différentes—la première α n'est pas "dans" un foncteur! Heureusement, nous pouvons résoudre ce problème en ajoutant une identité foncteur là: ∀α. Identity α → f α. Donc return est une transformation Identity → f.

Maintenant, nous pouvons penser à une monade comme juste une algèbre de autour de quelques foncteur f avec des opérations f ∘ f → f et Identity → f. N'est-ce pas vous semble familière? Il est très similaire à un monoïde, qui était juste un type τ avec des opérations τ × τ → τ et () → τ.

Donc une monade est juste comme un monoïde, sauf qu'au lieu d'avoir un type que nous avons un foncteur. C'est le genre même de l'algèbre, de la, juste dans une catégorie différente. (C'est là que la phrase "Une monade est juste un monoïde dans la catégorie des endofunctors" vient d'aussi loin que je sais.)

Maintenant, nous avons ces deux opérations: f ∘ f → f et Identity → f. Correspondant à l'coalgebra, nous avons il suffit de retourner les flèches. Cela nous donne deux nouvelles opérations: f → f ∘ f et f → Identity. Nous pouvons les transformer en Haskell types par l'ajout de variables de type que ci-dessus, nous donnant ∀α. f α → f (f α) et ∀α. f α → α. Cela ressemble tout à fait à la définition d'un comonad:

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

Donc un comonad est alors un coalgebra dans une catégorie de endofunctors.

Passer par le tutoriel papier Un tutoriel sur la (co)algèbres et (co)induction devrait vous donner un aperçu de la co-algèbre dans l'informatique.

Ci-dessous est une citation de lui pour vous en convaincre,

En termes généraux, un programme dans certains langage de programmation manipule les données. Au cours de la
le développement de l'informatique au cours des dernières décennies, il est devenu clair qu'un résumé
description de ces données est souhaitable, par exemple pour s'assurer que le programme ne dépend pas de la représentation particulière de données sur lesquelles il opère. Aussi, une telle abstraction facilite l'exactitude des preuves.

Cette volonté a conduit à utiliser des méthodes algébriques en informatique, dans une branche appelée spécification algébrique ou du type abstrait de données de la théorie. L'objet de l'étude sont les types de données en elles-mêmes, à l'aide des notions de techniques qui sont familiers de l'algèbre. Les types de données utilisés par les informaticiens sont souvent générés à partir d'une collection donnée de (constructeur) de l'exploitation,et c'est pour cette raison que "initiality" des algèbres joue un rôle important.

Standard techniques algébriques ont prouvé leur utilité dans la capture de divers aspects essentiels de structures de données utilisé en informatique. Mais il s'est avéré difficile à décrire algébriquement certains de la nature dynamique des structures qui se produisent dans le calcul. De telles structures sont généralement liés à une notion de l'état, qui peut être transformé en différentes manières. Formelle méthodes basées sur l'état des systèmes dynamiques en général de rendre l'utilisation d'automates ou de transition, les systèmes classiques de début de références.

Au cours de la dernière décennie, la perspicacité grandit peu à peu que cet état des systèmes à base ne devraient pas être décrit comme des algèbres, mais en tant que soi-disant co-algèbres. Ce sont les formel des double-algèbres, dans un sens qui sera précisé dans ce tutoriel. La double propriété de "initiality" pour les algèbres, à savoir la finalité s'est avéré déterminant pour la suite de la co-algèbres. Et le raisonnement logique principe qui est nécessaire pour de tels finale de la co-algèbres n'est pas l'induction, mais la co-induction.

Prélude, à propos de Catégorie de la théorie.
Catégorie de la théorie, doit être renommer la théorie des foncteurs.
Comme les catégories sont ce que l'on doit définir dans le but de définir les foncteurs.
(D'ailleurs, les foncteurs sont ce que l'on doit définir dans le but de définir les transformations naturelles.)

Ce qui est un foncteur?
C'est une transformation à partir d'un ensemble à un autre, la préservation de leur structure.
(Pour plus de détails il y a beaucoup de bonne description sur le net).

Ce qu'est une F-algèbre?
C'est l'algèbre de foncteur.
C'est juste l'étude de l'universel, de la bienséance de foncteur.

Comment peut-il être le lien à l'informatique ?
Le programme peut être vue comme un ensemble structuré d'informations.
Déroulement du programme correspondent à la modification de cet ensemble structuré d'informations.
Il sonne bien, que l'exécution doit préserver la structure du programme.
L'exécution peut être vue comme l'application d'un foncteur sur cet ensemble d'informations.
(Celui de la définition du programme).

Pourquoi F-co-algèbre ?
Programme double, par essence, comme ils sont de décrire l'information et de la ils agissent sur elle.
Puis principalement les informations qui composent le programme et les faire changé peut être vue dans les deux sens.

• De données qui peut être définit comme l'information est traitée par le programme.
• De l'état qui peuvent être définis comme le partage de l'information par le programme.

Puis, à ce stade, je tiens à dire que,

• F-algèbre est l'étude de functorial transformation agissant sur les Données de l'Univers (comme cela a été défini ici).
• F-co-algèbres est l'étude de functorial transformation agissant sur l'État de l'Univers (comme cela a été défini ici).

Au cours de la vie d'un programme, les données et l'état de co-existent, et ils se complètent.
Elles sont à double.