6.3. Casamento de Padrões como Expressão
A Aula 3 escreveu uma função como equações de nível superior, uma por forma de construtor. O mesmo poder está disponível como uma expressão match usável onde quer que um termo seja esperado, e como if c then … else … para uma condição decidível. Um match se traduz por meio do recursor do tipo, o seu casesOn da §6.1 nos casos mais simples, e if ramifica sobre uma instância Decidable da sua condição. Os padrões são tentados de cima para baixo, então um padrão anterior encobre um posterior, e o coringa _ casa com qualquer coisa.
namespace Func
def classify (n : ℕ) : String :=
match n with
| 0 => "zero"
| 1 => "one"
| _ => "many"
def pred? : ℕ → Option ℕ
| 0 => none
| n + 1 => some n
end Func
O tipo Option empacota um resultado parcial, some x para um valor e none para a sua ausência, então pred? é total embora o predecessor de 0 seja indefinido.
6.3.1. Exemplos
Os exemplos abaixo usam match e if dentro de um corpo, sobre números, pares, listas e opções.
Example 1. Um match devolvendo uma classificação, o seu coringa capturando todos os casos restantes.
namespace Func
example : classify 7 = "many" := rfl
end Func
Example 2. if testa uma condição decidível, aqui se um número é zero.
namespace Func
def isZero (n : ℕ) : Bool :=
if n = 0 then true else false
example : isZero 0 = true := rfl
end Func
Example 3. Um match sobre um par inspeciona as duas componentes de uma vez.
namespace Func
def bothZero (p : ℕ × ℕ) : Bool :=
match p with
| (0, 0) => true
| _ => false
example : bothZero (0, 3) = false := rfl
end Func
Example 4. pred? devolve none em zero, então o resultado está sempre definido.
namespace Func
example : pred? 0 = none := rfl
end Func
Example 5. Um match sobre uma lista devolve a cabeça como uma opção.
namespace Func
def firstOpt {α : Type} : List α → Option α
| [] => none
| x :: _ => some x
example : firstOpt [3, 1] = some 3 := rfl
end Func
Example 6. Um match sobre uma opção desempacota some e fornece um padrão para none.
namespace Func
def orZero : Option ℕ → ℕ
| none => 0
| some n => n
example : orZero (some 5) = 5 := rfl
end Func
Example 7. Os padrões são tentados de cima para baixo, então o caso específico precede o coringa.
namespace Func
def sign (n : ℤ) : String :=
match n with
| 0 => "zero"
| _ => "nonzero"
example : sign 0 = "zero" := rfl
end Func
Example 8. Um match pode aparecer dentro de um termo maior, aqui dentro de uma adição.
namespace Func
def bump (o : Option ℕ) : ℕ :=
1 + (match o with
| none => 0
| some n => n)
example : bump (some 4) = 5 := rfl
end Func
Example 9. if e um match de dois ramos decidem a mesma condição.
namespace Func
def isZeroMatch (n : ℕ) : Bool :=
match n with
| 0 => true
| _ => false
example : isZeroMatch 0 = isZero 0 := rfl
end Func
Example 10. Uma divisão segura devolvendo none quando o divisor é zero.
namespace Func
def safeDiv (m n : ℕ) : Option ℕ :=
if n = 0 then none else some (m / n)
example : safeDiv 6 0 = none := rfl
end Func