De bons exemples de Not a Functor / Functor / Applicative / Monad?

Tout en expliquant à quelqu'un ce qu'est une classe de type X, j'ai du mal à trouver de bons exemples de structures de données qui sont exactement X.

Je demande donc des exemples pour:

• Un constructeur de type qui n'est pas un Functor.
• Un constructeur de type qui est un Functor, mais pas Applicative.
• Un constructeur de type qui est un Applicatif, mais qui n'est pas une Monade.
• Un constructeur de type qui est une Monade.

Je pense qu'il y a beaucoup d'exemples de Monade partout, mais un bon exemple de Monade avec une relation avec les exemples précédents pourrait compléter l'image.

Je cherche des exemples qui seraient similaires les uns aux autres, ne différant que par des aspects importants pour l'appartenance à la classe de type particulière.

Si on arrivait à trouver un exemple d'Arrow quelque part dans cette hiérarchie (est-ce entre Applicative et Monad?), Ce serait bien aussi!

Un constructeur de type qui n'est pas un Functor:

newtype T a = T (a -> Int)

Vous pouvez en faire un foncteur contravariant, mais pas un foncteur (covariant). Essayez d'écrire fmapet vous échouerez. Notez que la version du foncteur contravariant est inversée:

fmap      :: Functor f       => (a -> b) -> f a -> f b
contramap :: Contravariant f => (a -> b) -> f b -> f a

Un constructeur de type qui est un foncteur, mais pas Applicatif:

Je n'ai pas de bon exemple. Il y en a Const, mais idéalement j'aimerais un béton non monoïde et je ne pense à aucun. Tous les types sont essentiellement numériques, des énumérations, des produits, des sommes ou des fonctions lorsque vous y arrivez. Vous pouvez voir ci-dessous pigworker et je ne suis pas d'accord pour savoir si Data.Voidc'est un Monoid;

instance Monoid Data.Void where
    mempty = undefined
    mappend _ _ = undefined
    mconcat _ = undefined

Puisqu'il _|_s'agit d'une valeur légale dans Haskell, et en fait la seule valeur légale de Data.Void, cela répond aux règles monoïdes. Je ne sais pas quoi unsafeCoerceen faire, car votre programme n'est plus garanti de ne pas violer la sémantique de Haskell dès que vous utilisez une unsafefonction.

Voir le wiki de Haskell pour un article sur les fonctions inférieures ( lien ) ou dangereuses ( lien ).

Je me demande s'il est possible de créer un tel constructeur de type en utilisant un système de type plus riche, comme Agda ou Haskell avec différentes extensions.

Un constructeur de type qui est un Applicatif, mais pas une Monade:

newtype T a = T {multidimensional array of a}

Vous pouvez en faire un applicatif, avec quelque chose comme:

mkarray [(+10), (+100), id] <*> mkarray [1, 2]
  == mkarray [[11, 101, 1], [12, 102, 2]]

Mais si vous en faites une monade, vous pourriez obtenir un décalage de dimension. Je soupçonne que des exemples comme celui-ci sont rares dans la pratique.

Un constructeur de type qui est une Monade:

[]

À propos des flèches:

Demander où se trouve une flèche sur cette hiérarchie, c'est comme demander quel genre de forme "rouge" est. Notez le genre de décalage:

Functor :: * -> *
Applicative :: * -> *
Monad :: * -> *

mais,

Arrow :: * -> * -> *

Mon style peut être à l'étroit par mon téléphone, mais voilà.

newtype Not x = Kill {kill :: x -> Void}

ne peut pas être Functor. Si c'était le cas, nous aurions

kill (fmap (const ()) (Kill id)) () :: Void

et la Lune serait faite de fromage vert.

pendant ce temps

newtype Dead x = Oops {oops :: Void}

est un foncteur

instance Functor Dead where
  fmap f (Oops corpse) = Oops corpse

mais ne peut pas être d'application, ou nous aurions

oops (pure ()) :: Void

et le vert serait fait de fromage Moon (ce qui peut effectivement arriver, mais seulement plus tard dans la soirée).

(Remarque supplémentaire:, Voidcomme dans Data.Voidest un type de données vide. Si vous essayez d'utiliser undefinedpour prouver que c'est un monoïde, je vais utiliser unsafeCoercepour prouver que ce n'est pas le cas.)

Joyeusement,

newtype Boo x = Boo {boo :: Bool}

est applicable à bien des égards, par exemple, comme le voudrait Dijkstra,

instance Applicative Boo where
  pure _ = Boo True
  Boo b1 <*> Boo b2 = Boo (b1 == b2)

mais ça ne peut pas être une Monade. Pour voir pourquoi, observez que le retour doit être constant Boo Trueou Boo False, et donc que

join . return == id

ne peut pas tenir.

Oh ouais, j'ai presque oublié

newtype Thud x = The {only :: ()}

est une monade. Roulez le vôtre.

Avion pour attraper ...

Je crois que les autres réponses ont manqué quelques exemples simples et courants:

Un constructeur de type qui est un foncteur mais pas un applicatif. Un exemple simple est une paire:

instance Functor ((,) r) where
    fmap f (x,y) = (x, f y)

Mais il n'y a aucun moyen de définir son Applicativeinstance sans imposer de restrictions supplémentaires r. En particulier, il n'y a aucun moyen de définir pure :: a -> (r, a)un arbitraire r.

Un constructeur de type qui est un Applicatif, mais qui n'est pas une Monade. Un exemple bien connu est ZipList . (C'est un newtypequi encapsule les listes et leur fournit une Applicativeinstance différente .)

fmapest défini de la manière habituelle. Mais pureet <*>sont définis comme

pure x                    = ZipList (repeat x)
ZipList fs <*> ZipList xs = ZipList (zipWith id fs xs)

purecrée ainsi une liste infinie en répétant la valeur donnée, et <*>zippe une liste de fonctions avec une liste de valeurs - applique la i- ème fonction au i- ème élément. (La norme <*>sur []produit toutes les combinaisons possibles d'application de la fonction i -th à l' élément j -th.) Mais il n'y a aucun moyen sensé de définir une monade (voir cet article ).

Comment les flèches s'intègrent-elles dans la hiérarchie foncteur / applicative / monade? Voir Les idiomes sont inconscients, les flèches sont méticuleuses, les monades sont promiscueuses par Sam Lindley, Philip Wadler, Jeremy Yallop. MSFP 2008. (Ils appellent les idiomes des foncteurs applicatifs .) Le résumé:

Nous revisitons le lien entre trois notions de calcul: les monades de Moggi, les flèches de Hughes et les idiomes de McBride et Paterson (également appelés foncteurs applicatifs). Nous montrons que les idiomes sont équivalents aux flèches qui satisfont le type isomorphisme A ~> B = 1 ~> (A -> B) et que les monades sont équivalentes aux flèches qui satisfont le type isomorphisme A ~> B = A -> (1 ~ > B). De plus, les idiomes s'intègrent dans les flèches et les flèches s'intègrent dans les monades.

Un bon exemple pour un constructeur de type qui n'est pas un foncteur est Set: Vous ne pouvez pas implémenter fmap :: (a -> b) -> f a -> f b, car sans contrainte supplémentaire Ord bvous ne pouvez pas construire f b.

Je voudrais proposer une approche plus systématique pour répondre à cette question, et aussi pour montrer des exemples qui n'utilisent aucune astuce spéciale comme les valeurs "inférieures" ou les types de données infinis ou quelque chose comme ça.

Quand les constructeurs de types ne parviennent-ils pas à avoir des instances de classe de type?

En général, il existe deux raisons pour lesquelles un constructeur de type ne parvient pas à avoir une instance d'une certaine classe de type:

1. Impossible d'implémenter les signatures de type des méthodes requises à partir de la classe de type.
2. Peut implémenter les signatures de type mais ne peut pas satisfaire aux lois requises.

Les exemples du premier type sont plus faciles que ceux du deuxième type car pour le premier type, il suffit de vérifier si l'on peut implémenter une fonction avec une signature de type donnée, tandis que pour le second type, nous devons prouver qu'aucune implémentation pourrait éventuellement satisfaire aux lois.

Exemples spécifiques

• Un constructeur de type qui ne peut pas avoir d'instance de foncteur car le type ne peut pas être implémenté:

  data F z a = F (a -> z)

Il s'agit d'un contrafoncteur, pas d'un foncteur, par rapport au paramètre type a, car adans une position contravariante. Il est impossible d'implémenter une fonction avec signature de type (a -> b) -> F z a -> F z b.

• Un constructeur de type qui n'est pas un foncteur légal même si la signature de type de fmappeut être implémentée:

  data Q a = Q(a -> Int, a)
  fmap :: (a -> b) -> Q a -> Q b
  fmap f (Q(g, x)) = Q(\_ -> g x, f x)  -- this fails the functor laws!

L'aspect curieux de cet exemple est que nous pouvons implémenter fmaple bon type même s'il Fne peut pas être un foncteur car il utilise adans une position contravariante. Donc, cette implémentation de celle fmapmontrée ci-dessus est trompeuse - même si elle a la signature de type correcte (je crois que c'est la seule implémentation possible de cette signature de type), les lois du foncteur ne sont pas satisfaites. Par exemple, fmap id≠ id, parce que let (Q(f,_)) = fmap id (Q(read,"123")) in f "456"est 123, mais let (Q(f,_)) = id (Q(read,"123")) in f "456"est 456.

En fait, Fc'est seulement un profuncteur, - ce n'est ni un foncteur ni un contrefoncteur.

• Un foncteur légal qui n'est pas applicatif car la signature de type de purene peut pas être implémentée: prenez la monade Writer (a, w)et supprimez la contrainte qui wdevrait être un monoïde. Il est alors impossible de construire une valeur de type (a, w)sur a.

• Un foncteur qui n'est pas applicative car la signature de type de <*>ne peut pas être mis en œuvre: data F a = Either (Int -> a) (String -> a).

• Un foncteur qui n'est pas d'application légale même si les méthodes de classe de type peuvent être implémentées:

  data P a = P ((a -> Int) -> Maybe a)

Le constructeur de type Pest un foncteur car il n'utilise aque dans des positions covariantes.

instance Functor P where
   fmap :: (a -> b) -> P a -> P b
   fmap fab (P pa) = P (\q -> fmap fab $ pa (q . fab))

La seule implémentation possible de la signature de type de <*>est une fonction qui renvoie toujours Nothing:

 (<*>) :: P (a -> b) -> P a -> P b
 (P pfab) <*> (P pa) = \_ -> Nothing  -- fails the laws!

Mais cette implémentation ne satisfait pas à la loi d'identité des foncteurs applicatifs.

• Un foncteur qui n'est Applicativepas unMonad car la signature de type de bindne peut pas être implémentée.

Je ne connais pas de tels exemples!

• Un foncteur qui n'est Applicativepas unMonad car les lois ne peuvent pas être satisfaites même si la signature de type de bindpeut être implémentée.

Cet exemple a généré pas mal de discussions, il est donc sûr de dire que prouver cet exemple n'est pas facile. Mais plusieurs personnes l'ont vérifié indépendamment par différentes méthodes. Voir Is `data PoE a = Empty | Paire aa` une monade? pour une discussion supplémentaire.

 data B a = Maybe (a, a)
   deriving Functor

 instance Applicative B where
   pure x = Just (x, x)
   b1 <*> b2 = case (b1, b2) of
     (Just (x1, y1), Just (x2, y2)) -> Just((x1, x2), (y1, y2))
     _ -> Nothing

Il est quelque peu lourd de prouver qu'il n'y a pas d' Monadinstance légale . La raison du comportement non monadique est qu'il n'y a aucun moyen naturel d'implémenter bindquand une fonction f :: a -> B bpourrait retourner Nothingou Justpour différentes valeurs de a.

Il est peut-être plus clair d'envisager Maybe (a, a, a), qui n'est pas non plus une monade, et d'essayer de l'implémenter joinpour cela. On constatera qu'il n'y a pas de moyen de mise en œuvre intuitivement raisonnable join.

 join :: Maybe (Maybe (a, a, a), Maybe (a, a, a), Maybe (a, a, a)) -> Maybe (a, a, a)
 join Nothing = Nothing
 join Just (Nothing, Just (x1,x2,x3), Just (y1,y2,y3)) = ???
 join Just (Just (x1,x2,x3), Nothing, Just (y1,y2,y3)) = ???
 -- etc.

Dans les cas indiqués par ???, il semble clair que nous ne pouvons pas produire Just (z1, z2, z3)de manière raisonnable et symétrique sur six valeurs de type différentes a. Nous pourrions certainement choisir un sous-ensemble arbitraire de ces six valeurs, - par exemple, toujours prendre la première non vide Maybe- mais cela ne satisferait pas les lois de la monade. Le retour Nothingne satisfera pas non plus aux lois.

• Une structure de données arborescente qui n'est pas une monade même si elle a une associativité bind- mais qui ne respecte pas les lois sur l'identité.

La monade arborescente habituelle (ou "un arbre avec des branches en forme de foncteur") est définie comme

 data Tr f a = Leaf a | Branch (f (Tr f a))

Il s'agit d'une monade gratuite sur le foncteur f. La forme des données est un arbre où chaque point de branchement est un "foncteur" de sous-arbres. L'arbre binaire standard serait obtenu avec type f a = (a, a).

Si nous modifions cette structure de données en faisant également les feuilles en forme de foncteur f, nous obtenons ce que j'appelle une "semi-monade" - elle a bindqui satisfait aux lois de naturalité et d'associativité, mais sa pureméthode échoue à l'une des lois d'identité. "Les semi-monades sont des semi-groupes dans la catégorie des endofuncteurs, quel est le problème?" Ceci est la classe de type Bind.

Par souci de simplicité, je définis la joinméthode au lieu de bind:

 data Trs f a = Leaf (f a) | Branch (f (Trs f a))
 join :: Trs f (Trs f a) -> Trs f a
 join (Leaf ftrs) = Branch ftrs
 join (Branch ftrstrs) = Branch (fmap @f join ftrstrs)

La greffe de branche est standard, mais la greffe de feuille est non standard et produit a Branch. Ce n'est pas un problème pour la loi d'associativité mais viole l'une des lois d'identité.

Quand les types polynomiaux ont-ils des instances de monade?

Aucun des foncteurs Maybe (a, a)et Maybe (a, a, a)ne peut se voir attribuer une Monadinstance légale , bien qu'ils le soient évidemment Applicative.

Ces foncteurs n'ont aucune astuce - pas Voidou bottomn'importe où, pas de paresse / rigueur délicate, pas de structures infinies et pas de contraintes de classe de type. L' Applicativeinstance est complètement standard. Les fonctions returnet bindpeuvent être implémentées pour ces foncteurs mais ne satisferont pas aux lois de la monade. En d'autres termes, ces foncteurs ne sont pas des monades car il manque une structure spécifique (mais il n'est pas facile de comprendre ce qui manque exactement). Par exemple, un petit changement dans le foncteur peut en faire une monade: data Maybe a = Nothing | Just ac'est une monade. Un autre foncteur similaire data P12 a = Either a (a, a)est également une monade.

Constructions pour les monades polynomiales

En général, voici quelques constructions qui produisent des Monads licites à partir de types polynomiaux. Dans toutes ces constructions, Mest une monade:

1. type M a = Either c (w, a)où west monoïde
2. type M a = m (Either c (w, a))où mest toute monade et wtout monoïde
3. type M a = (m1 a, m2 a)où m1et où m2sont les monades
4. type M a = Either a (m a)où mest toute monade

La première construction est WriterT w (Either c), la deuxième construction est WriterT w (EitherT c m). La troisième construction est un produit de monades pure @Mpar composant : est définie comme le produit par composant de pure @m1et pure @m2, et join @Mest définie en omettant les données de produits croisés (par exemple, m1 (m1 a, m2 a)est mappée m1 (m1 a)en omettant la deuxième partie du tuple):

 join :: (m1 (m1 a, m2 a), m2 (m1 a, m2 a)) -> (m1 a, m2 a)
 join (m1x, m2x) = (join @m1 (fmap fst m1x), join @m2 (fmap snd m2x))

La quatrième construction est définie comme

 data M m a = Either a (m a)
 instance Monad m => Monad M m where
    pure x = Left x
    join :: Either (M m a) (m (M m a)) -> M m a
    join (Left mma) = mma
    join (Right me) = Right $ join @m $ fmap @m squash me where
      squash :: M m a -> m a
      squash (Left x) = pure @m x
      squash (Right ma) = ma

J'ai vérifié que les quatre constructions produisent des monades légales.

Je suppose qu'il n'y a pas d'autres constructions pour les monades polynomiales. Par exemple, le foncteur Maybe (Either (a, a) (a, a, a, a))n'est obtenu par aucune de ces constructions et n'est donc pas monadique. Cependant, Either (a, a) (a, a, a)est monadique parce qu'il est isomorphe au produit de trois monades a, a, et Maybe a. Aussi, Either (a,a) (a,a,a,a)est monadique car il est isomorphe au produit de aet Either a (a, a, a).

Les quatre constructions présentées ci-dessus nous permettront d'obtenir n'importe quelle somme de n'importe quel nombre de produits de n'importe quel nombre a, par exemple Either (Either (a, a) (a, a, a, a)) (a, a, a, a, a))et ainsi de suite. Tous ces constructeurs de types auront (au moins une) Monadinstance.

Il reste à voir, bien sûr, quels cas d'utilisation pourraient exister pour de telles monades. Un autre problème est que les Monadinstances dérivées via les constructions 1-4 ne sont généralement pas uniques. Par exemple, le constructeur de type type F a = Either a (a, a)peut recevoir une Monadinstance de deux manières: par la construction 4 en utilisant la monade (a, a), et par la construction 3 en utilisant l'isomorphisme de type Either a (a, a) = (a, Maybe a). Encore une fois, trouver des cas d'utilisation pour ces implémentations n'est pas immédiatement évident.

Une question demeure - étant donné un type de données polynomiales arbitraires, comment savoir s'il a une Monadinstance. Je ne sais pas prouver qu'il n'y a pas d'autres constructions pour les monades polynomiales. Je ne pense pas qu'il existe jusqu'à présent de théorie pour répondre à cette question.