A quoi ressemble un comonoïde non trivial?
Comonoids sont mentionnés, par exemple, dans Haskell distributive bibliothèque de documents :
en raison de l'absence de comonoïdes non triviaux à Haskell, nous pouvons nous limiter à exiger un fonctionnement plutôt qu'une classe Coapplicative.
après une petite recherche, j'ai trouvé une réponse StackOverflow qui explique cela un peu plus avec les lois que les comonoïdes seraient ont à satisfaire. Donc je pense que je comprends pourquoi il n'y a qu'une seule instance possible pour une hypothétique classe Typo-Comonoïde à Haskell.
donc, pour trouver un comonoïde non trivial, je suppose que nous devrions chercher dans une autre catégorie. Sûrement, si les théoriciens de catégorie ont un nom pour les comonoïdes, alors il ya quelques intéressants. Les autres réponses sur cette page semblent faire allusion à un exemple impliquant Supply , mais je ne pouvais pas comprendre un qui satisfait encore les lois.
je me suis aussi tourné vers Wikipedia: il y a une page pour les monoïdes qui ne fait pas référence à la théorie des catégories, ce qui me semble être une description adéquate de la Monoid typeclass de Haskell, mais les redirections" comonoïdes " à une description de catégorie-théorétique des monoïdes et des comonoïdes ensemble que je ne peux pas comprendre, et il ne semble toujours pas être des exemples intéressants.
donc mes questions sont:
- peut comonoids être expliqué en Non-catégorie-des termes théoriques comme monoids?
- Quel est un exemple simple d'un comonoïde intéressant, même si ce n'est pas un type Haskell? (Pourrait-on en trouver une dans une catégorie Kleisli sur une monade Haskell familière?)
edit: Je ne suis pas sûr que ce soit réellement catégorie-théoriquement correcte, mais ce que j'imaginais dans la parenthetical de la question 2 était des définitions non triviales de delete :: a -> m () et split :: a -> m (a, a) pour certains spécifiques Haskell type a et Haskell monad m qui satisfont Kleisli-arrow versions des lois comonoïdes dans la réponse liée. D'autres exemples de comonoïdes sont encore les bienvenus.
3 réponses
comme L'a mentionné Phillip JF, les comonoïdes sont intéressants à discuter dans les logiques substructurales. Parlons du calcul lambda linéaire. Cela ressemble beaucoup à votre calcul lambda typé normal, sauf que chaque variable doit être utilisée exactement une fois.
pour obtenir une sensation, nous allons compter les fonctions linéaires des types donnés , i.e.
a -> a
a exactement un habitant, id . Tandis que
(a,a) -> (a,a)
en a deux, id et flip . Notez que dans le calcul lambda régulier (a,a) -> (a,a) a quatre habitants
(a, b) ↦ (a, a)
(a, b) ↦ (b, b)
(a, b) ↦ (a, b)
(a, b) ↦ (b, a)
mais les deux premiers exigent que nous utilisions l'un des arguments deux fois tout en rejetant l'autre. C'est exactement l'essence du calcul lambda linéaire-rejeter ces types de fonctions.
comme un raccourci, Quel est le point de LC linéaire? Bien, nous pouvons l'utiliser pour modéliser les effets linéaires ou l'utilisation des ressources. Si, par exemple, nous avons un type de fichier et quelques Transformateurs il pourrait ressembler à
data File
open :: String -> File
close :: File -> () -- consumes a file, but we're ignoring purity right now
t1 :: File -> File
t2 :: File -> File
et ensuite les pipelines suivants sont valides:
close . t1 . t2 . open
close . t2 . t1 . open
close . t1 . open
close . t2 . open
mais ce calcul de "ramification" n'est pas
let f1 = open "foo"
f2 = t1 f1
f3 = t2 f1
in close f3
puisque nous avons utilisé f1 deux fois.
Maintenant, vous pourriez vous demander quelque chose à ce point sur ce que les choses doivent suivre les règles linéaires. Par exemple, j'ai décidé que certains pipelines ne doivent pas inclure à la fois t1 et t2 (comparer l'exercice d'énumération d'avant). En outre, j'ai introduit les fonctions open et close qui créent et détruisent heureusement le type File malgré que ce soit une violation de la linéarité.
en effet, nous pourrions poser l'existence de fonctions qui violent linéarité-mais pas tous les clients peuvent. C'est un peu comme le monad IO -tous les secrets vivent à l'intérieur de la mise en œuvre de IO afin que les utilisateurs travaillent dans un monde "pur".
et c'est ici que Comonoid entre en jeu.
class Comonoid m where
destroy :: m -> ()
split :: m -> (m, m)
un type qui instancie Comonoid dans un calcul lambda linéaire est un type qui a des règles de destruction et de duplication carry-along. En d'autres termes, c'est un type qui n'est pas très lié par linéaire lambda calcul.
depuis Haskell ne met pas en œuvre les règles de calcul lambda linéaire du tout, nous pouvons toujours instantiate Comonoid
instance Comonoid a where
destroy a = ()
split a = (a, a)
ou, peut-être l'autre façon de penser, C'est que Haskell est un système LC linéaire qui instancie juste Comonoid pour chaque type et applique destroy et split pour vous automatiquement.
- un monoïde au sens habituel est le même qu'un monoïde catégorique dans la catégorie des ensembles. On s'attendrait à ce qu'un comonoïde dans le sens habituel soit le même qu'un comonoïde catégorique dans la catégorie des ensembles. Mais chaque ensemble dans la catégorie des ensembles est un comonoïde d'une manière triviale, donc apparemment il n'y a pas de description non-catégorique des comonoïdes qui serait parallèle à celle des monoïdes.
- comme une monade est un monoïde dans la catégorie de endofuncteurs (Quel est le problème?), une comonade est un comonoïde dans la catégorie des endofoncteurs (Quel est le coproblème? Donc oui, toute comonade à Haskell serait un exemple de comonoïde.
une façon de penser à un monoïde est aussi accrochée à n'importe quelle construction de produit que nous utilisons, donc dans L'ensemble nous prendrions cette signature:
mul : A * A -> A
one : A
à celui-ci:
dup : A -> A * A
one : A
mais l'idée de la dualité est que les déclarations logiques que vous pouvez faire tous ont des duels qui peuvent être appliqués aux objets duels, et il y a une autre façon d'affirmer ce qu'est un monoïde, et c'est être agnostique au choix du produit la construction et puis quand nous prenons la costructure nous pouvons prendre le coproduit dans la sortie, comme:
div : A -> A + A
one : A
où + est une somme marquée. Ici nous avons essentiellement que chaque terme simple qui est dans ce type est toujours prêt à produire un nouveau bit, qui est implicitement dérivé de l'étiquette utilisée pour désigner la gauche ou la droite instance de A. je pense personnellement que c'est vraiment cool. Je pense que la version cool des choses que les gens étaient parler de ci-dessus est quand vous ne construisez pas particulièrement que pour les monoïdes, mais pour les actions monoïdes.
un monoïde M est dit agir sur un ensemble a s'il y a une fonction
act : M * A -> A
où nous avons les règles suivantes
act identity a = a
act f (act g a) = act (f * g) a
si nous voulons une co-action, que voulons-nous exactement?
act : A -> M * A
cela nous génère un flux du type de notre comonoïde! Je vais avoir beaucoup de mal à venir avec les lois de ces systèmes, mais je pense qu'ils doivent être quelque part donc, je vais continuer à chercher ce soir. Si quelqu'un peut me les dire ou que j'ai tort sur ces choses d'une manière ou d'une autre, ça l'intéresse aussi.