Définition de fmap avec id et return

Question

En La théorie des catégories pour les programmeurs par Bartosz Milewski, Milewski écrit le code suivant pour définir le retour et l'opérateur "poisson" (composition dans la catégorie de Kleisli) pour la monade Writer.

return :: a -> Writer a
return x = (x, "")

(>=>) :: (a -> Writer b) -> (b -> Writer c) -> (a -> Writer c)
m1 >=> m2 = \x ->
  let (y, s1) = m1 x
      (z, s2) = m2 y
  in  (z, s1 ++ s2)

Il définit ensuite fmap comme suit :

fmap f = id >=> (\x -> return (f x))

J'ai des difficultés à comprendre comment le id est utilisée ici. Le premier argument de l'opérateur poisson est clairement (a -> Writer b) mais id a la signature de type a -> a .

S'agit-il d'une erreur ou d'une faille dans ma compréhension ? Remplacement de id avec return est plus logique pour moi.

Answer 1

N'oubliez pas les quantifications universelles.

Poisson (>=>) a un type (a -> Writer b) -> ..... pour tout a y b .

id a un type a -> a pour tout a .

Ainsi, en particulier, le poisson a aussi le type (Writer b -> Writer b) -> ... pour tout b (prenez juste a = Writer b comme un cas particulier).

Plus loin, id a aussi le type Writer b -> Writer b (encore une fois, comme un cas particulier).

L'astuce consiste ici à "fusionner" les deux types à l'aide de la fonction unification . Nous commençons par exiger (a -> Writer b) = (a' -> a') et nous en déduisons a = a' y Writer b = a' . A partir de là, nous pouvons voir que ces deux types peuvent être unifiés, il n'y a donc pas de contradiction dans le passage des arguments.

(Notez également qu'ici nous avons renommé le a dans le type de id a a' pour éviter toute confusion avec les autres a pour le poisson)