Como o IO é uma mônada?

7

Estou aprendendo a linguagem de programação Haskell. Pelo que estou lendo, Input / Ouput ( IO ) levanta desafios para a pureza de Haskell, pois, por definição, estamos interagindo com o mundo exterior. Da Wikipedia:

Em uma linguagem puramente funcional, como Haskell, as funções não podem ter efeitos colaterais visíveis externamente como parte da semântica da função. Embora uma função não possa causar diretamente um efeito colateral, ela pode criar um valor que descreva o efeito colateral desejado, que o chamador deve aplicar em um momento conveniente.

Na notação Haskell, um valor do tipo IO a representa uma ação que, quando executada, produz um valor do tipo a.

Logo aprendi que IO é um exemplo de uma mônada de Haskell. Embora não tenhamos muitas explicações sobre o que são mônadas. De Functors, candidatos e mônadas em imagens

Como aprender sobre as Mônadas:

  1. Obter um PhD em ciência da computação.
  2. Jogue fora, porque você não precisa para esta seção!

Até agora, já li várias definições de - que elas adicionam contexto ou criam linguagens de programação menores dentro de uma grande em torno de um conceito específico. Ainda tentando entender o que as mônadas e como essas idéias se aplicam.

Em Haskell, monadhá outra classe tipográfica, com basicamente apenas uma regra definindo-a. E IOé um exemplo disso.

class Monad m where    
    (>>=) :: m a -> (a -> m b) -> m b  

/programming/44965/what-is-a-monad

Há algo algébrico acontecendo aqui? O que há de algébrico no IO?


Peço desculpas por ser específico do idioma. Minha esperança é que a maior parte dessa discussão se aplique a todas as linguagens de programação funcionais. Quaisquer erros na minha discussão representam meu próprio entendimento limitado dessa área.

Há outra definição de mônada que encontrei no nLab que nem sequer é específica para linguagens de programação.

Em uma pergunta à parte, eu gostaria de entender como a noção de mônada da teoria da categoria corresponde à definição de CS no caso de Haskell.

john mangual
fonte

Respostas:

9

TLDR: Os tipos e funções Haskell formam uma categoria e, a partir disso, percebemos que as coisas cumprem >>=e returncumprem as regras das mônadas.

Para considerar o que significa para algum tipo fazer parte de um trigêmeo de mônada, devemos primeiro considerar o que significa uma categoria no sentido de Haskell.

Deixamos que nossa categoria Haskseja definida com objetos como tipos e setas Haskell para serem funções. Cada seta de identidade é uma instância ide a composição é normal .. É trivial ver que elas satisfazem as condições normais de coerência.

Agora podemos ver os endofuncionários em Hask. Eles contêm duas partes, um mapa de tipos para tipos e um mapa de funções para funções, para que

  • map g . map f = map (g . f)
  • map id = id

Functors são, portanto, construtores de tipos (que mapeiam tipos para tipos) emparelhados com uma função mapque eleva setas a -> bem setas F a -> F b. Também podemos definir transformações naturais entre eles como algo que "desliza" um membro F apara um membro de G asatisfazer as condições normais de coerência

  • nat . fmap f = fmap f . nat

Então, podemos concluir que uma transformação natural é algo do tipo

nat :: forall a. F a -> G a

Finalmente, observamos que o construtor do tipo de identidade

type Id a = a

é um functor com seu mapa dado por identidade.

Agora estamos preparados para discutir mônadas! Uma mônada é um trio de três coisas,

  • Um functor, F
  • Uma transformação natural returnentre IdeF
  • Uma transformação natural joinentre F x FeF

Com as condições de coerência que join . fmap join = join . joine join . fmap return = join . return = id.

onde xsignifica o produto de dois functores que é apenas definido pela composição dos construtores de tipo.

A IOmônada tem umreturn :: a -> IO a Id a -> IO a. Essa é a nossa primeira transformação natural. Nosso segundo não é tão fácil, mas podemos definir joincomo

join :: IO (IO a) -> IO a
join = (>>= id)

Podemos ver joincomo uma operação de seqüenciamento. Ele pega todas as ações armazenadas na estrutura externa IOe as coloca na frente de todas as ações internas IO, retornando uma maior, porém plana IO a.

Portanto, em essência, temos essa noção abstrata de mônadas na teoria das categorias e, como os tipos Haskell podem ser vistos como uma categoria, podemos aplicar noções teóricas de categorias normais, como mônadas, e obter padrões comuns delas. É isso aí. Não existe uma teoria secreta da categoria que dê mais significado às mônadas além dessas condições de coerência.

Este é realmente um padrão bastante comum. Sempre que vemos algo com categorias, seja lógica, semântica ou sistemas de tipos, podemos aplicar cegamente os últimos 100 anos de pesquisa em nossa nova categoria e descobrir "novas" abstrações.

Daniel Gratzer
fonte