Tipos algébricos e recursão

Tipos, construtores e padrões

• type Ponto = (Double,Double) é um sinónimo. data Dia = Seg | Ter cria um tipo novo com alternativas próprias.
• O nome do tipo aparece nas assinaturas; os construtores aparecem nos valores e nos padrões.
• Maybe a distingue Nothing de Just x: a ausência passa a ser um caso a tratar, não um erro escondido.
• deriving (Eq,Show) gera implementações a partir dos campos. Num tipo parametrizado, comparar exige igualdade dos elementos.
• Either erro valor permite ainda explicar por que o cálculo falhou.

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

Cada equação desmonta um construtor; a recursão segue os componentes menores. Como nas listas, o caso vazio termina a recursão.

Árvores de pesquisa

• Invariância: a esquerda tem valores menores que o nó, a direita maiores ou iguais. A condição vale em cada nó.
• inserir conserva a invariância; procura usa-a para excluir uma subárvore por comparação.
• A travessia em ordem de uma árvore de pesquisa devolve os valores ordenados, mesmo com duplicados.
• O custo segue a altura, não log n por decreto: numa árvore degenerada degrada-se para linear. inserir desta lição não equilibra.
• Indica a convenção de altura: aqui a árvore vazia tem altura zero e uma folha tem altura um.

Provar e transformar

Para provar length (map f xs) = length xs em listas finitas, usa indução: o caso vazio por cálculo direto, o passo aplicando a hipótese à cauda. Testar exemplos reforça a confiança; não substitui a prova.

• Substituir variáveis conserva a expressão: lookup decide por folha. Nothing conserva a variável; Just n constrói a constante. Nunca inventes zero para a variável ausente.
• Com nomes repetidos no ambiente, lookup usa a primeira ocorrência: decide essa política antes de escrever o resultado.
• Para converter tipos recursivos, transforma cada componente e conserva a ordem. Folha x vira Rosa x []; Ramo e x d vira Rosa x [conversao e, conversao d].
• Cada chamada recursiva recebe uma subexpressão ou subárvore própria: essa é a medida de progresso em entradas finitas.

Recursão estrutural e contratos.