O que é mônada indexada e a motivação para essa mônada?

Eu li que ajuda a controlar os efeitos colaterais. Mas a assinatura do tipo e a documentação não me levam a lugar nenhum.

Qual seria um exemplo de como pode ajudar a controlar os efeitos colaterais (ou qualquer outro exemplo válido)?

Como sempre, a terminologia que as pessoas usam não é totalmente consistente. Há uma variedade de noções inspiradas em mônadas, mas, estritamente falando, não são exatamente. O termo "mônada indexada" é um de vários (incluindo "monadish" e "mônada parametrizada" (o nome de Atkey para eles)) de termos usados ​​para caracterizar tal noção. (Outra noção, se você estiver interessado, é a "mônada de efeito paramétrico" de Katsumata, indexada por um monóide, onde o retorno é indexado de forma neutra e o vínculo se acumula em seu índice.)

Em primeiro lugar, vamos verificar os tipos.

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

Ou seja, o tipo de "cálculo" (ou "ação", se preferir, mas ficarei com "cálculo"), parece

m before after value

onde before, after :: statee value :: *. A ideia é capturar os meios para interagir com segurança com um sistema externo que tenha alguma noção previsível de estado. O tipo de um cálculo diz a você qual deve ser o estado em que beforeele executa, qual será o estado em que afterele executa e (como com mônadas regulares *) que tipo de values o cálculo produz.

As partes e peças usuais são - *sábias como uma mônada e - statecomo jogar dominó.

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

A noção de "seta de Kleisli" (função que produz computação) assim gerada é

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

e obtemos uma composição

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

e, como sempre, as leis garantem exatamente isso ireturne icompnos dão uma categoria

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

ou, na comédia falsa C / Java / qualquer coisa,

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

Porque se importar? Modelar "regras" de interação. Por exemplo, você não pode ejetar um DVD se não houver um na unidade, e você não pode colocar um DVD na unidade se já houver um nele. assim

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

Com isso no lugar, podemos definir os comandos "primitivos"

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

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

do qual outros são montados com ireturne ibind. Agora, posso escrever (emprestando- doanotação)

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

mas não o fisicamente impossível

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

Alternativamente, pode-se definir seus comandos primitivos diretamente

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

e instanciar o modelo genérico

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

Na verdade, dissemos o que são as flechas de Kleisli primitivas (o que um "dominó" é) e, em seguida, construímos uma noção adequada de "sequência de computação" sobre elas.

Observe que para cada mônada indexada m, a "diagonal sem mudança" m i ié uma mônada, mas, em geral, m i jnão é. Além disso, os valores não são indexados, mas os cálculos são indexados; portanto, uma mônada indexada não é apenas a ideia usual de mônada instanciada para alguma outra categoria.

Agora, olhe novamente para o tipo de flecha de Kleisli

a -> m i j b

Sabemos que devemos estar no estado ipara começar e prevemos que qualquer continuação começará do estado j. Sabemos muito sobre este sistema! Esta não é uma operação arriscada! Quando colocamos o DVD no drive, ele entra! O drive de DVD não diz qual é o estado após cada comando.

Mas isso não é verdade em geral, ao interagir com o mundo. Às vezes, você pode precisar abrir mão de algum controle e deixar o mundo fazer o que quiser. Por exemplo, se você for um servidor, poderá oferecer uma escolha ao seu cliente e o estado da sua sessão dependerá do que ele escolher. A operação de "escolha de oferta" do servidor não determina o estado resultante, mas o servidor deve ser capaz de continuar de qualquer maneira. Não é um "comando primitivo" no sentido acima, então mônadas indexadas não são uma ferramenta tão boa para modelar o cenário imprevisível .

Qual é a melhor ferramenta?

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

Biscoitos assustadores? Na verdade não, por dois motivos. Um, parece um pouco mais com o que é uma mônada, porque é uma mônada, mas acabou (state -> *)ao invés de *. Dois, se você olhar para o tipo de flecha de Kleisli,

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

você obtém o tipo de cálculos com uma pré - condiçãoa e uma pós-condição b, assim como em Good Old Hoare Logic. As afirmações em lógicas de programa levaram menos de meio século para cruzar a correspondência Curry-Howard e se tornarem tipos Haskell. O tipo de returnIxdiz "você pode alcançar qualquer pós-condição que se mantenha, simplesmente sem fazer nada", que é a regra da lógica de Hoare para "pular". A composição correspondente é a regra da lógica de Hoare para ";".

Vamos terminar examinando o tipo de bindIx, colocando todos os quantificadores em.

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

Esses foralls têm polaridade oposta. Escolhemos o estado inicial ie um cálculo que pode começar icom a pós-condição a. O mundo escolhe qualquer estado intermediário de jsua preferência, mas deve nos dar a evidência de que a pós-condição se bmantém e, de qualquer estado desse tipo, podemos prosseguir para balcançá-la. Então, em sequência, podemos alcançar a condição bdo estado i. Ao liberar nosso controle sobre os estados "depois", podemos modelar cálculos imprevisíveis .

Ambos IxMonade MonadIxsão úteis. Ambos modelam a validade de cálculos interativos com relação à mudança de estado, previsível e imprevisível, respectivamente. A previsibilidade é valiosa quando você pode obtê-la, mas às vezes a imprevisibilidade é um fato da vida. Esperançosamente, então, esta resposta dá alguma indicação do que são as mônadas indexadas, prevendo quando elas começam a ser úteis e quando elas param.

Existem pelo menos três maneiras de definir uma mônada indexada que eu conheço.

Vou me referir a essas opções como mônadas indexadas à la X , em que X ultrapassa os cientistas da computação Bob Atkey, Conor McBride e Dominic Orchard, pois é assim que costumo considerá-los. Partes dessas construções têm uma história muito mais ilustre e interpretações mais agradáveis ​​por meio da teoria das categorias, mas primeiro aprendi sobre elas associadas a esses nomes e estou tentando evitar que essa resposta se torne muito esotérica.

Atkey

O estilo de mônada indexada de Bob Atkey é trabalhar com 2 parâmetros extras para lidar com o índice da mônada.

Com isso, você obtém as definições que as pessoas lançaram em outras respostas:

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

Também podemos definir comonads indexados à la Atkey. Eu, na verdade, aproveito bastante aqueles da lensbase de código .

McBride

A próxima forma de mônada indexada é a definição de Conor McBride em seu artigo "Kleisli Arrows of Outrageous Fortune" . Em vez disso, ele usa um único parâmetro para o índice. Isso faz com que a definição de mônada indexada tenha uma forma bastante inteligente.

Se definirmos uma transformação natural usando parametricidade da seguinte forma

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

então podemos escrever a definição de McBride como

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

Isso parece bem diferente do de Atkey, mas parece mais uma Mônada normal, em vez de construir uma mônada (m :: * -> *), nós a construímos (m :: (k -> *) -> (k -> *).

Curiosamente, você pode recuperar o estilo de mônada indexada de Atkey de McBride usando um tipo de dados inteligente, que McBride, em seu estilo inimitável, escolhe dizer que você deve ler como "na chave".

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

Agora você pode resolver isso

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

que se expande para

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

só pode ser invocado quando j = i, e então uma leitura cuidadosa de ibindpode trazer de volta o mesmo que Atkeyibind . Você precisa passar essas (: =) estruturas de dados, mas elas recuperam o poder da apresentação Atkey.

Por outro lado, a apresentação de Atkey não é forte o suficiente para recuperar todos os usos da versão de McBride. O poder foi estritamente adquirido.

Outra coisa boa é que a mônada indexada de McBride é claramente uma mônada, é apenas uma mônada em uma categoria de functor diferente. Ele funciona sobre endofunctors na categoria de functores de (k -> *)a, (k -> *)em vez da categoria de functores de *a *.

Um exercício divertido é descobrir como fazer a conversão de McBride em Atkey para comonads indexados . Eu pessoalmente uso um tipo de dados 'At' para a construção "at key" no artigo de McBride. Na verdade, fui até Bob Atkey no ICFP 2013 e mencionei que o virei do avesso ao transformá-lo em um "casaco". Ele parecia visivelmente perturbado. A frase funcionou melhor na minha cabeça. =)

Pomar

Finalmente, um terceiro requerente muito menos comumente referenciado ao nome de "mônada indexada" é devido a Dominic Orchard, onde ele usa um monóide de nível de tipo para esmagar os índices. Em vez de passar pelos detalhes da construção, vou simplesmente criar um link para esta palestra:

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

Como um cenário simples, suponha que você tenha uma mônada estadual. O tipo de estado é complexo e grande, mas todos esses estados podem ser divididos em dois conjuntos: estados vermelho e azul. Algumas operações nesta mônada só fazem sentido se o estado atual for um estado azul. Entre eles, alguns manterão o estado azul ( blueToBlue), enquanto outros o tornarão vermelho ( blueToRed). Em uma mônada regular, poderíamos escrever

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

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

acionando um erro de tempo de execução, pois a segunda ação espera um estado azul. Gostaríamos de evitar isso estaticamente. A mônada indexada cumpre este objetivo:

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

Um erro de tipo é disparado porque o segundo índice de blueToRed( Red) difere do primeiro índice de blueToBlue( Blue).

Como outro exemplo, com mônadas indexadas, você pode permitir que uma mônada de estado mude o tipo de seu estado, por exemplo, você poderia ter

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

Você poderia usar o acima para construir um estado que é uma pilha heterogênea estaticamente tipada. As operações teriam tipo

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

Como outro exemplo, suponha que você queira uma mônada de IO restrita que não permita o acesso ao arquivo. Você pode usar, por exemplo

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

Desta forma, uma ação com tipo IO ... NoAccess ()é estaticamente garantida como livre de acesso ao arquivo. Em vez disso, uma ação do tipo IO ... FilesAccessed ()pode acessar arquivos. Ter uma mônada indexada significaria que você não teria que construir um tipo separado para o IO restrito, o que exigiria duplicar todas as funções não relacionadas a arquivo em ambos os tipos de IO.

Uma mônada indexada não é uma mônada específica como, por exemplo, a mônada estadual, mas uma espécie de generalização do conceito de mônada com parâmetros de tipo extras.

Enquanto um valor monádico "padrão" tem o tipo, Monad m => m aum valor em uma mônada indexada seria IndexedMonad m => m i j aonde ie jsão tipos de índice, de modo que esse ié o tipo do índice no início do cálculo monádico e jno final do cálculo. De certa forma, você pode pensar iem uma espécie de tipo de entrada e de jsaída.

Usando Statecomo exemplo, uma computação com estado State s amantém um estado do tipo em stoda a computação e retorna um resultado do tipo a. Uma versão indexada IndexedState i j a,, é um cálculo com estado em que o estado pode mudar para um tipo diferente durante o cálculo. O estado inicial tem o tipo ie o estado e o final da computação tem o tipo j.

Usar uma mônada indexada sobre uma mônada normal raramente é necessário, mas pode ser usado em alguns casos para codificar garantias estáticas mais rígidas.

Pode ser importante dar uma olhada em como a indexação é usada em tipos dependentes (por exemplo, em agda). Isso pode explicar como a indexação ajuda em geral e, em seguida, traduzir essa experiência em mônadas.

A indexação permite estabelecer relacionamentos entre instâncias particulares de tipos. Então, você pode raciocinar sobre alguns valores para estabelecer se esse relacionamento se mantém.

Por exemplo (em agda), você pode especificar que alguns números naturais estão relacionados _<_, e o tipo indica quais são os números. Então, você pode exigir que alguma função receba uma testemunha de que m < n, porque somente então a função funciona corretamente - e sem fornecer essa testemunha o programa não compilará.

Como outro exemplo, dada a perseverança e o suporte do compilador para o idioma escolhido, você pode codificar que a função assume que uma determinada lista está classificada.

As mônadas indexadas permitem codificar parte do que os sistemas de tipos dependentes fazem, para gerenciar os efeitos colaterais com mais precisão.