Archive for the ‘Programação Funcional’ Category

Provando a Comutatividade da Adição em Agda

maio 23, 2011

Uma das primeiras demonstrações realizadas por todos que utilizam assistentes de provas (ou, linguagens com suporte a tipos dependentes), é a prova formal de que a adição é uma operação comutativa. Por isto, neste post, pretendo apresentar a prova de que a adição é comutativa utilizando a linguagem Agda.

Agda é uma linguagem com suporte a tipos dependentes. Por isso, permite a escrita de proposições e provas na mesma linguagem que escrevemos tipos e programas. Se você não conhece nada sobre Agda, pode julgar interessante este post.

1. Definindo o que é comutatividade.

A comutatividade é uma propriedade tão natural que muitas vezes esquecemos de sua definição formal.  Seja \circ uma operação binária sobre um conjunto A. Dizemos que \circ é comutativa se e somente se:

\forall\,n\,m\in\,A.\, n\,\circ\,m\,=\,m\,\circ\,n

Isso é, se a ordem de aplicação dos parâmetros n e m for irrelevante para \circ, dizemos que esta operação é comutativa.

Mas agora surge a seguinte questão: como provar que a adição é comutativa? Isso é o que abordarei a partir de agora.

2. Uma Prova Informal

Ao tentar utilizar um assistente de provas para a formalização de algum teorema é importante saber como construir a prova “no papel”.

Mas qual a razão disso, já que utilizamos assistentes de provas justamente para não realizar provas “no papel”?

Ao tentarmos provar algum teorema em um assistente de provas sem ter a mínima idéia de como prová-lo, corre-se o risco de simplesmente não conseguirmos provar nada. Isso acontece porquê ao utilizar assistentes de prova, temos que formalizar cada mínima etapa de raciocínio, o que muitas vezes fica sub-entendido em provas convencionais.

Para demonstrar que a adição é comutativa, devemos provar que:

\forall\,n\,m\in\,A.\, n\,\circ\,m\,=\,m\,\circ\,n

Portanto, devemos supor n e m arbitrários e na sequência proceder por indução sobre m (observação: esta indução poderia ser sobre n, mas faremos indução sobre m para ser coerente com a prova a ser apresentada em Agda).

No caso m = 0 temos que:

\begin{array}{lcll}n+m & = & n + 0 & \{\text{como m = 0}\}\\ & = & n & \{\text{por n + 0 = n}\}\\ & = & 0 + n & \{\text{por n = 0 + n}\}\\ & = & m + n _{\Box}& \{\text{como m = 0}\}\end{array}

Seja m = m_{1} + 1 e suponha que n + m_{1} = m_{1} + n. Temos que:

\begin{array}{lcll}n+m & = & n + (m_{1} + 1) & \{\text{como m = m1 + 1}\}\\ & = & (n + m_{1}) + 1 & \{\text{por associatividade}\}\\ & = & (m_{1} + n) + 1 & \{\text{pela h.i.}\}\\ & = & (m_{1} + 1) + n & \{\text{por (n+m)+1 = (n+1) +m}\}\\ & = & m + n _{\Box} &\{\text{por m1 + 1 = m}\} \end{array}

Simples, não? Aliás, é um resultado tão direto que não precisa de prova, mas para construir esta prova em Agda, teremos que provar diversos detalhes que na prova anterior foram aceitos como verdade a priori.

3. A Prova em Agda

Para mostrar, em Agda, que a adição é comutativa,  precisamos primeiro de algumas definições. A primeira delas é, evidentemente, o tipo que define números naturais:

data N : Set where
   zero : N
   succ : N -> N

e uma função para a adição, cuja definição é direta:

_+_ : N -> N -> N
zero + m = m
(succ n) + m = succ (n + m)

Ao contrário de outras linguagens, em Agda, devemos definir praticamente tudo “do zero”, inclusive definições simples como números naturais e adição. Uma funcionalidade que está disponível a priori em quase todas as linguagens de programação é a noção de igualdade. Em Agda, tal noção deve ser implementada manualmente. A próxima seção apresenta a definição de igualdade e alguns resultados sobre esta.

3.1. Igualdade em Agda

Quando lidamos com assistentes de provas, a igualdade é um assunto um pouco problemático. Isso ocorre porquê, em primeiro lugar, a igualdade não é definida (ou decidível) para todos os tipos. Neste post consideraremos apenas a forma mais simples de igualdade, chamada de igualdade proposicional.

A igualdade é codificada pelo seguinte tipo de dados Agda:

data _=_ {A : Set} (x : A) : A -> Set where
     refl : x = x

Isso é, para qualquer valor x de um tipo A qualquer, temos que o construtor refl representa provas de x = x. Para ficar um pouco mais claro, considere a seguinte definição:

oneequalone : 1 = 1
oneequalone = refl

A definição anterior mostra uma prova de que 1 = 1! A primeira vista, parece estranho… pois, para provar isto utilizamos apenas o construtor refl. Mas, de acordo com a definição deste construtor, ele representa provas de que x = x, para qualquer valor x.

A igualdade possui algumas propriedades interessantes. A primeira delas é a transistividade, isto é, se x = y e y = z então x = z. Esta propriedade é representada pelo seguinte teorema Agda:

trans : {A : Set}{x y z : A} -> x = y -> y = z -> x = z
trans refl refl = refl

Mas, isto é apenas uma definição de função! Mas, de acordo com o isomorfismo de Curry-Howard, tipos em linguagens funcionais podem ser pensados como fórmulas da lógica de primeira ordem.  Uma vez que tipos são vistos como fórmulas lógicas, funções de um tipo podem ser vistas como provas da fórmula representada por seu tipo.

No trecho de código anterior temos que o tipo:

trans : {A : Set}{x y z : A} -> x = y -> y = z -> x = z

representa a seguinte fórmula da lógica de primeira ordem:

\forall x\,y\,z\in\,A. x = y \rightarrow y = z \rightarrow x = z

Como o resultado do teorema trans é uma igualdade, temos que refl é o termo que representa esta prova.

Outra propriedade da igualdade que é útil é a chamada congruência, apresentada no trecho de código seguinte:

cong : {A : Set}{f : A -> Set}{x y : A} -> x = y -> f x = f y
cong f refl = refl

A congruência mostra que a igualdade é preservada pela aplicação de funções. Novamente, como a prova envolve uma igualdade, esta é simplesmente o termo refl.

Agora que temos a definição de igualdade e alguns lemas sobre esta podemos começar a demonstrar que a adição é comutativa.

3.2. Alguns Lemas

Se observarmos atentamente a prova informal da comutatividade da adição, podemos perceber que utilizamos alguns fatos que consideramos como verdade, sem demonstrações. Os fatos são:

  • \forall n\,\in\,\mathbb{N}.n+0 = n
  • associatividade da adição.

Estes fatos não podem ser aceitos a priori em Agda. Estes devem ser demonstrados. Como ambas as provas envolvem a adição, que é definida recursivamente sobre números naturais, então, nada mais natural que provar estas propriedades por indução sobe algum dos parâmetros da adição.

Provas por indução em Agda nada mais são que funções recursivas! Portanto, uma prova por indução sobre algum parâmetro da adição nada mais é que uma função recursiva sobre este parâmetro.

O primeiro lema a ser provado é:

\forall n\,\in\,\mathbb{N}.n+0 = n

Como o único parâmetro da adição que podemos utilizar recursão é n, temos que este lema nada mais é que uma função recursiva sobre n. A definição desta segue abaixo:

n+0=n : \forall (n : N) -> (n + 0) = n
n+0=n zero = refl
n+0=n (succ n') = cong succ (n+0=n n')

O caso base desta prova (n = 0) é direto. Já que n = 0, temos que:

\begin{array}{lcll}n+ 0 & = & 0 + 0 & \{\text{como n = 0}\}\\ & = & 0 & \{\text{como 0 + 0 = 0}\}\\ & = & n & \{\text{como n = 0}\}\end{array}

Todos os detalhes desta manipulação algébrica são realizados diretamente pelo próprio sistema de tipos de Agda, que é capaz de “entender” que, a partir da definição da adição, é possível inferir que n+0 = 0, se n= 0. Novamente, como o resultado deste caso é, em última instância, uma igualdade da forma 0 = 0, temos que o termo refl é a definição necessária.

A parte interessante dessa demonstração é o caso indutivo (recursivo). Em provas por indução em Agda, utilizar a chamada hipótese de indução é o mesmo que realizar uma chamada recursiva à função que implementa o teorema a ser provado. No lema anterior, temos que a chamada:

(n+0=n n’)

representa exatamente a utilização da hipótese de indução sobre um valor n’, que é tal que n= succ n'. Este termo, possui o seguinte tipo:

n’ + 0 = n’

Mas como n = succ n’, um termo deste tipo não constitui uma prova para o lema que desejamos provar. O termo que buscamos deve possuir o tipo:

n + 0 = n

parece que não há como prosseguir com a prova, não é mesmo? Se observamos estes dois tipos, vemos que estes são iguais a menos de uma aplicação da função de sucessor, isto é:

n + 0 = n \Leftrightarrow succ (n' + 0) = succ\, n'

Portanto, podemos resolver isso meramente utilizando congruência! Com isso temos que o caso indutivo deste lema é:

n+0=n (succ n’) = cong succ (n+0=n n’)

Simples não?

Para a provar a comutatividade não precisamos de uma versão “geral” da associatividade, mas sim uma versão mais simples. Cuja prova é apresentada a seguir. Faremos a prova por indução sobre n:

sn+m=sn+sm : \forall (n m : N) -> (n + (succ m)) = (succ (n + m))
sn+m=sn+sm zero m = refl
sn+m=sn+sm (succ n') m = cong succ (sn+m=sn+sm n' m)

esta prova possui estrutura similar ao primeiro lema apresentado. Aconselho ao leitor a tentar compreender o raciocínio utilizado. De posse destes dois lemas, podemos finalmente provar a comutatividade da adição.

3.3. Comutatividade da Adição – A prova.

De posse destes dois lemas, podemos provar a comutatividade da adição. Primeiramente, o tipo Agda que representa a fórmula lógica a ser provada é:

n+m=m+n : \forall (n m : N) -> n + m = m + n

A prova será por indução sobre m, de maneira similar a prova informal apresentada na seção 2. Para o caso base, utilizaremos o lema n+0=n, isto é:

n+m=m+n : \forall (n m : N) -> n + m = m + n
n+m=m+n n zero = n+0=n n

Para o caso indutivo, utilizaremos a hipótese de indução, junto com congruência:

n+m=m+n : \forall (n m : N) -> n + m = m + n
n+m=m+n n zero = n+0=n n
n+m=m+n n (succ m') = (cong succ (n+m=m+n n m'))

Porém o tipo de

cong succ (n+m=m+n n m’)

é:

succ (n+m’) = succ (m’+n)

que não é redutível a

n + m = m + n

considerando m = succ m'. Então o que está faltando? O tipo:

succ (n + m’) = succ (m’ + n)

de acordo com a definição de soma é idêntico a:

(succ n) + m’ = (succ m’) + n

que ainda não é igual ao tipo n + m = m + n… Então o que fazer? A solução para este dilema encontra-se em dois lemas ainda não utilizados: a transitividade da igualdade e a associatividade da adição. O lemma da associatividade prova a seguinte fórmula:

sn+m=sn+sm : \forall (n m : N) -> (n + (succ m)) = (succ (n + m))

e a hipótese de indução da comutatividade prova que:

succ (n + m’) = succ (m’ + n)

que é igual a:

succ (n + m’) = (succ m’) + n

e como m = succ\, m', temos que:

succ (n + m’) = m + n

Portanto, para terminar a prova, basta aplicar a transitividade da igualdade a estes dois lemas! A versão final do  teorema é:

n+m=m+n : \forall (n m : N) -> n + m = m + n
n+m=m+n n zero = n+0=n n
n+m=m+n n (succ m') = trans (sn+m=sn+sm n m')(cong succ (n+m=m+n n m'))

Totalmente demais!

4 . Conclusão

Neste post foi apresentada uma prova, passo-a-passo da comutatividade da adição em Agda. Provar teoremas em Agda é uma tarefa árdua (e viciante!) devido a falta de ferramentas que permitam a automação de provas simples (mas entendiantes) como esta que envolve meramente manipulação algébrica.

O principal objetivo do post foi mostrar como uma linguagem com tipos dependentes pode ser utilizada para formalizar teoremas matemáticos, utilizando o isomorfismo de Curry-Howard.

Anúncios

Efeitos Colaterais em Haskell

abril 23, 2011

Ser puro ou impuro? Eis a questão!

Atualmente a comunidade de pesquisa em linguagens funcionais debate incessantemente sobre o tema de qual a melhor maneira de manipular efeitos (estado, I/O, logging, continuações, …) .  Existem duas correntes principais:

  • Linguagens funcionais “puras”, como Haskell, que são baseadas na noção matemática de que uma função consiste no simples mapeamento de seus argumentos em seus respectivos resultados.
  • Linguagens funcionais impuras, como ML, que estendem esta noção com “efeitos” como atribuições, exceções, etc.

Linguagens puras são mais simples, por permitirem que raciocínio algébrico padrão da matemática seja utilizado em seus programas sem maiores problemas (o que facilita a prova de corretude de programas) . Além disso, essas linguagens permitem a utilização de avaliação sobre demanda. Porém linguagens impuras tendem a ser mais eficientes.

Diante de tal impasse, na década de 90 iniciaram-se diversas pesquisas visando integrar as abordagens puras e impuras, utilizando o conceito matemático de mônadas. Neste post, irei apresentar como mônadas podem ser utilizadas para permitir o desenvolvimento de programas effect-ivos (programas com efeitos) em Haskell.

Reutilizando padrões de computação

Mônadas são um exemplo de uma idéia recorrente em computação de reutilizar padrões de programas. Antes de considerarmos mônadas, vamos rever como podemos reutilizar padrões de computação em linguagens funcionais, utilizando dois exemplos simples:

   inc :: [Int] -> [Int]
   inc [ ] = [ ]
   inc (x:xs) = (x + 1) : inc xs

   sqr :: [Int] -> [Int]
   sqr [ ] = [ ]
   sqr (x:xs) = x ^ 2 : sqr xs

É simples observar que  as funções anteriores possuem a mesma estrutura, ambas quando aplicadas a uma lista vazia a retornam e quando a lista é não vazia, aplicam uma função à cabeça desta lista e repetem o processo para a cauda desta lista. A reutilização de tal padrão de computação nos leva a função map, presente na biblioteca de Haskell:

    map :: (a -> b) -> [a] -> [b]
    map f []     = []
    map f (x:xs) = f x : map f xs

Utilizando map, as duas funções anteriores podem ser descritas de maneira mais compacta:

    inc = map (+1)
    sqr = map (^2)

Avaliando expressões aritméticas

Sem sombra de dúvida, o exemplo mais utilizado para mostrar o poder de linguagens funcionais é a codificação de interpretadores de alguma linguagem. Considere, a seguinte linguagem simples de expressões que é constituída de constantes inteiras e um operador de divisão:

   data Expr = Val Int | Div Expr Expr

A função que avalia tais expressões possui uma implementação direta:

  eval :: Expr -> Int
  eval (Val n) =  n
  eval (Div x y) =  eval x `div` eval y

Porém,esta função não leva em consideração a possibilidade de uma divisão por zero, e irá produzir um erro em tempo de execução neste caso. Para lidar com este problema de maneira simples, podemos utilizar o tipo de dados Maybe

data Maybe a = Nothing | Just a

para definir uma versão “segura” (isto é, que não causa erros em tempo de execução) da divisão:

safediv :: Int -> Int -> Maybe Int
safediv n m =  if m == 0 then Nothing else Just (n `div` m)

e então realizar as mudanças necessárias na função que interpreta as expressões, como mostrado no trecho seguinte:

eval :: Expr -> Maybe Int
eval (Val n)   =  Just n
eval (Div x y) =  case eval x of
                    Nothing -> Nothing
                    Just n   -> case eval y of
                                 Nothing -> Nothing
                                 Just m  -> safediv n m

Assim como na seção anterior, pode-se observar um padrão nesta definição: um casamento de padrão sobre um valor do tipo Maybe, mapeando valores Nothing neles próprios, e valores da forma Just x em algum resultado que depende de alguma maneira de x.

Mas como este padrão pode ser reutilizado? Uma abordagem seria observar que a chave de avaliar uma divisão é realizar um casamento de padrão sobre dois valores do tipo Maybe que resultam de avaliar ambos os argumentos da divisão. Sendo assim, pode-se definir uma função para abstrair este casamento de padrão:

seqn  :: Maybe a -> Maybe b -> Maybe (a,b)
seqn Nothing   _        =  Nothing
seqn _         Nothing  =  Nothing
seqn (Just x)  (Just y) =  Just (x,y)

Usando seqn pode-se definir a avaliação de expressões de maneira mais elegante e compacta:

eval (Val n)   = Just n
eval (Div x y) = apply f (eval x `seqn` eval y)
                 where f (n,m) = safediv n m

A função apply é uma simples aplicação par ao tipo Maybe e é usada para processar o resultado de duas avaliações:

apply :: (a -> Maybe b) -> Maybe a -> Maybe b
apply f Nothing  =  Nothing
apply f (Just x) =  f x

Tudo parece muito bom! Porém a função seqn pode tornar o código uma “baderna”  se tentarmos manipular tuplas aninhadas.  Suponha, como exemplo, que nossa linguagem de expressões possuísse suporte a operadores de três argumentos. A avaliação de tal operador é apresentada no trecho de código seguinte:

eval (Op x y z) = apply f (eval x `seqn` (eval y `seqn` eval z))
                  where f (a,(b,c)) = ...

Reutilizando sequenciamento e processamento

O problema de tuplas aninhadas pode ser evitado ao novamente observar que isso nada mais é que “um casamento de padrão sobre valores do tipo Maybe, que preserva valores da forma Nothing e transforma valores da forma Just x em algo que depende de x.” A reutilização deste padrão é feita pelo operador definido a seguir:

(>>=) :: Maybe a -> (a -> Maybe b) -> Maybe b
Nothing  >>= _ = Nothing
(Just x) >>= f = f x

Se o primeiro argumento é da forma Nothing, então o segundo argumento é ignorado e Nothing é retornado como resultado. Caso contrário, se o primeiro argumento é da forma (Just x), então o segundo argumento é aplicado a x para obter um resultado de tipo Maybe b. Simples, não?

O operador >= evita o problema do aninhamento de tuplas de resultados porque o resultado do primeiro argumento é disponibilizado diretamente para processamento pelo segundo, ao invés de aguardar um segundo resultado para ser processado posteriormente. Desta maneira, >>= integra o sequenciamento de valores de tipo Maybe com o processamento de valores resultantes de computações sobre esse tipo. Em Haskell, o operador >>= é muitas vezes denominado “bind” (vincular), pois o segundo argumento é vinculado ao resultado do primeiro. Observe que >>= é idêntico a função apply definida anteriormente, a menos de que seus argumentos são “trocados”.

Usando o operador >>=, a função que avalia expressões aritméticas pode ser reescrita como:

eval (Val n)   = Just n
eval (Div x y) = eval x >>= (\n -> eval y >>=
                        (\m -> safediv n m))

A equação para a divisão pode ser lida da seguinte maneira: avalie x e chame o resultado desta avaliação de n, então avalie y e chame seu resultado de m, e finalmente combine estes dois resultados usando a função safediv.

Podemos generalizar a estrutura deste pequeno exemplo para expressões quaisquer que utilizam o operador >>=. Essas expressões possuem a seguinte estrutura:

     m1 >>= \x1 ->
     m2 >>= \x2 ->
         ...
     mn >>= \xn ->
         f x1 x2 ... xn

Traduzindo esta definição para português simples: Avalie cada uma das expressões m1, m2, …, mn e combine os resultados de cada uma delas aplicando a função f.

A definição de >>= garante que tal expressão somente retorna um valor de forma Just se nenhum mi na sequência retorna Nothing. Em outras palavras, não é necessário o programador se preocupar com eventuais falhas (representado no exemplo, por retornar um valor Nothing) em cada uma das expressões envolvidas, pois o operador >>= cuida desta manipulação de maneira simples.

Tais expressões são tão comuns em Haskell, que a linguagem possui uma notação especial permitindo que essas sejam escritas de uma forma mais legível:

do
    x1 <- m1
    x2 <- m2
    ...
    xn <- mn
    f x1 x2 ... xn

Utilizando esta notação, pode-se reescrever o avaliador de expressões de maneira bem simples e legível:

eval (Val n)   = Just n
eval (Div x y) = do
                    n <- eval x
                    m <- eval y
                    safediv n m

Mônadas em Haskell

O uso da notação do não é restrita a valores do tipo Maybe, a única restrição sobre essa notação é que ela deve somente ser utilizada em computações envolvendo tipos que constituem uma mônada. O conceito de mônada vem de um ramo da matemática chamado de teoria das categorias. Para a utilização de mônadas em Haskell não é necessário entender este conceito matemático. Na prática, uma mônada em Haskell, é um tipo m que possui duas funções:

return :: a -> m a

(>>=)  :: m a -> (a -> m b) -> m b

Por exemplo, se considerarmos que m  = Maybe, temos que os tipos de return e >>= são:

return :: a -> Maybe a

(>>=)  :: Maybe a -> (a -> Maybe b) -> Maybe b

Com estas duas funções, temos nossa primeira mônada.

Haskell suporta a definição de funções sobrecarregadas utilizando classes de tipos. Uma classe de tipo é uma coleção de tipos que possuem uma determinada interface de funções sobrecarregadas definidas sobre estes.

Por exemplo, a classe Eq de tipos que permitem o teste de igualdade, pode ser declarado da seguinte maneira:

class Eq a where
    (==) :: a -> a -> Bool
    (/=) :: a -> a -> Bool

    x /= y = not (x == y)

A definição declara que para um tipo “a” ser uma instância da classe Eq , ele deve suportar os operadores de teste de igualdade / desigualdade com os tipos especificados. Devido ao fato da classe possuir uma definição padrão para o operador de desigualdade (/=), é necessário apenas definir a igualdade para o tipo em questão. Como um exemplo, podemos definir uma instância para o tipo Bool:

instance Eq Bool where
    False == False = True
    True  == True  = True
     _     == _      = False

A noção de mônada pode ser representada utilizando a seguinte declaração de classe:

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

Isto é, uma mônada é um tipo “m” que implementa as funções return e >>= dos tipos especificados. A definição de uma instância para o tipo Maybe:


instance Monad Maybe where
     return x       =  Just x

     Nothing  >>= _ =  Nothing
     (Just x) >>= f =  f x

Agora que definimos esta instância para o tipo Maybe, podemos utilizar a notação do para computações envolvendo este tipo. Todo tipo que é instância da classe Monad, pode ser utilizado com a notação do.

A mônada de listas

A mônada de Maybe provê um simples modelo de computações que podem falhar, no sentido de que um valor de tipo Maybe é da forma Nothing, que pode ser pensado como uma falha, ou possui a forma Just x para algum x de tipo a, que pode ser entendido como um sucesso. A mônada de listas generaliza esta noção, permitindo múltiplos resultados no caso de sucesso.

Sendo mais preciso, um valor de tipo [a] ou é uma lista vazia [ ], que podemos ver como uma falha, ou possui a forma de uma lista não vazia [x_1, x_2, ..., x_n] para algum x_i de tipo a, que pode ser visto como o sucesso. De certa maneira, uma mônada de lista pode ser utilizada para modelar computações não determinísticas, onde mais de um resultado é produzido a cada passo. A definição de uma lista como sendo uma mônada é direta:

instance Monad [ ] where
    return x  =  [x]
    xs >>= f  =  concat (map f xs)

(Nota: Nesta definição, [ ] representa um tipo lista sem seu parâmetro a ). A função return simplesmente converte um valor qualquer em um resultado contendo este valor, enquanto >>= fornece uma maneira de sequenciar computações que podem retornar mais de um resultado: xs >>= f aplica a função f a cada um dos resultados da lista xs produzindo, assim, uma lista de listas de resultados que é posteriormente concatenada para formar uma única lista contendo todos os resultados.

Como exemplo da utilização da mônada de listas, uma função que retorna todas as maneiras de combinar pares de elementos de duas listas pode ser definida utilizando a notação do da seguinte maneira:

pairs     :: [a] -> [b] -> [(a,b)]
pairs xs ys =  do
                 x <- xs
                 y <- ys
                 return (x,y)

Isto é, considere cada possível valor x da lista xs, e cada valor y da lista ys, e retorne o par (x,y). Observe a definição da função pairs utilizando list comprehension:

pairs xs ys = [(x,y) | x <- xs, y <- ys]

Na verdade, list comprehensions e a notação do para listas são equivalentes. Ambas notações são maneiras diferentes de se utilizar o operador >>= para listas.

A mônada de estado

Agora consideremos o problema de implementar funções que manipulam algum tipo de estado, representado por um tipo cujos detalhes internos podemos, por agora, ignorar. Pode-se considerar que este tipo possui a seguinte forma:

type State = ...

A mais básica função sobre um estado é o que chamamos de “transformador de estado” (abreviado como ST , do inglês state transformer), que recebe como parâmetro o estado atual, e produz um estado possivelmente modificado e um resultado.

type ST a = State -> (a, State)

A figura a seguir ilustra a aplicação de tal função a um estado s, produzindo um novo estado s’ e um resultado v.

Transformador de estado

Um transformador de estados pode receber argumentos adicionais. Todavia, não é necessário alterar o tipo ST, porque este comportamento pode obtido por currying. Por exemplo, um transformador de estados que recebe um caractere (Char) e retorna um inteiro (Int) possui o tipo Char -> ST Int, que é uma abreviação para Char -> State -> (Int, State). Isto pode ser representado graficamente por:

Retornando às mônadas, é fácil observar que ST constitui uma mônada de simples definição:

 instance Monad ST where
    return x  =  \s -> (x,s)
    st >>= f  =  \s -> let (x,s') = st s in f x s'

Isto é, return converte um valor em um transformador de estado que apenas retorna aquele valor sem modificar o estado. Graficamente:

Visão diagramática da função return

Por sua vez, (>>=) provê uma maneira de sequenciar transformadores de estados: st >>= f aplica o tranformador de estado st a um estado inicial s, então aplica a função f ao resultado x para produzir um segundo transformador de estado (f x), que é então aplicado ao novo estado s’ para produzir o resultado final. Graficamente:

Sequenciando transformadores de estado

Perceba que return poderia ser definido como:

return x s = (x,s)

Todavia, a definição anterior é preferida por ocultar o parâmetro de estado s. Um pequeno detalhe sobre a instância para a mônada ST definida anteriormente: Haskell não permite a definição de instâncias para sinônimos de tipos. Portanto, podemos definir o tipo ST da seguinte forma alternativa (mas equivalente):

newtype ST a = ST { runST :: State -> (a, State) }

A definição da mônada ST pode ser feita da seguinte maneira:

instance Monad ST where
    return x   = ST (\s -> (x,s))
    st >>= f   = ST (\s -> let
                             (x,s') = runST st s
                           in runST (f x) s')

Mônada de estado: Um Exemplo

Como um simples exemplo de utilização de uma mônada de estado, vamos considerar a tarefa de rotular cada nó de uma árvore binária com um número inteiro que o identifica unicamente. Para isso, será necessário definir um tipo de dados para árvores binárias:

data Tree a = Leaf a | Node (Tree a) (Tree a)

Segue um pequeno exemplo de uma árvore:

tree :: Tree Char
tree =  Node (Node (Leaf 'a') (Leaf 'b')) (Leaf 'c')

Agora iremos considerar nosso problema original: de rotular cada nó com um número inteiro correspondente ao valor deste nó. Primeiramente, deve-se definir o tipo do estado a ser manipulado. Como o objetivo é adicionar um número inteiro para cada nó da árvore, toda vez que passarmos por um nó devemos “incrementar nosso” contador, que representa o estado a ser manipulado. Portanto, nada mais natural que definir o estado como sendo um número inteiro:


type State = Int

Considerando que o estado armazenado seja um número inteiro e que a cada nó visitado o estado deve ser atualizado com o sucessor deste número, temos que implementar um transformador de estado que retorna o estado atual como seu resultado e incrementa este número para formar o novo estado. Isto é:

fresh :: ST Int
fresh =  S (\n -> (n, n+1))

Usando esta função e as funções monádicas para ST fica fácil definir uma função que recebe uma árvore como argumento e retorna um transformador que produz a mesma árvore onde cada nó é rotulado com um inteiro:

mlabel :: Tree a -> ST (Tree (a,Int))
mlabel (Leaf x)   =  do
                       n <- fresh
                       return (Leaf (x,n))
mlabel (Node l r) =  do
                       l' <- mlabel l
                       r' <- mlabel r
                       return (Node l' r')

Observe que não é necessário que o programador se preocupe com a tarefa tediosa e propensa a erros de lidar com a criação de novos rótulos para cada componente da árvore, já que isso é diretamente manipulado pela mônada de estado!

Tendo este transformador de estado em mãos, podemos definir uma função que rotula uma árvore simplesmente aplicando o transformador tendo o inteiro 0 como estado inicial e descartando o estado final.

label  :: Tree a -> Tree (a,Int)
label t = fst (apply (mlabel t) 0)

A aplicação da função label à árvore tree resulta em:

Node (Node (Leaf ('a',0)) (Leaf ('b',1))) (Leaf ('c',2))

A mônada de I/O

Programas interativos em Haskell são escritos utilizando o tipo IO a que retorna um valor de tipo a, mas pode realizar alguma entrada / saída. A biblioteca Prelude possui diversas funções para construir valores de tipo IO:

return  :: a -> IO a
(>>=)   :: IO a -> (a -> IO b) -> IO b
getChar :: IO Char
putChar :: Char -> IO ()

Veja só… o tipo IO  possui as funções return  e (>>=), o que quer dizer que o tipo IO é uma mônada, e portanto, podemos utilizar a notação do para escrever programas interativos. Como exemplo, considere a seguinte função que lê uma sequência de caracteres a partir do teclado:

getLine :: IO String
getLine = do
            x <- getChar
            if x == '\n' then []
              else do
                    xs <- getLine
                    return (x:xs)

É interessante notar que a mônada de IO pode ser interpretada como um caso especial de uma mônada de estado, na qual o estado interno da mônada representa o estado de “todo o mundo”:

type World = ...
type IO a  = World -> (a,World)

Isto é, uma ação (um valor de tipo IO a) pode ser visto como uma função que recebe o estado atual do mundo como seu argumento, e produz um valor e este estado possivelmente modificado (refletindo possíveis resultados de entrada e saída executados pela ação). Internamente, o compilador GHC utiliza uma representação similar a esta para codificar valores de tipo IO.

Conclusão

Este post foi extenso, mas serviu apenas para “arranhar” o tópico sobre mônadas e programação funcional. Como o tema é deveras extenso, não é possível abordar todas as nuances deste. Recomendo os seguintes artigos, para leitores que desejam aprofundar seus conhecimentos:

  1. The Essence of Functional Programming – Philip Wadler
  2. Monadic Parsing Combinators – Graham Hutton

Além disso tem havido interesse em arrows  e funtores aplicativos que são generalizações de mônadas. Referências sobre estes temas são

  1. Generalizing monads to arrows – John Hughes
  2. Applicative Programming with Effects – Connor McBride.

Agda – Uma linguagem com tipos dependentes

março 14, 2011

Um problema recorrente em linguagem com suporte a arrays é a tentativa de acesso a uma posição inválida. Um pequeno exemplo deste inconveniente acontece neste simples algoritmo para busca sequencial em Java:

public int search(int [] vector, int key) {
     for(int i = 0; i <= vet.length; i++)
         if (vet[i] == key) return i;
     return -1;
}

É fácil ver que este código causará um ArrayIndexOutOfBoundsException, já que a variável que controla a condição de parada do loop é inicializada em zero e é testada se é menor ou igual ao número de elementos do arranjo. Em Java e C/C++ o intervalo de elementos em um array vai de zero ao número de elementos do arranjo menos um. Com isso, ao tentarmos acessar a n-ésima posição do array estaremos acessando uma área de memória inválida, causando a já acima citada exceção ou um possível segmentation fault ou outros erros mirabolantes em C/C++.

Idealmente erros como este deveriam ser capturados pelo compilador durante a verificação estática do programa no processo de compilação. Porém, verificar se o valor de indexação de um array está dentro dos limites deste é um problema indecidível, já que é equivalente ao problema da parada.

Então devemos conviver com estes tipos de erros esdrúxulos e ser mais atentos quando usamos arrays? Na verdade, isso não é necessário. Existem linguagens de programação que podem remediar esta situação utilizando os chamados tipos dependentes (dependent types) adicionando “mais informação” aos tipos de arranjos, permitindo assim, que o compilador capture estaticamente um acesso a uma posição inválida de um arranjo. Atualmente, existem diversas linguagens que dão suporte a tipos dependentes, estas são utilizadas principalmente como assistentes de provas.

Neste post, pretendo apresentar a linguagem Agda, uma linguagem funcional com suporte a tipos dependentes.

Tipos de dados em Agda.

Pessoas que já desenvolveram algum programa ou pelo menos conhecem a linguagem Haskell, não encontrarão dificuldades em aprender Agda, já que a sintaxe dessa linguagem é baseada na sintaxe de Haskell. Como um primeiro exemplo, considere a seguinte definição do tipo de dados Bool em Haskell (infelizmente o wordpress não fornece syntax highlighting para Haskell e Agda):

data Bool = True | False

A definição acima é usual. O tipo de dados Bool possui dois construtores, a saber: True e False. A mesma definição em Agda é:


data Bool : Set where
    true  : Bool
    false : Bool

Apesar de similares, as definições possuem algumas diferenças. Primeiramente, na definição em Agda, o tipo Bool é seguido por uma anotação de Sort. Podemos pensar em um Sort, como sendo um “tipo de tipos”. Anotar um tipo com o sort “Set” indica que este é um tipo. Na sequência, logo após a palavra reservada where, temos a especificação dos construtores de dados deste tipo. Note que estes construtores são também anotados, mas, com o tipo Bool.

Ao contrário de outras linguagens de programação, em Agda, todos os tipos de dados podem ser construídos a partir de princípios simples. Por exemplo, na linguagem o tipo de números naturais é definido na biblioteca padrão da linguagem como:

data Nat : Set where
   Z : Nat
   S : Nat -> Nat

Em Agda, números naturais são representados utilizando os axiomas de Peano, onde números naturais são representados por sucessivas aplicações da função sucessor ao número zero. A definição anterior apresenta o tipo de dados Nat que representa números naturais de acordo com a axiomática de Peano. O tipo Nat possui dois construtores: Z que representa o número natural zero e S, que representa a função sucessor. Para facilitar a utilização, os compiladores Agda reconhecem que 1 = S\,\,Z, isto é, a linguagem ofecere um suporte a definição de números formados algarismos arábicos convencionais. Internamente, o compilador realiza a conversão entre estes números e o tipo de dados Nat.

Funções em Agda

Por ser uma linguagem funcional, Agda permite a definição de funções sobre tipos de dados por meio de casamento de padrão. A seguinte função codifica a soma de dois números naturais:

_+_ : Nat -> Nat -> Nat
Z + m = m
(S n) + m = S (n + m)

A definição recursiva da soma de dois números naturais é direta: Caso o primeiro deles seja zero, o resultado da soma é o segundo. Caso o primeiro seja um número diferente de zero (isto é, um número da forma S\,\,n para algum n) o resultado da soma será o sucessor da soma de n com o segundo parâmetro m.

Tipos dependentes

A motivação apresentada no início deste post era evitar que operações de acesso a elementos de arranjos pudessem acessar posições inválidas desses arranjos. Para podermos contornar esta situação, é necessário que a linguagem permita combinar valores e tipos para definir novos tipos. Tipos dependentes são tipos que “dependem” de valores e não apenas de outros tipos como o caso de construtores de tipos em linguagens que suportam polimorfismo paramétrico. A definição a seguir apresenta um tipo de dados que representa vetores de um determinado tamanho:

data Vec (A : Set) : Nat -> Set where
      [ ] : Vec A Z
      _::_ : {n : Nat} -> A -> Vec A n -> Vec A (S n)

Esta declaração possui um número de coisas “interessantes”. Primeiramente, o tipo Vec não é um valor do
sort Set, mas sim uma família de tipos indexada por um valor de tipo Nat, isto é, Nat -> Set. Intuitivamente, o tipo Vec A n representa o tipo de vetores de valores de tipo A com exatamente n elementos. Este tipo é formado por dois construtores de dados:

  • [ ] :: Vec A Z, que representa um vetor com zero elementos de tipo A.
  • _::_ : {n : Nat} -> A -> Vec A n -> Vec A (S n), que representa a inserção de um elemento de tipo A em um vetor com n elementos, produzindo um vetor de n + 1 elementos.

Oberve que o tipo dos construtores captura invariantes sobre as funções que os definem. O construtor de lista vazia, codifica em seu tipo, o fato de que não possui nenhum elemento e o construtor _::_ captura o invariante de que após a inserção de um elemento em um vetor contendo n elementos este passa a possuir n + 1 elementos.

Com este tipo, é possível obter uma função “segura” que obtem o primeiro elemento de uma lista. Em Haskell, tal função pode causar problemas, pois sua implementação na biblioteca Prelude é:

head :: [a] -> a
head [ ] = error "Prelude.head: empty list."
head (x:_) = x

Se a função head for aplicada a uma lista vazia, ocorrerá a interrupção da execução do programa devido a chamada da função error. Em Agda, tal situação é contornada, evitando em tempo de compilação que uma função similar a head seja aplicada a um vetor vazio. O código desta função é apresentado a seguir:

vhead : {A : Set} {n : Nat} -> Vec A (S n) -> A
vhead (x :: xs) = x

Neste exemplo, pode-se observar que a aplicação da função vhead a um vetor vazio não é possível pois esta função exige como parâmetro um vetor que possua pelo menos um elemento (fato representado pelo tipo do parâmetro: Vec A (S n)). Totalmente demais!

Representando provas

O sistema de tipos de Agda é suficientemente expressivo para permitir que expressemos proposições lógicas arbitrárias como tipo e seus valores como provas. Como exemplo, podemos definir os seguintes tipos que representam, respectivamente, proposições verdadeiras e falsas:

data True : Set where
     trivial : True

data False : Set where

No trecho de código acima, podemos observar que uma proposição verdadeira (representada pelo tipo True) possui uma prova trivial (representada pelo construtor trivial). Por sua vez, uma proposição falsa, representada pelo tipo False não possui prova, já que, consideramos como falso algo que não possui prova de que é verdadeira (considerando a lógica intuicionista).

Com isso, podemos definir uma função que representa proposições decidíveis (isto é, que são verdadeiras ou falsas):

isTrue : Bool -> Set
isTrue true = True
isTrue false = False

Com isso temos que, isTrue b é o tipo de provas de que b é igual a true. Com isto, podemos implementar uma função segura para obter o n-ésimo elemento de uma lista. Para isso, primeiramente devemos definir um tipo que expressa quando um número natural n é menor que outro número natural m. Este tipo é apresentado a seguir:

_<_ : Nat -> Nat -> Bool
_  < zero = false
zero  < m = true
(S n) < (S m) = n < m 

Além disso, vamos precisar de uma função que calcula o número de elementos de uma lista. A implementação desta função é trivial:

 length : {A : Set} -> List A -> Nat
length [ ] = Z
length (x :: xs) = S (length xs)

Agora possuímos todo o arsenal necessário para codificar uma função segura para obter o n-ésimo elemento em uma lista. Podemos conjecturar que a função de obter o n-ésimo elemento de uma lista é segura se e somente se n < length xs. Tal fato pode ser codificado pelo tipo:

lookup : {A : Set}(xs : List A)(n : Nat) ->
           isTrue (n < length xs) -> A

onde o parâmetro isTrue (n < length xs) representa uma prova da proposição n < length xs. O código completo da função lookup é apresentado a seguir:

lookup : {A : Set}(xs : List A)(n : Nat) ->
             isTrue (n < length xs) -> A
lookup [] n  ()
lookup (x :: xs) zero p = x
lookup (x :: xs) (suc n) p = lookup xs n p

Temos as seguintes possibilidades para esta definição: se n é maior que o tamanho da lista xs então não é possível obter uma prova de isTrue (n < length xs). Na definição de lookup, a primeira equação representa a situação de quando não é possível obter uma prova de n < length xs. A notação () representa uma padrão absurdo permitindo assim, que o lado direito da equação seja omitido. As duas equações seguintes lidam com a possibilidade de ser possível obter uma prova para n < length xs.

Conclusão

Neste post foi apresentado uma pequena introdução a linguagem Agda. Tipos dependentes apresentam uma possibilidade interresante para o desenvolvimento por permitiram a codificação de invariantes que podem ser verificados estaticamente pelo compilador.

Este post foi inspirado no artigo Dependently Typed Programming in Agda por Ulf Norell. Maiores informações sobre Agda, downloado do compilador da linguagem podem ser encontrados no site http://wiki.portal.chalmers.se/agda/pmwiki.php.

Consequências Computacionais da lei do Terceiro Excluído

março 6, 2011

Recentemente em meu doutorado tenho dedicado grande esforço em compreender e utilizar a lógica intuicionista. Sendo extremamente simplista, a lógica intuicionista é um sistema formal que difere da lógica clássica em apenas um ponto: a lei do terceiro excluído e eliminação da dupla negação não são axiomas.

A lei do terceiro excluído é de simples compreensão: Toda proposição lógica deve ser verdadeiro ou falsa. Mais formalmente:

\forall p . P \lor \neg P

Aparentemente tal afirmação ingênua (e por sinal bastante lógica!) não possui nenhum tipo de complicação inerente ou mesmo qualquer relação com os fundamentos da computação. De acordo com o isomorfismo de Curry-Howard, caso sejamos capazes de construir uma prova para uma proposição qualquer, é possível extrair desta prova um programa funcional cujo tipo é isomórfico à proposição provada. Sendo assim, assuma o seguinte predicado halt(p) que é verdadeiro se um determinado programa p pára e falso caso contrário. Considere, então, agora a seguinte proposição:

\forall p. halt(p) \lor \neg halt(p)

Se o isomorfismo de curry howard estiver correto, podemos construir uma prova para esta afirmativa e esta poderia ser utilizada para obtermos um algoritmo que decide para um programa arbitrário p se este pára ou não. É fato bem conhecido, que o chamado problema da parada é indecidível e portanto não é possível obter tal programa. Então, qual o problema? O isomorfismo de Curry Howard está incorreto? O grande “pulo-do-gato” é que o isomorfismo de Curry-Howard é restrito à lógica intuicionista, que requer uma prova para afirmar que uma determinada proposição é verdadeira ou falsa.

É evidente que a adoção da lei do terceiro excluído é problemática em termos computacionais, já que esta implicaria na solução do problema da parada.

The Expression Problem

abril 25, 2010

Philip Wadler apresentou em [1] o chamado “The Expression Problem” que pode ser enunciado da seguinte maneira:

O objetivo é definir um tipo de dados por casos, onde pode-se adicionar novos casos ao tipo de dados e novas funções sobre este tipo, sem recompilar código existente e garantindo que erros de tipo sejam sempre encontrados.

Além de enunciá-lo, Wadler apresentou uma solução para este em GJ (antiga versão experimental de Java com suporte a polimorfismo paramétrico).

Algumas soluções já foram propostas e publicadas para este problema, como por exemplo em [2]. Porém, a solução mais elegante, que conheço, para este problema é a apresentada em [3]. Swierstra apresenta como estender tipos de dados com novos casos (construtores de dados) e novas funcionalidades. Para isso, cada tipo de dados é representado com um coproduto dos diferentes construtores de dados que formam este tipo e funcionalidades, por sua vez, são implementadas utilizando funções sobrecarregadas (classes de tipos e instâncias em Haskell).

Como o problema de estender tipos de dados e funcionalidades sem recompilar código existente é recorrente no desenvolvimento de software, é útil saber como pode-se obter uma solução elegante para isto utilizando Haskell. A solução utiliza algumas extensões presentes no compilador GHC, são elas:

* TypeOperators
* MultiParamTypeClasses
* FlexibleInstances
* FlexibleContexts
* IncoherentInstances
* UndecidableInstances

A seguir apresento um pequeno avaliador de expressões aritméticas onde pode-se estender tanto a sintaxe das expressões avaliadas quanto o conjunto de operações aplicadas sobre estas expressões.

1 – Avaliando Expressões Aritméticas.

1.1 – Definindo Expressões

O primeiro passo é representar o tipo de expressões de maneira que este possa ser parametrizado pelos construtores de dados que podem ser acrescentados a este. Para isso, representaremos uma expressão aritmética pelo tipo Expr, apresentado a seguir:

data Expr f = In { out :: f (Expr f) }

Observe que o tipo de dados Expr, é parametrizado por uma variável de tipo de kind \star\rightarrow\star. A função principal do tipo Expr é ser um operador de ponto fixo dos construtores que parametrizarão este tipo de dados. Até o presente momento nenhum construtor de dados que represente algum tipo de expressão aritmética foi definido. O único construtor de dados definido para o tipo Expr é:

In :: f (Expr f) \rightarrow Expr f

Que não representa nenhuma expressão aritmética. Então como definimos expressões que envolvam adição, multiplicação, subtração, etc.? Para alcançar os objetivos de definir novos construtores de dados sem a necessidade de alterar código existente, temos que representar construtores de dados como novos tipos de dados que representam os diferentes construtores para expressões aritméticas. Como exemplo, considere as seguintes declarações que representam respectivamente valores inteiros e a soma de duas expressões quaisquer:

data Val e = Val Int

data Add e = Add e e

Com isso, temos que uma expressão formada exclusivamente por valores inteiros pode possuir o seguinte tipo:

type IntExpr = Expr Val

Expressões que o tipo IntExpr são da forma In (Val x) para qualquer número inteiro x. O tipo de dados Val não utiliza em seu construtor seu parâmetro e, uma vez que, valores inteiros são expressões que não possuem um componente recursivo (isto é, não possuem outras expressões como descendentes em uma árvore).

Por sua vez, o tipo Add utiliza seu parâmetro de tipo para representar que a operação de adição recebe como argumento duas expressões de tipo e.

Tipos de dados que representam constantes inteiras ou adições não são interessantes isoladamente. Para combinar estes novos tipos, devemos introduzir um tipo de dados que representa um coproduto de construtores de tipos (similar ao tipo Either que é um coproduto que opera sobre valores). A definição seguinte, mostra como declarar um tipo de dados para o coproduto de dois construtores de tipos que associa à direita:

data (f :+: g) e = Inl (f e) | Inr (g e)

infixr 6 :+:

Expressões que possuem o tipo Expr (Val :+: Add) são ou um valor inteiro ou a soma de duas outras expressões. Porém, esta técnica torna a tarefa de escrever uma expressão que representa a soma 33 + 77 extremamente tediosa, como pode ser observado pelo trecho de código que representa a soma anterior:

dummyExpr :: Expr (Val :+: Add)

dummyExpr = In (Inr (Add (In (In (Val 33))) (In (In (Val 77)))))

Evidentemente não é isso que desejamos. Nosso próximo passo será criar uma maneira simples para definir expressões.

1.2 – Definindo Expressões mais Facilmente

Vimos que a definição de expressões utilizando coprodutos é extremamente longa, mesmo para expressões simples. Para contornar esta situação, precisamos definir uma maneira para injetar automaticamente valores em coprodutos. Esta tarefa será realizada por funções que farão o papel de construtores de dados. No nosso exemplo, teríamos uma função para a criação de valores e uma para a adição:

val :: Int \rightarrow Expr Val

val = In . Val

infixl 6 <+>

(<+>) :: Expr Add \rightarrow Expr Add \rightarrow Expr Add

x <+> y = In (Add x y)

Com essas definições podemos tentar reescrever a soma 33 + 77:

val 33 <+> val 77

O que aparentemente está perfeito. Porém, ao tentarmos definir tal expressão obtemos um erro de tipo. Para entender o porquê, basta verificar o tipo das funções utilizadas:

  • val :: Int \rightarrow Expr Val
  • (<+>) :: Expr Add \rightarrow Expr Add \rightarrow Expr Add

Veja que a função <+> espera como argumentos duas expressões de tipo Expr Add, isto é, expressões que possuam sub-expressões formadas apenas por adições. Para solucionar este problema, [3] propõe a generalização dos tipos destas definições para:

(<+>) :: (Add :<: f ) \Rightarrow Expr f \rightarrow Expr f \rightarrow Expr f

val :: (Val :<: f ) \Rightarrow Int \rightarrow Expr f

Onde a restrição de tipo Val :<: f representa que podemos injetar um valor em um coproduto f. Para permitir que estas “injeções” (não consegui pensar numa tradução melhor para injections) sejam feitas automaticamente, definiremos uma classe de tipos e algumas instâncias que realizarão este trabalho. A definição destas é apresentada abaixo:

class (Functor sub, Functor sup) \Rightarrow (:<:) sub sup where
+++ inj :: sub a \rightarrow sup a

instance (Functor f, Functor g) \Rightarrow (:<:) f f where
+++ inj = id

instance (Functor f, Functor g) \Rightarrow (:<:) f (f :+: g) where
+++ inj = Inl

instance (Functor f, Functor g,
++++++Functor h, (:<:) f g)
++++++ \Rightarrow (:<:) f (h :+: g) where
++++++++++ inj = Inr . inj

A classe de tipos (:<:) sub sup possui somente uma função: inj :: sub a \rightarrow sup a, que injeta um valor de tipo sub a em um coproduto de tipo sup a. A primeira instância mostra que a relação entre construtores de tipos definida pela classe (:<:) é reflexiva. A segunda explica como injetar um valor de tipo f a em um valor de tipo (f :+: g) a. A última instância mostra que se podemos injetar um valor de tipo f a em um valor de tipo g a então podemos injetá-lo em um valor de tipo (h :+: g) a, independente do construtor de tipos h envolvido.

Com estas instâncias em mãos, podemos definir as seguintes funções que farão o papel de construtores de dados para constantes e adição.

inject :: (g :<: f) \Rightarrow g (Expr f) \rightarrow Expr f

inject = In . inj

val :: (Val :<: f ) \Rightarrow Int \rightarrow Expr f

val = inject . Val

(<+>) :: (Add :<: f ) \Rightarrow Expr f \rightarrowExpr f \rightarrow Expr f

x <+> y = inject (Add x y)

Como o leitor atento deve ter percebido, os tipos Add, Val e (:+:) precisam possuir instâncias da classe Functor. Essas instâncias são auto-explicativas:

instance Functor Val where
+++ fmap f (Val x) = f x

instance Functor Add where
+++ fmap f (Add e1 e2) = Add (f e1) (f e2)

instance (Functor f, Functor g) \Rightarrow Functor (f :+: g) where
+++ fmap f (Inl e1) = Inl (fmap f e1)
+++ fmap f (Inr e2) = Inr (fmap f e2)

Agora podemos escrever expressões mais facilmente:

x :: Expr (Add :+: Val)

x = val 33 <+> val 77

Note a presença da anotação de tipo para o valor x. Somente com esta anotação o compilador será capaz de identificar qual instância será executada para realizar a injeção de valores corretamente.

1.3 – Definindo Operações sobre Expressões

Até agora escrevemos uma grande quantidade de código somente para definir expressões mais facilmente usando coprodutos. Mas nada foi dito sobre como codificar operações sobre estas expressões. Antes de definir uma primeira operação, vamos definir um fold sobre uma expressão de tipo Expr f:

foldExpr :: Functor f \Rightarrow (f a \rightarrow a) \rightarrow Expr f \rightarrow a

foldExpr f = f . fmap (foldExpr f) . out

Um fold é um operador que representa o caminhamento recursivo pela estrutura de um tipo. Folds são parametrizados por uma álgebra, que determina como valores produzidos por diferentes construtores de dados são utilizados para formar o resultado final em cada passo do caminhamento recursivo por toda a estrutura da expressão[4][5]. Como uma álgebra define como é feito o processamento em cada nível de um valor, devemos implementar operações sobre nossos tipos como álgebras, isto é, todas as operações devem ter um tipo que é instância de f a \rightarrow a.

Como um primeiro exemplo de operação, considere a seguinte álgebra para avaliação de expressões:

class Functor f \Rightarrow Eval f where

+++evalAlgebra :: f Int \rightarrow Int

e as suas instâncias para os tipos Val e Add:

instance Eval Val where

+++evalAlgebra (Val x) = x

instance Eval Add where

+++evalAlgebra (Add e1 e2) = x + y

Observe que a implementação das álgebras para valores inteiros e adição é idêntica a uma implementação tradicional de um avaliador de expressões aritméticas. Porém, como nossas expressões são formadas pelo coproduto de tipos, temos que definir esta mesma álgebra para coprodutos:

instance (Eval f, Eval g) \Rightarrow Eval (f :+: g) where

+++evalAlgebra (Inl x) = evalAlgebra x

+++evalAlgebra (Inr x) = evalAlgebra x

Agora que possuímos todo o armamento necessário, podemos finalmente implementar a avaliação de expressões, usando o fold e a álgebra:

eval :: Eval f \Rightarrow Expr f \rightarrow Int

eval = foldExpr evalAlgebra

Usando a função eval podemos avaliar a soma definida anteriormente:

Main\rangle eval x

110

O leitor deve estar se perguntando: Qual a vantagem de tanta complicação para avaliar expressões aritméticas? Até o presente momento, codificamos uma grande quantidade de código para implementar um simples avaliador de expressões aritméticas que poderia ter sido implementado da seguinte maneira:

data Expr = Val Int | Add Expr Expr

eval :: Expr \rightarrow Int

eval (Val x) = x

eval(Add e1 e2) = eval e1 + eval e2

Mas nosso trabalho será recompensado pela extensibilidade de nosso código, que permitirá a inclusão de novas operações à nossa linguagem de expressões sem alterar nenhuma linha de código.

1.4 – Estendendo o Avaliador de Expressões

Suponha que desejamos que nosso avaliador de expressões também seja capaz de realizar subtração, multiplicação e divisão. Como podemos fazer isso? Primeiramente, devemos definir novos tipos de dados e suas correspondentes instâncias da classe Functor:

data Mult e = Mult e e

instance Functor Mult where

+++fmap f (Mult e1 e2) = Mult (f e1) (f e2)

data Sub e = Sub e e

instance Functor Sub where

+++fmap f (Sub e1 e2) = Sub (f e1) (f e2)

data Div e = Div e e

instance Functor Div where

+++fmap f (Div e1 e2) = Div (f e1) (f e2)

Agora basta definir, para cada nova operação, a álgebra que fará a avaliação deste tipo de expressão e uma função que será utilizada para construir valores deste tipo:

instance Eval Mult where
+++evalAlgebra(Mult e1 e2) = e1 * e2

infixl <*> 7

(<*>) :: (Mult :<: f ) \Rightarrow Expr f \rightarrow Expr f \rightarrow Expr f
e1 <*> e2 = inject (Mult e1 e2)

O código da álgebra de avaliação e da função para construir valores para subtração e divisão é tão simples e direto quanto o da multiplicação. Veja que a inclusão de uma nova operação em nossa linguagem não exigiu que alterássemos nada na implementação anterior! Nosso trabalho está começando a dar resultados…

Agora que já foi apresentado como estender a sintaxe de nossa linguagem de expressões aritméticas, veremos como introduzir uma nova operação sobre esta linguagem. Considere agora a tarefa de realizar o pretty-printting de uma expressão. A classe de tipos Render destina-se a esta tarefa:

class Render f where

+++render :: Render g \Rightarrow f (Expr f) \rightarrow String

Supondo a existência de instâncias para cada um dos tipos de expressões que já definimos, podemos implementar uma função para o pretty-printting de expressões como:

pretty :: Render f \Rightarrow Expr f \rightarrow String

pretty = render . out

A implementação das instâncias da classe Render são diretas:

instance Render Val where

+++render (Val x) = show x

instance Render Add where

+++render (Add x y) = “(” ++ pretty x ++ ” + ” ++ pretty y ++ “)”

instance Render Mult where

+++render (Mult x y) = “(” ++ pretty x ++ ” * ” ++ pretty y ++ “)”

instance (Render f, Render g ) \Rightarrow Render (f :+: g ) where

+++render (Inl x) = render x

+++render (Inr x) = render x

Com isso, podemos realizar o pretty-printting de expressões:

Main\rangle pretty x

“(33 + 77)”

Com isso, podemos observar como estender código existente, sem modificá-lo, com novas funcionalidades e construtores de dados. Data Types a la Carte, constitui um exemplo interessante de como o sistema de tipos de Haskell é expressivo e pode ser utilizado para produzir software extensível.

Referências
1 – Wadler, Philip (1999). The expression problem. http://www.daimi.au.dk/~madst/tool/papers/expression.txt

2 – Blume, Mathias; Acar, Umut A.; Chae, Wonseok (2006). Extensible programming with first class cases. Proceedings of ICFP 2006.

3 – Swierstra, Wouter (2008). Data Types a la carte. Journal of Functional Programming – 18.

4 – Hutton, Graham (1993). A tutorial on the universality and expressiveness of fold. Journal of Functional Programming.

5 – Lammel, Ralf; Visser, Joost; Kort Jan. Dealing with Large Bananas.