Quels sont les exemples motivants de CoMonad libre en Haskell ?

Question

J'ai joué avec Cofree et je n'arrive pas à le comprendre.

Par exemple, je veux jouer avec Cofree [] Num dans ghci et je n'arrive pas à trouver d'exemples intéressants.

Par exemple, si je construis un type Cofree :

let a = 1 :< [2, 3]

Je m'attendrais extract a == 1 mais au lieu de cela, j'obtiens cette erreur :

No instance for (Num (Cofree [] a0)) arising from a use of ‘it’
    In the first argument of ‘print’, namely ‘it’
    In a stmt of an interactive GHCi command: print it

Et un type de :

extract a :: (Num a, Num (Cofree [] a)) => a

Puis-je obtenir quelques exemples simples, même triviaux, de la façon d'utiliser Cofree avec, disons, des foncteurs : [] ou Maybe ou Either qui démontre

• extract
• extend
• unwrap
• duplicate ?

Posté en croix : https://www.reddit.com/r/haskell/comments/4wlw70/what_are_some_motivating_examples_for_cofree/

EDIT : Guidé par le commentaire de David Young, voici quelques meilleurs exemples qui montrent où mes premières tentatives étaient malavisées, cependant j'aimerais toujours avoir des exemples qui peuvent guider une intuition de Cofree :

> let a = 1 :< []
> extract a
    1
> let b = 1 :< [(2 :< []), (3 :< [])]
> extract b
    1
> unwrap b
    [2 :< [],3 :< []]
> map extract $ unwrap b
    [2,3]

Answer 1

Récapitulons simplement la définition de la Cofree type de données.

data Cofree f a = a :< f (Cofree f a)

C'est au moins suffisant pour diagnostiquer le problème de l'exemple. Quand vous avez écrit

1 :< [2, 3]

vous avez fait une petite erreur qui est signalée plus subtilement qu'elle n'est utile. Ici, f = [] y a est quelque chose de numérique, car 1 :: a . En conséquence, vous devez

[2, 3] :: [Cofree [] a]

et donc

2 :: Cofree [] a

dont pourrait ça va si Cofree [] a étaient également un exemple de Num . Votre définition acquiert ainsi une contrainte qui a peu de chances d'être satisfaite, et en effet, lorsque vous utiliser votre valeur, la tentative de satisfaire la contrainte échoue.

Essayez à nouveau avec

1 :< [2 :< [], 3 :< []]

et vous devriez avoir plus de chance.

Maintenant, voyons ce que nous avons. Commencez par faire simple. Qu'est-ce que Cofree f () ? Qu'est-ce qui, en particulier, est Cofree [] () ? Ce dernier est isomorphe au point fixe de [] : les structures arborescentes où chaque nœud est une liste de sous-arbres, également connues sous le nom de "rosaces non étiquetées". Par exemple,

() :< [  () :< [  () :< []
               ,  () :< []
               ]
      ,  () :< []
      ]

De même, Cofree Maybe () est plus ou moins le point fixe de Maybe : une copie des nombres naturels, car Maybe nous donne soit zéro, soit une position dans laquelle nous pouvons insérer un sous-arbre.

zero :: Cofree Maybe ()
zero = () :< Nothing
succ :: Cofree Maybe () -> Cofree Maybe ()
succ n = () :< Just n

Un cas trivial important est Cofree (Const y) () qui est une copie de y . Le site Const y donne pas de les positions des sous-arbres.

pack :: y -> Cofree (Const y) ()
pack y = () :< Const y

Ensuite, occupons-nous de l'autre paramètre. Il vous indique le type d'étiquette à attacher à chaque nœud. En renommant les paramètres de manière plus suggestive

data Cofree nodeOf label = label :< nodeOf (Cofree nodeOf label)

Quand nous étiquetons le (Const y) par exemple, on obtient paires

pair :: x -> y -> Cofree (Const y) x
pair x y = x :< Const y

Lorsque nous attachons des étiquettes aux nœuds de nos nombres, nous obtenons non vide listes

one :: x -> Cofree Maybe x
one = x :< Nothing
cons :: x -> Cofree Maybe x -> Cofree Maybe x
cons x xs = x :< Just xs

Et pour les listes, on obtient étiqueté des rosiers.

0 :< [  1 :< [  3 :< []
             ,  4 :< []
             ]
     ,  2 :< []
     ]

Ces structures sont toujours "non vides", car il y a au moins un nœud supérieur, même s'il n'a pas d'enfants, et ce nœud aura toujours une étiquette. Le site extract vous donne l'étiquette du noeud supérieur.

extract :: Cofree f a -> a
extract (a :< _) = a

C'est-à-dire, extract jette le contexte de l'étiquette supérieure.

Maintenant, le duplicate opération décore chaque étiquette avec son propre le contexte.

duplicate :: Cofree f a -> Cofree f (Cofree f a)
duplicate a :< fca = (a :< fca) :< fmap duplicate fca  -- f's fmap

Nous pouvons obtenir un Functor instance pour Cofree f en visitant l'arbre entier

fmap :: (a -> b) -> Cofree f a -> Cofree f b
fmap g (a :< fca) = g a :< fmap (fmap g) fca
    --                     ^^^^  ^^^^
    --                 f's fmap  ||||
    --                           (Cofree f)'s fmap, used recursively

Il n'est pas difficile de voir que

fmap extract . duplicate = id

parce que duplicate décore chaque nœud avec son contexte, alors fmap extract jette la décoration.

Notez que fmap ne regarde que les étiquettes de l'entrée pour calculer les étiquettes de la sortie. Supposons que nous voulions calculer les étiquettes de sortie en fonction de chaque étiquette d'entrée dans son contexte ? Par exemple, avec un arbre non étiqueté, nous pourrions vouloir étiqueter chaque nœud avec la taille de son sous-arbre entier. Grâce à l'outil Foldable instance pour Cofree f nous devrions être en mesure de compter les nœuds avec.

length :: Foldable f => Cofree f a -> Int

Cela signifie donc

fmap length . duplicate :: Cofree f a -> Cofree f Int

L'idée clé des comonades est qu'elles capturent les "choses avec un certain contexte", et qu'elles vous permettent d'appliquer partout des cartes dépendant du contexte.

extend :: Comonad c => (c a -> b) -> c a -> c b
extend f = fmap f       -- context-dependent map everywhere
           .            -- after
           duplicate    -- decorating everything with its context

Définition de extend plus directement vous évite la duplication (même si cela ne revient qu'à un partage).

extend :: (Cofree f a -> b) -> Cofree f a -> Cofree f b
extend g ca@(_ :< fca) = g ca :< fmap (extend g) fca

Et vous pouvez obtenir duplicate en prenant

duplicate = extend id -- the output label is the input label in its context

De plus, si vous choisissez extract comme la chose à faire à chaque étiquette dans le contexte, il suffit de remettre chaque étiquette là d'où elle vient :

extend extract = id

Ces "opérations sur les étiquettes-en-contexte" sont appelées "flèches de co-Kleisli",

g :: c a -> b

et le travail de extend est d'interpréter une flèche co-Kleisli comme une fonction sur des structures entières. Le site extract L'opération est la flèche d'identité co-Kleisli, et elle est interprétée par extend comme fonction d'identité. Bien sûr, il existe une composition co-Kleisli

(=<=) :: Comonad c => (c s -> t) -> (c r -> s) -> (c r -> t)
(g =<= h) = g . extend h

et les lois comonad garantissent que =<= est associatif et absorbe extract ce qui nous donne la catégorie co-Kleisli. De plus, nous avons

extend (g =<= h)  =  extend g . extend h

de sorte que extend est un foncteur (au sens catégorique) de la catégorie co-Kleisli aux ensembles et fonctions. Ces lois ne sont pas difficiles à vérifier Cofree car ils découlent de la Functor pour la forme du nœud.

Une façon utile de voir une structure dans une comonade libre est de la considérer comme une sorte de "serveur de jeu". Une structure

a :< fca

représente l'état du jeu. Un mouvement dans le jeu consiste soit à "s'arrêter", auquel cas vous obtenez le symbole de l'état d'avancement du jeu. a ou de "continuer", en choisissant un sous-arbre de l'élément fca . Par exemple, on peut considérer

Cofree ((->) move) prize

Un client pour ce serveur doit soit s'arrêter, soit continuer en donnant un move : c'est un liste de move s. Le jeu se déroule comme suit :

play :: [move] -> Cofree ((->) move) prize -> prize
play []       (prize :< _) = prize
play (m : ms) (_     :< f) = play ms (f m)

Peut-être qu'un move est un Char et le prize est le résultat de l'analyse de la séquence de caractères.

Si vous fixez assez fort, vous verrez que [move] est une version de Free ((,) move) () . Les monades libres représentent les stratégies des clients. Le foncteur ((,) move) équivaut à une interface de commande avec seulement la commande "envoyer un move ". Le foncteur ((->) move) est la structure correspondante "répondre à l'envoi d'un move ".

Certains foncteurs peuvent être considérés comme capturant une interface de commande ; la monade libre d'un tel foncteur représente les programmes qui émettent des commandes ; le foncteur aura un "dual" qui représente la façon de répondre aux commandes ; la comonade cofree du dual est la notion générale d'environnement dans lequel les programmes qui émettent des commandes peuvent être exécutés, avec l'étiquette indiquant ce qu'il faut faire si le programme s'arrête et renvoie une valeur, et les sous-structures indiquant comment poursuivre l'exécution du programme s'il émet une commande.

Par exemple,

data Comms x = Send Char x | Receive (Char -> x)

décrit être autorisé à envoyer ou recevoir des caractères. Son double est

data Responder x = Resp {ifSend :: Char -> x, ifReceive :: (Char, x)}

Comme exercice, voyez si vous pouvez mettre en œuvre l'interaction

chatter :: Free Comms x -> Cofree Responder y -> (x, y)