Introdução

Mônadas são uma maneira de estruturar computações que envolvem efeitos colaterais em linguagens de programação funcional. O conceito de mônada foi desenvolvido na matemática e utilizado, primeiramente, em semântica denotacional para formalização de efeitos colaterais. O uso de mônadas foi popularizado pela linguagem Haskell que as utiliza para estruturar programas que envolvem I/O e manipulação de estado entre outros tipos de efeitos colaterais.

Nesse post apresentaremos como classes de tipos em Coq podem ser utilizadas para definir mônadas e alguns exemplos de como essas podem estruturar programas envolvendo efeitos diversos.

Definindo uma mônada

De maneira simples, uma mônada é um construtor de tipos (mais precisamente, uma função M : Type -> Type) que possui duas operações:

• ret : A -> M A, que converte um valor A qualquer em uma computação que retorna, como resultado um valor desse tipo.

• bind : M A -> (A -> M B) -> M B, que compõe duas computações permitindo que a segunda utilize o resultado da primeira.

Abaixo apresentamos a definição de mônada como uma classe de tipos e notações para facilitar sua utilização.

Class Monad (M : Type -> Type) : Type
  :={
      ret : forall {A : Type}, A -> M A
    ; bind : forall {A B : Type}, M A -> (A -> M B) -> M B
    }.

Notation "x <- c1 ;; c2" := (bind c1 (fun x => c2)) 
                           (right associativity, at level 84, c1 at next level).

Notation "c1 ;; c2" := (bind c1 (fun _ => c2)) (at level 100, right associativity).

A mônada option

Um exemplo de instância para essa classe usa o tipo option. De maneira simples, essa mônada (option) define computações que podem falhar.

Instance option_monad : Monad option
  :={
      ret := fun {A : Type}(x : A) => Some x 
    ; bind := fun {A B : Type}(x : option A)(f : A -> option B) =>
                match x with
                | None => None
                | Some y => f y
                end
    }.

Um possível uso dessa mônada seria para definir a operação de subtração sobre números naturais.

Fixpoint subtract (n m : nat) : option nat :=
  match n, m with
  | n' , 0 => ret n'
  | 0  , _ => None
  | S n', S m' => subtract n' m'
  end.

Usando a mônada definida, podemos escrever de maneira simples um avaliador de expressões aritméticas que usam a subtração.

Inductive exp : Set :=
| Num : nat -> exp
| Plus : exp -> exp -> exp
| Minus : exp -> exp -> exp.

Fixpoint eval (e : exp) : option nat :=
  match e with
  | Num n => ret n
  | Plus e1 e2 =>
      n1 <- eval e1 ;;
      n2 <- eval e2 ;;
      ret (n1 + n2)
  | Minus e1 e2 =>
      n1 <- eval e1 ;;
      n2 <- eval e2 ;;
      subtract n1 n2
  end.

A mônada err

Apesar de útul para definir computações parciais, a mônada option possui um inconveniente: ela não permite que informações sobre o tipo de falha sejam retornas pela computação que a ocasionou. Uma outra possibilidade para a modelagem deste tipo de situação é usar o tipo de dados err.

Inductive err (A : Type) : Type :=
| Ok : A -> err A | Fail : string -> err A.

O construtor Ok denota o sucesso, retornando um valor de tipo A e Fail denota a falha, armazendo uma string que a descreve. Podemos definir uma instância de Monad para err de maneira similar à mônada para option.

Instance err_monad : Monad err
  :={
      ret := fun {A : Type}(x : A) => Ok x
      ; bind := fun {A B : Type}(x : err A)(f : A -> err B) =>
                  match x with
                  | Ok y => f y
                  | Fail s => Fail s
                  end
    }.

Utilizando a mônada err, podemos interpretar as expressões aritméticas indicando quando ocorre um erro de “underflow”.

Fixpoint eval' (e : exp) : err nat :=
  match e with
  | Num n => ret n
  | Plus e1 e2 =>
      n1 <- eval' e1 ;;
      n2 <- eval' e2 ;;
      ret (n1 + n2)
  | Minus e1 e2 =>
      n1 <- eval' e1 ;;
      n2 <- eval' e2 ;;
      match subtract n1 n2 with
      | None => Fail "underflow"
      | Some m => ret m
      end
  end.

A mônada de estado

A mônada de estado permite utilizarmos valores que podem ser modificados durante a execução de uma computação. Mostraremos como utilizar essa mônada para implementar um interpretador para uma linguagem que provê suporte a variáveis.

Primeiramente, definimos variáveis como sendo do string.

Definition var := string.

A sintaxe de expressões possui variáveis, soma, multiplicação, atribuição (Set_s), sequência (Seq_s) e um condicional.

Inductive exp_s : Type := 
| Var_s : var -> exp_s
| Plus_s : exp_s -> exp_s -> exp_s
| Times_s : exp_s -> exp_s -> exp_s
| Set_s : var -> exp_s -> exp_s
| Seq_s : exp_s -> exp_s -> exp_s
| If0_s : exp_s -> exp_s -> exp_s -> exp_s.

Para representação do estado, ou seja, do valor associado a cada uma das variáveis utilizadas, utilizaremos uma função de tipo var -> nat.

Definition state := var -> nat.

Na sequência, definimos uma função para atualizar o valor de uma variável em um estado. Utilizamos a função string_dec, da biblioteca de Coq, que realiza o teste de igualdade de duas strings.

Definition upd(x:var)(n:nat)(s:state) : state :=
  fun v => if string_dec x v then n else s x.

De posse dessa infraestrutura, podemos definir o tipo que será utilizado pela mônada de estado. De maneira simples, a mônada de estado é uma função que a partir do estado atual produz um par formado por um (possivelmente) novo estado e resultado da computação realizada. A definição da mônada simplesmente faz a composição de computações passando o estado atualizado para a próxima computação na sequência.

Definition state_comp (A:Type) := state -> (state * A).

Instance state_monad : Monad state_comp := {
  ret := fun {A:Type} (x:A) => (fun (s:state) => (s,x)) ; 
  bind := fun {A B:Type} (c : state_comp A) (f: A -> state_comp B) => 
            fun (s:state) => 
              let (s',v) := c s in 
              f v s'
}.

Visando facilitar a definição do interpretador, vamos definir funções para a leitura e escrita de valores em variáveis.

Definition read (x:var) : state_comp nat := 
  fun s => (s, s x).

Definition write (x:var) (n:nat) : state_comp nat := 
  fun s => (upd x n s, n).

O intepretador para a linguagem de expressões possui implementação direta.

Fixpoint eval_sm (e:exp_s) : state_comp nat := 
  match e with 
    | Var_s x => read x
    | Plus_s e1 e2 => 
      n1 <- eval_sm e1 ;; 
      n2 <- eval_sm e2 ;; 
      ret (n1 + n2)
    | Times_s e1 e2 =>
      n1 <- eval_sm e1 ;; 
      n2 <- eval_sm e2 ;; 
      ret (n1 * n2)
    | Set_s x e => 
      n <- eval_sm e ;; 
      write x n 
    | Seq_s e1 e2 => 
      _ <- eval_sm e1 ;; 
      eval_sm e2
    | If0_s e1 e2 e3 => 
      n <- eval_sm e1 ;;
      match n with 
        | 0 => eval_sm e2
        | _ => eval_sm e3 
      end
  end.

Conclusão

Nesse post apresentamos como mônadas podem ser definidas em Coq usando o mecanismo de classes de tipos. Foram implementadas três versões de intepretadores para expressões possuindo diferentes tipos de efeitos colaterais e como esses podem ser desenvolvidos como instâncias da classe Monad apresentada.

Um ponto não desenvolvido nesse post é como demonstrar propriedades de mônadas. Para um tipo M ser considerado uma mônada, esse deve possuir operações ret e bind de forma que:

• ret é identidade a direita e a esquerda para bind.
• bind é associativo.

De maneira simples, essas operações devem formar um monóide. Abaixo apresentamos uma classe de tipos para representar propriedades de uma mônada e a prova de que a mônada option as satisfaz.

Todo o código desenvolvido nesse post está disponível no seguinte gist.

Class Monad_with_Laws (M: Type -> Type){MonadM : Monad M} :=
{
  m_left_id : forall {A B:Type} (x:A) (f:A -> M B), bind (ret x) f = f x ;
  m_right_id : forall {A B:Type} (c:M A), bind c ret = c ;
  m_assoc : forall {A B C} (c:M A) (f:A->M B) (g:B -> M C), 
    bind (bind c f) g = bind c (fun x => bind (f x) g)
}.


Instance OptionMonadLaws : @Monad_with_Laws option _ := {}.
  auto.
  intros ; destruct c ; auto.
  intros ; destruct c ; auto.
Defined.