3.2. Tipos Indutivos
O comando inductive define um tipo novo listando os seus construtores. O tipo contém exatamente os valores construídos por finitas aplicações de construtores, e nada mais. A definição abaixo reconstrói os números naturais dentro de um espaço de nomes, já que o nome Nat pertence a Lean.
namespace MyNat
inductive Nat : Type where
| zero : Nat
| succ : Nat → Nat
end MyNat
Os comandos #check e #print inspecionam o resultado. O construtor succ recebe um Nat e constrói o seguinte.
#check MyNat.Nat.succ
#print MyNat.Nat
Construtores podem carregar dados de outros tipos. O tipo abaixo representa expressões aritméticas com constantes inteiras, variáveis nomeadas por cadeias de caracteres e quatro operadores. Ele é a sintaxe abstrata de uma linguagem pequena, e a linguagem imperativa das últimas aulas o estende.
inductive AExp : Type where
| num : ℤ → AExp
| var : String → AExp
| add : AExp → AExp → AExp
| sub : AExp → AExp → AExp
| mul : AExp → AExp → AExp
| div : AExp → AExp → AExp
Por fim, as listas. Uma lista sobre α é vazia ou é um elemento seguido de uma lista. Como no caso de Nat, Lean já fornece List, então a reconstrução vive em um espaço de nomes.
namespace MyList
inductive List (α : Type) : Type where
| nil : List α
| cons : α → List α → List α
end MyList
3.2.1. Exemplos
Os exemplos abaixo constroem valores dos tipos indutivos desta seção e os inspecionam com #check e #print.
Exemplo 1. O numeral três são três aplicações de succ a zero.
#check MyNat.Nat.succ
(MyNat.Nat.succ (MyNat.Nat.succ MyNat.Nat.zero))
Exemplo 2. Uma enumeração é um tipo indutivo cujos construtores não carregam dados.
inductive Answer : Type where
| yes : Answer
| no : Answer
| maybe : Answer
#check Answer.maybe
Exemplo 3. A expressão (x + 3) * y é um valor de AExp. As aplicações de construtores espelham a forma da expressão.
#check AExp.mul
(AExp.add (AExp.var "x") (AExp.num 3))
(AExp.var "y")
Exemplo 4. A lista que contém 3 e 7 são duas aplicações de cons terminadas em nil.
#check MyList.List.cons 3
(MyList.List.cons 7 MyList.List.nil)
Exemplo 5. Um construtor pode receber vários argumentos. O tipo abaixo empacota dois inteiros.
inductive Interval : Type where
| mk : ℤ → ℤ → Interval
#check Interval.mk 1 5
Exemplo 6. #print lista os construtores de um tipo.
#print MyList.List
Exemplo 7. Aplicações de construtores se aninham a qualquer profundidade. O valor abaixo é a expressão x / 0, um trecho de sintaxe legítimo cuja avaliação as próximas seções discutem.
#check AExp.div (AExp.var "x") (AExp.num 0)
Exemplo 8. Os numerais do próprio Lean elaboram para o Nat do núcleo. A reconstrução e o original são tipos distintos.
#check (3 : ℕ)
Exemplo 9. A lista vazia sobre ℤ exige uma anotação de tipo, já que nil sozinho não determina α.
#check (MyList.List.nil : MyList.List ℤ)
Exemplo 10. Os quatro pontos cardeais como uma enumeração, impressos.
inductive Direction : Type where
| north : Direction
| south : Direction
| east : Direction
| west : Direction
#print Direction