Tipos algébricos e recursão

Uma árvore binária pode estar vazia ou conter um valor e duas subárvores. Uma declaração data representa estas alternativas com construtores. Os padrões das funções desmontam cada alternativa e a recursão segue as subárvores. A página começa pela ausência como valor, define árvores e tipos, e termina com provas, substituição e conversão entre tipos recursivos.

Ausência como valor

Uma média sobre uma lista vazia não tem valor. Maybe a representa essa ausência com Nothing ou a presença com Just x:

segura :: Double -> Double -> Maybe Double
segura _ 0 = Nothing
segura x y = Just (x / y)

segura 5 0 dá Nothing. segura 5 2 dá Just 2.5. Quem recebe um Maybe tem de tratar os dois construtores com padrões ou case. A média que pode faltar mostra o mesmo contrato numa função sobre listas.

data e padrões

Uma árvore binária ou está vazia ou é um nó com um valor e duas subárvores. A definição é quase essa frase:

data Arvore a = Vazia | No a (Arvore a) (Arvore a)

Vazia é um construtor sem argumentos e No guarda um valor e duas árvores. Funções sobre a árvore têm uma equação por construtor:

emOrdem :: Arvore a -> [a]
emOrdem Vazia = []
emOrdem (No x esq dir) = emOrdem esq ++ [x] ++ emOrdem dir

O padrão (No x esq dir) desmonta o nó e dá nome às peças. A travessia em ordem lista a esquerda, depois o valor, depois a direita. O caso base Vazia devolve a lista vazia, e é ele que termina a recursão, como o [] nas listas da primeira página.

Pesquisa em árvores binárias

Nesta árvore de pesquisa, todos os valores da subárvore esquerda são menores que o valor do nó; todos os da direita são maiores ou iguais. A condição vale em cada nó, não apenas entre pais e filhos. inserir mantém esta invariância e procura usa-a para excluir uma subárvore:

inserir :: Ord a => a -> Arvore a -> Arvore a
inserir x Vazia = No x Vazia Vazia
inserir x (No y esq dir)
  | x < y     = No y (inserir x esq) dir
  | otherwise = No y esq (inserir x dir)

procura :: Ord a => a -> Arvore a -> Bool
procura _ Vazia = False
procura x (No y esq dir)
  | x == y    = True
  | x < y     = procura x esq
  | otherwise = procura x dir

Constrói a árvore inserindo 3, 1, 4, 1, 5 por ordem em Vazia: o 3 abre a raiz, o 1 vai para a esquerda e o 4 para a direita; o segundo 1 é igual ao primeiro, por isso cai no otherwise e vai para a direita dele, e o 5 vai para a direita do 4.

A travessia em ordem devolve [1,1,3,4,5], pois a invariância garante saída ordenada mesmo com o duplicado. A procura segue a mesma invariância: procura 4 compara com 3, desce à direita e encontra 4; procura 2 desce à esquerda de 3, compara com o primeiro 1, desce à sua direita, compara com o segundo 1 e chega a Vazia, dando False. Cada comparação escolhe uma subárvore, por isso o número de comparações depende da altura da árvore¹.

data Arvore a = Vazia | No a (Arvore a) (Arvore a)

emOrdem :: Arvore a -> [a]
emOrdem Vazia = []
emOrdem (No x esq dir) = emOrdem esq ++ [x] ++ emOrdem dir

inserir :: Ord a => a -> Arvore a -> Arvore a
inserir x Vazia = No x Vazia Vazia
inserir x (No y esq dir)
  | x < y     = No y (inserir x esq) dir
  | otherwise = No y esq (inserir x dir)

procura :: Ord a => a -> Arvore a -> Bool
procura _ Vazia = False
procura x (No y esq dir)
  | x == y    = True
  | x < y     = procura x esq
  | otherwise = procura x dir

arv :: Arvore Int
arv = foldl (flip inserir) Vazia [3,1,4,1,5]

main :: IO ()
main = do
  print (emOrdem arv)
  print (procura 4 arv)
  print (procura 2 arv)

Quando a resposta pode faltar

A média ingénua das aprovações dividia por zero na lista vazia. O contrato que declara “valor ou ausência” é o mesmo Maybe da abertura:

mediaSegura :: [Double] -> Maybe Double
mediaSegura [] = Nothing
mediaSegura xs = Just (sum xs / fromIntegral (length xs))

Nothing é a ausência e Just embrulha o valor presente. O compilador pode avisar se falta um caso, mas ainda permite funções parciais; usar Maybe não obriga, por si só, a esse tratamento.

Construtores, sinónimos e recursão estrutural

type Ponto = (Double,Double) dá outro nome a um tipo existente. data Forma = Circulo Double | Retangulo Double Double cria um tipo novo com duas alternativas. Uma função area :: Forma -> Double precisa de considerar cada construtor: area (Circulo r) = pi*r*r e area (Retangulo a b) = a*b. A validade de dimensões positivas continua a ser uma condição separada.

O nome do tipo aparece nas assinaturas; o nome do construtor aparece nos valores e padrões. Em data Arvore a = Vazia | No a (Arvore a) (Arvore a), No tem tipo a -> Arvore a -> Arvore a -> Arvore a. A função construtora também pode ser parcialmente aplicada.

O esquema de recursão segue os componentes recursivos: para contar nós, o caso vazio dá zero e o nó dá 1 + tamanho esq + tamanho dir; para a altura, com vazio de altura zero, o nó dá 1 + max (altura esq) (altura dir). Numa folha, as duas subárvores vazias têm altura zero, dando altura um; indica a convenção, pois outra definição pode dar altura menos um à árvore vazia.

Uma árvore de expressões

data Expr = Valor Integer | Soma Expr Expr | Produto Expr Expr
  deriving (Eq, Show)

avaliar :: Expr -> Integer
avaliar (Valor n) = n
avaliar (Soma a b) = avaliar a + avaliar b
avaliar (Produto a b) = avaliar a * avaliar b

Soma (Valor 2) (Produto (Valor 3) (Valor 4)) representa 2+3*4. Avaliamos as folhas para 2, 3, 4, o produto para 12 e a soma para 14, porque a precedência já está na estrutura; avaliar não decide que operador tem prioridade.

deriving (Eq,Show) pede ao compilador implementações baseadas nos construtores e campos; num tipo parametrizado, comparar duas Arvore a requer também Eq a. Either erro valor é outro tipo algébrico que permite explicar por que o cálculo falhou.

Justificar uma lei por indução

Para provar length (map f xs) = length xs, considera listas finitas com comprimento representável em Int e os valores necessários à avaliação definidos. Usamos as equações de map e length.

Caso vazio: map f [] = [], por isso os dois comprimentos são 0.

Passo recursivo: supõe que a igualdade vale para a cauda xs. Então:

length (map f (x:xs))
= length (f x : map f xs)       pela equação de map
= 1 + length (map f xs)        pela equação de length
= 1 + length xs                pela hipótese sobre xs
= length (x:xs)                pela equação de length

A hipótese aplica-se à cauda menor, sem assumir a igualdade para a lista inteira em prova; length não precisa de avaliar f x, apenas de contar a célula construída.

Uma propriedade testada em exemplos reforça a confiança, mas não substitui esta prova para todas as listas finitas. A afirmação sobre length não pode ser avaliada numa lista infinita.

Substituir variáveis conservando a expressão

Avaliar uma expressão e construir outra expressão são tarefas diferentes. Nesta variante, acrescentamos folhas com nomes de variáveis:

data ExprVar = Const Integer | Var String
             | Add ExprVar ExprVar | Mult ExprVar ExprVar
  deriving (Eq, Show)

Um ambiente [(String,Integer)] liga nomes a valores. Substituir com [("x",4)] em Mult (Var "x") (Add (Var "z") (Const 2)) troca apenas a folha de x:

A resposta é Mult (Const 4) (Add (Var "z") (Const 2)). Não calculamos o produto nem inventamos zero para a variável ausente. lookup devolve Maybe Integer; Nothing conserva a variável e Just n constrói uma constante. Se o ambiente tiver um nome repetido, lookup usa a primeira ocorrência; decide esta política antes de escrever o resultado.

Converter uma árvore para outro tipo

Uma árvore binária não vazia pode ter folhas com valores ou ramos com dois filhos e um valor. Uma árvore rosa guarda uma lista de filhos:

data Bin a = Folha a | Ramo (Bin a) a (Bin a)
data Rosa a = Rosa a [Rosa a]

paraRosa :: Bin a -> Rosa a
paraRosa (Folha x) = Rosa x []
paraRosa (Ramo e x d) = Rosa x [paraRosa e, paraRosa d]

A folha torna-se um nó sem filhos. O ramo conserva o valor e coloca as duas conversões na ordem esquerda, direita. Não é uma travessia que achata a árvore: cada ramo continua a guardar os seus filhos. O tipo não exige Ord, Eq nem Num, porque a conversão não compara nem calcula valores.

data ExprVar = Const Integer | Var String
             | Add ExprVar ExprVar | Mult ExprVar ExprVar
  deriving (Eq, Show)

subst :: [(String,Integer)] -> ExprVar -> ExprVar
subst _ (Const n) = Const n
subst env (Var x) = case lookup x env of
  Nothing -> Var x
  Just n -> Const n
subst env (Add a b) = Add (subst env a) (subst env b)
subst env (Mult a b) = Mult (subst env a) (subst env b)

data Bin a = Folha a | Ramo (Bin a) a (Bin a)
  deriving (Eq, Show)
data Rosa a = Rosa a [Rosa a]
  deriving (Eq, Show)

paraRosa :: Bin a -> Rosa a
paraRosa (Folha x) = Rosa x []
paraRosa (Ramo e x d) = Rosa x [paraRosa e, paraRosa d]

main :: IO ()
main = do
  print (subst [("x",4)] (Mult (Var "x") (Add (Var "z") (Const 2))))
  print (subst [("x",4),("x",9)] (Var "x"))
  print (paraRosa (Ramo (Folha 'a') 'b' (Ramo (Folha 'c') 'd' (Folha 'e'))))

Nos dois algoritmos, cada chamada recursiva recebe uma subexpressão ou uma subárvore própria. Essa é a medida de progresso em entradas finitas. Para a substituição, com m entradas no ambiente e n nós na expressão, procurar cada variável com lookup pode exigir ordem n*m comparações no pior caso; a conversão visita cada nó uma vez.