Qu'est-ce que la monade indexée et la motivation de cette monade?

J'ai lu que cela aide à suivre les effets secondaires. Mais la signature de type et la documentation ne me mènent nulle part.

Quel serait un exemple de la façon dont il peut aider à suivre les effets secondaires (ou tout autre exemple valable)?

Comme toujours, la terminologie utilisée par les gens n'est pas entièrement cohérente. Il existe une variété de notions inspirées par les monades mais à proprement parler qui ne sont pas tout à fait. Le terme «monade indexée» est l'un d'un certain nombre (y compris «monade» et «monade paramétrée» (le nom d'Atkey pour eux)) de termes utilisés pour caractériser une telle notion. (Une autre notion de ce type, si vous êtes intéressé, est la "monade d'effet paramétrique" de Katsumata, indexée par un monoïde, où le retour est indexé de manière neutre et la liaison s'accumule dans son index.)

Tout d'abord, vérifions les types.

IxMonad (m :: state -> state -> * -> *)

Autrement dit, le type de "calcul" (ou "action", si vous préférez, mais je m'en tiendrai à "calcul"), ressemble à

m before after value

où before, after :: stateet value :: *. L'idée est de saisir les moyens d'interagir en toute sécurité avec un système externe qui a une certaine notion prévisible d'état. Le type d'un calcul vous indique quel état doit être beforeil s'exécute, quel sera l'état afteril s'exécute et (comme avec les monades régulières sur *) quel type devalue s le calcul produit.

Les morceaux habituels sont dans le *sens comme une monade et dans le statesens comme pour jouer aux dominos.

ireturn  ::  a -> m i i a    -- returning a pure value preserves state
ibind    ::  m i j a ->      -- we can go from i to j and get an a, thence
             (a -> m j k b)  -- we can go from j to k and get a b, therefore
             -> m i k b      -- we can indeed go from i to k and get a b

La notion de "flèche de Kleisli" (fonction qui donne le calcul) ainsi générée est

a -> m i j b   -- values a in, b out; state transition i to j

et on obtient une composition

icomp :: IxMonad m => (b -> m j k c) -> (a -> m i j b) -> a -> m i k c
icomp f g = \ a -> ibind (g a) f

et, comme toujours, les lois garantissent exactement cela ireturnet icompnous donnent une catégorie

      ireturn `icomp` g = g
      f `icomp` ireturn = f
(f `icomp` g) `icomp` h = f `icomp` (g `icomp` h)

ou, dans la comédie faux C / Java / peu importe,

      g(); skip = g()
      skip; f() = f()
{g(); h()}; f() = h(); {g(); f()}

Pourquoi s'embêter? Modéliser des «règles» d'interaction. Par exemple, vous ne pouvez pas éjecter un DVD s'il n'y en a pas dans le lecteur, et vous ne pouvez pas mettre un DVD dans le lecteur s'il y en a déjà un. Alors

data DVDDrive :: Bool -> Bool -> * -> * where  -- Bool is "drive full?"
  DReturn :: a -> DVDDrive i i a
  DInsert :: DVD ->                   -- you have a DVD
             DVDDrive True k a ->     -- you know how to continue full
             DVDDrive False k a       -- so you can insert from empty
  DEject  :: (DVD ->                  -- once you receive a DVD
              DVDDrive False k a) ->  -- you know how to continue empty
             DVDDrive True k a        -- so you can eject when full

instance IxMonad DVDDrive where  -- put these methods where they need to go
  ireturn = DReturn              -- so this goes somewhere else
  ibind (DReturn a)     k  = k a
  ibind (DInsert dvd j) k  = DInsert dvd (ibind j k)
  ibind (DEject j)      k  = DEject j $ \ dvd -> ibind (j dvd) k

Avec ceci en place, nous pouvons définir les commandes "primitives"

dInsert :: DVD -> DVDDrive False True ()
dInsert dvd = DInsert dvd $ DReturn ()

dEject :: DVDrive True False DVD
dEject = DEject $ \ dvd -> DReturn dvd

à partir de laquelle d'autres sont assemblés avec ireturnet ibind. Maintenant, je peux écrire (emprunter do-notation)

discSwap :: DVD -> DVDDrive True True DVD
discSwap dvd = do dvd' <- dEject; dInsert dvd ; ireturn dvd'

mais pas l'impossible physiquement

discSwap :: DVD -> DVDDrive True True DVD
discSwap dvd = do dInsert dvd; dEject      -- ouch!

Alternativement, on peut définir directement ses commandes primitives

data DVDCommand :: Bool -> Bool -> * -> * where
  InsertC  :: DVD -> DVDCommand False True ()
  EjectC   :: DVDCommand True False DVD

puis instanciez le modèle générique

data CommandIxMonad :: (state -> state -> * -> *) ->
                        state -> state -> * -> * where
  CReturn  :: a -> CommandIxMonad c i i a
  (:?)     :: c i j a -> (a -> CommandIxMonad c j k b) ->
                CommandIxMonad c i k b

instance IxMonad (CommandIxMonad c) where
  ireturn = CReturn
  ibind (CReturn a) k  = k a
  ibind (c :? j)    k  = c :? \ a -> ibind (j a) k

En effet, nous avons dit ce que sont les flèches primitives de Kleisli (ce qu'est un "domino"), puis nous avons construit une notion appropriée de "séquence de calcul" sur elles.

Notez que pour chaque monade indexée m, la "diagonale sans changement" m i iest une monade, mais en général, m i jne l'est pas. De plus, les valeurs ne sont pas indexées mais les calculs sont indexés, donc une monade indexée n'est pas seulement l'idée habituelle de monade instanciée pour une autre catégorie.

Maintenant, regardez à nouveau le type de flèche Kleisli

a -> m i j b

Nous savons que nous devons être en état ipour commencer, et nous prédisons que toute continuation commencera par l'état j. Nous en savons beaucoup sur ce système! Ce n'est pas une opération risquée! Lorsque nous mettons le DVD dans le lecteur, il entre! Le lecteur DVD n'a aucun mot à dire sur l'état après chaque commande.

Mais ce n'est pas vrai en général, lorsqu'on interagit avec le monde. Parfois, vous devrez peut-être abandonner un peu de contrôle et laisser le monde faire ce qu'il veut. Par exemple, si vous êtes un serveur, vous pouvez proposer à votre client un choix et l'état de votre session dépendra de ce qu'il choisit. L'opération de "choix d'offre" du serveur ne détermine pas l'état résultant, mais le serveur devrait pouvoir continuer de toute façon. Ce n'est pas une "commande primitive" dans le sens ci-dessus, donc les monades indexées ne sont pas un si bon outil pour modéliser le scénario imprévisible .

Quel meilleur outil?

type f :-> g = forall state. f state -> g state

class MonadIx (m :: (state -> *) -> (state -> *)) where
  returnIx    :: x :-> m x
  flipBindIx  :: (a :-> m b) -> (m a :-> m b)  -- tidier than bindIx

Des biscuits effrayants? Pas vraiment, pour deux raisons. Un, il semble un peu plus comme ce monade est, parce qu'il est une monade, mais plus (state -> *)plutôt que *. Deux, si vous regardez le type d'une flèche Kleisli,

a :-> m b   =   forall state. a state -> m b state

vous obtenez le type de calculs avec une précondition a et une postcondition b, tout comme dans Good Old Hoare Logic. Les affirmations dans la logique des programmes ont mis moins d'un demi-siècle à traverser la correspondance Curry-Howard et à devenir des types Haskell. Le type de returnIxdit "vous pouvez réaliser n'importe quelle post-condition qui tient, juste en ne faisant rien", qui est la règle de Hoare Logic pour "sauter". La composition correspondante est la règle Hoare Logic pour ";".

Terminons en regardant le type de bindIx, en mettant tous les quantificateurs.

bindIx :: forall i. m a i -> (forall j. a j -> m b j) -> m b i

Ces foralls ont une polarité opposée. On choisit l'état initial i, et un calcul qui peut commencer à i, avec postcondition a. Le monde choisit n'importe quel état intermédiaire jqu'il aime, mais il doit nous donner la preuve que la post-condition btient, et à partir d'un tel état, nous pouvons continuer à btenir. Ainsi, en séquence, nous pouvons obtenir une condition à bpartir de l'état i. En relâchant notre emprise sur les états «après», nous pouvons modéliser des calculs imprévisibles .

Les deux IxMonadet MonadIxsont utiles. Les deux modèles de validité des calculs interactifs par rapport à l'état changeant, prévisible et imprévisible, respectivement. La prévisibilité est précieuse lorsque vous pouvez l'obtenir, mais l'imprévisibilité est parfois une réalité. Espérons donc que cette réponse donne une indication de ce que sont les monades indexées, prédisant à la fois quand elles commencent à être utiles et quand elles s'arrêtent.

Il y a au moins trois façons de définir une monade indexée que je connais.

J'appellerai ces options des monades indexées à la X , où X s'étend sur les informaticiens Bob Atkey, Conor McBride et Dominic Orchard, car c'est ainsi que j'ai tendance à les considérer. Certaines parties de ces constructions ont une histoire beaucoup plus longue et plus illustre et des interprétations plus agréables grâce à la théorie des catégories, mais j'ai d'abord appris qu'elles étaient associées à ces noms, et j'essaie d'empêcher que cette réponse ne devienne trop ésotérique.

Atkey

Le style de monade indexée de Bob Atkey est de travailler avec 2 paramètres supplémentaires pour gérer l'index de la monade.

Avec cela, vous obtenez les définitions que les gens ont jetées dans d'autres réponses:

class IMonad m where
  ireturn  ::  a -> m i i a
  ibind    ::  m i j a -> (a -> m j k b) -> m i k b

Nous pouvons également définir des comonades indexées à la Atkey. En fait, je tire beaucoup de kilomètres de ceux de la lensbase de code .

McBride

La prochaine forme de monade indexée est la définition de Conor McBride tirée de son article "Kleisli Arrows of Outrageous Fortune" . Il utilise à la place un seul paramètre pour l'index. Cela donne à la définition de la monade indexée une forme plutôt intelligente.

Si nous définissons une transformation naturelle en utilisant la paramétrie comme suit

type a ~> b = forall i. a i -> b i 

alors nous pouvons écrire la définition de McBride comme

class IMonad m where
  ireturn :: a ~> m a
  ibind :: (a ~> m b) -> (m a ~> m b)

Cela semble assez différent de celui d'Atkey, mais cela ressemble plus à une Monade normale, au lieu de construire une monade (m :: * -> *), nous la construisons (m :: (k -> *) -> (k -> *).

Il est intéressant de noter que vous pouvez en fait récupérer le style de monade indexée d'Atkey à partir de McBride en utilisant un type de données intelligent, que McBride dans son style inimitable choisit de dire que vous devriez lire comme "at key".

data (:=) :: a i j where
   V :: a -> (a := i) i

Maintenant tu peux comprendre ça

ireturn :: IMonad m => (a := j) ~> m (a := j)

qui s'étend à

ireturn :: IMonad m => (a := j) i -> m (a := j) i

ne peut être invoqué que lorsque j = i, puis une lecture attentive de ibindpeut vous ramener à la même chose que celle d'Atkeyibind . Vous devez contourner ces structures de données (: =), mais elles récupèrent la puissance de la présentation Atkey.

En revanche, la présentation Atkey n'est pas assez forte pour récupérer toutes les utilisations de la version de McBride. Le pouvoir a été strictement acquis.

Une autre bonne chose est que la monade indexée de McBride est clairement une monade, c'est juste une monade sur une catégorie de foncteurs différente. Il fonctionne sur les endofoncteurs sur la catégorie des foncteurs de (k -> *)à (k -> *)plutôt que sur la catégorie des foncteurs de *à *.

Un exercice amusant consiste à trouver comment faire la conversion McBride en Atkey pour les comonads indexés . J'utilise personnellement un type de données «At» pour la construction «at key» dans l'article de McBride. En fait, je me suis approché de Bob Atkey à l'ICFP 2013 et j'ai mentionné que je l'avais transformé à l'envers pour en faire un "manteau". Il semblait visiblement dérangé. La réplique s'est mieux déroulée dans ma tête. =)

Verger

Enfin, Dominic Orchard, où il utilise à la place un monoïde de niveau de type pour écraser les indices, est un troisième demandeur beaucoup moins souvent référencé sous le nom de "monade indexée". Plutôt que de passer en revue les détails de la construction, je vais simplement faire un lien vers cette conférence:

https://github.com/dorchard/effect-monad/blob/master/docs/ixmonad-fita14.pdf

En tant que scénario simple, supposons que vous ayez une monade d'État. Le type d'état est complexe, mais tous ces états peuvent être partitionnés en deux ensembles: les états rouge et bleu. Certaines opérations dans cette monade n'ont de sens que si l'état actuel est un état bleu. Parmi ceux-ci, certains garderont l'état bleu ( blueToBlue), tandis que d'autres le rendront rouge ( blueToRed). Dans une monade ordinaire, nous pourrions écrire

blueToRed  :: State S ()
blueToBlue :: State S ()

foo :: State S ()
foo = do blueToRed
         blueToBlue

déclenchant une erreur d'exécution car la deuxième action attend un état bleu. Nous aimerions éviter cela de manière statique. La monade indexée remplit cet objectif:

data Red
data Blue

-- assume a new indexed State monad
blueToRed  :: State S Blue Red  ()
blueToBlue :: State S Blue Blue ()

foo :: State S ?? ?? ()
foo = blueToRed `ibind` \_ ->
      blueToBlue          -- type error

Une erreur de type est déclenchée car le deuxième index de blueToRed( Red) diffère du premier index de blueToBlue( Blue).

Comme autre exemple, avec les monades indexées, vous pouvez autoriser une monade d'état à changer le type de son état, par exemple vous pourriez avoir

data State old new a = State (old -> (new, a))

Vous pouvez utiliser ce qui précède pour créer un état qui est une pile hétérogène de type statique. Les opérations auraient le type

push :: a -> State old (a,old) ()
pop  :: State (a,new) new a

Comme autre exemple, supposons que vous vouliez une monade IO restreinte qui n'autorise pas l'accès aux fichiers. Vous pouvez utiliser par exemple

openFile :: IO any FilesAccessed ()
newIORef :: a -> IO any any (IORef a)
-- no operation of type :: IO any NoAccess _

De cette manière, une action de type IO ... NoAccess ()est statiquement garantie sans accès aux fichiers. Au lieu de cela, une action de type IO ... FilesAccessed ()peut accéder aux fichiers. Avoir une monade indexée signifierait que vous n'avez pas à créer un type distinct pour l'E / S restreinte, ce qui nécessiterait de dupliquer chaque fonction non liée à un fichier dans les deux types d'E / S.

Une monade indexée n'est pas une monade spécifique comme, par exemple, la monade d'état, mais une sorte de généralisation du concept de monade avec des paramètres de type supplémentaires.

Alors qu'une valeur monadique "standard" a le type, Monad m => m aune valeur dans une monade indexée serait IndexedMonad m => m i j aoù iet jsont des types d'index de sorte que ic'est le type de l'index au début du calcul monadique et jà la fin du calcul. D'une certaine manière, vous pouvez penser ià une sorte de type d'entrée et jde type de sortie.

En utilisant Statecomme exemple, un calcul avec état State s amaintient un état de type stout au long du calcul et renvoie un résultat de type a. Une version indexée IndexedState i j a, est un calcul avec état dans lequel l'état peut passer à un type différent pendant le calcul. L'état initial a le type iet l'état et la fin du calcul a le typej .

L'utilisation d'une monade indexée sur une monade normale est rarement nécessaire mais elle peut être utilisée dans certains cas pour coder des garanties statiques plus strictes.

Il peut être important de regarder comment l'indexation est utilisée dans les types dépendants (par exemple dans agda). Cela peut expliquer comment l'indexation aide en général, puis traduire cette expérience en monades.

L'indexation permet d'établir des relations entre des instances particulières de types. Ensuite, vous pouvez raisonner sur certaines valeurs pour déterminer si cette relation tient.

Par exemple (dans agda), vous pouvez spécifier que certains nombres naturels sont liés _<_, et le type indique de quels nombres ils sont. Ensuite, vous pouvez exiger qu'une fonction soit donnée à un témoin quim < n , parce que ce n'est qu'alors que la fonction fonctionne correctement - et sans fournir un tel témoin, le programme ne se compilera pas.

Comme autre exemple, étant donné suffisamment de persévérance et de support du compilateur pour le langage choisi, vous pouvez coder que la fonction suppose qu'une certaine liste est triée.

Les monades indexées permettent d'encoder une partie de ce que font les systèmes de types dépendants, pour gérer plus précisément les effets secondaires.