6.6. Construindo Novos Tipos de Dados
O mesmo esquema constrói tipos mais ricos. Uma árvore binária é uma leaf ou uma branch carregando um valor e duas subárvores, e as funções sobre ela recorrem sobre as subárvores. A seção define size, height e mirror e enuncia as suas leis, provando apenas as instâncias fechadas por computação; as leis gerais são da Aula 7, pois precisam de indução.
namespace Func
inductive Tree (α : Type) where
| leaf
| branch (l : Tree α) (x : α) (r : Tree α)
def treeSize {α : Type} : Tree α → ℕ
| .leaf => 0
| .branch l _ r => treeSize l + 1 + treeSize r
def height {α : Type} : Tree α → ℕ
| .leaf => 0
| .branch l _ r => max (height l) (height r) + 1
def mirror {α : Type} : Tree α → Tree α
| .leaf => .leaf
| .branch l x r => .branch (mirror r) x (mirror l)
end Func
O recursor de Tree mostra o esquema geral sobre um tipo novo. Ele toma um valor para o caso leaf e, para o caso branch, uma função que recebe as duas subárvores, o valor armazenado e os resultados recursivos sobre as duas subárvores, que se tornam as hipóteses de indução de uma prova por indução.
namespace Func
#check @Tree.rec
end Func
As leis gerais que esta seção enuncia e a Aula 7 prova são mirror (mirror t) = t, treeSize (mirror t) = treeSize t e a lei de contagem que relaciona as folhas e as ramificações de uma árvore. Cada uma precisa de indução, então esta seção prova apenas as suas instâncias fechadas.
6.6.1. Exemplos
Os exemplos abaixo constroem uma árvore, computam com ela e leem os outros tipos de dados que o esquema produz.
Example 1. Uma árvore pequena com um valor na raiz e um na sua subárvore esquerda.
namespace Func
def t1 : Tree ℕ :=
.branch (.branch .leaf 1 .leaf) 2 .leaf
end Func
Example 2. size conta as ramificações, recorrendo sobre as duas subárvores.
namespace Func
#eval treeSize t1
end Func
Example 3. height toma a maior das duas alturas de subárvore e soma um.
namespace Func
#eval height t1
end Func
Example 4. mirror troca as duas subárvores em cada ramificação, e esta lei de construtor vale para toda árvore por computação, sem indução.
namespace Func
example {α : Type} (l : Tree α) (x : α) (r : Tree α) :
mirror (.branch l x r)
= .branch (mirror r) x (mirror l) := rfl
end Func
A lei do duplo espelhamento mirror (mirror t) = t, para toda árvore, é diferente, pois precisa de indução, e é um exemplo resolvido da Aula 7.
Example 5. Espelhar uma folha nada muda.
namespace Func
example : mirror (Tree.leaf : Tree ℕ) = Tree.leaf := rfl
end Func
Example 6. Espelhar preserva o tamanho, aqui na árvore fechada; a lei geral espera a Aula 7.
namespace Func
example : treeSize (mirror t1) = treeSize t1 := rfl
end Func
Example 7. Um tipo soma α ⊕ β guarda um valor de um lado ou do outro, e um match sobre inl/inr o consome.
namespace Func
def fromSum : ℕ ⊕ Bool → ℕ
| .inl n => n
| .inr b => if b then 1 else 0
example : fromSum (.inl 4) = 4 := rfl
end Func
Example 8. Option é o tipo anulável canônico, e uma função pode mapear sobre o seu valor. A lei para some vale para toda função e argumento por computação, sem indução.
namespace Func
def mapOption {α β : Type} (f : α → β) :
Option α → Option β
| none => none
| some a => some (f a)
example {α β : Type} (f : α → β) (a : α) :
mapOption f (some a) = some (f a) := rfl
end Func
Example 9. Um tipo indutivo dependente carrega informação no seu próprio tipo. Um Vec α n é uma lista de comprimento n, e os seus construtores registram o comprimento. Isto é uma prévia somente de leitura; as semanas seguintes desenvolvem os tipos dependentes.
namespace Func
inductive Vec (α : Type) : ℕ → Type where
| nil : Vec α 0
| cons {n : ℕ} : α → Vec α n → Vec α (n + 1)
end Func
Example 10. Como o tipo de vhead exige um vetor não vazio, o caso vazio não pode ocorrer, e a função é total sem uma opção.
namespace Func
def vhead {α : Type} {n : ℕ} : Vec α (n + 1) → α
| .cons x _ => x
def v1 : Vec ℕ 2 := .cons 3 (.cons 4 .nil)
#eval vhead v1
end Func