6.5. Classes de Tipos
Uma classe de tipos é uma estrutura de operações parametrizada por um ou mais argumentos, em geral tipos. Uma class declara as operações, uma instance as fornece para argumentos particulares, e a resolução de instâncias encontra a instância certa a partir desses argumentos sempre que uma função a pede com [C α]. Algumas classes são indexadas por mais do que um tipo, e Std.Associative op da Aula 4 é indexada por uma operação. É o mecanismo que a Aula 2 usou para dar ao ∈ o seu significado por meio de uma instância de Membership e a Aula 4 usou para registrar add como associativo e comutativo para ac_rfl.
namespace Func
class Size (α : Type) where
size : α → ℕ
instance {α : Type} : Size (List α) where
size xs := xs.length
instance {α : Type} : Size (Option α) where
size
| none => 0
| some _ => 1
def usize {α : Type} [Size α] (a : α) : ℕ :=
Size.size a
end Func
A função usize não nomeia nenhuma instância. Ela pede [Size α], e a resolução fornece a instância de lista ou a instância de opção conforme o tipo no ponto de chamada.
6.5.1. Exemplos
Os exemplos abaixo declaram instâncias, observam a resolução escolher por tipo e nomeiam as classes que as aulas anteriores usaram.
Example 1. A instância de lista mede uma lista pelo seu comprimento.
namespace Func
#eval usize [1, 2, 3]
end Func
Example 2. A instância de opção mede a presença, 1 ou 0.
namespace Func
#eval usize (some 7)
end Func
Example 3. Uma instância pode depender de outras instâncias, como um produto depende dos seus fatores.
namespace Func
instance {α β : Type} [Size α] [Size β] :
Size (α × β) where
size p := Size.size p.1 + Size.size p.2
#eval usize ([1, 2], some 3)
end Func
Example 4. A resolução escolhe a instância a partir do tipo apenas, o que inferInstance torna explícito.
namespace Func
#check (inferInstance : Size (List ℕ))
end Func
Example 5. Uma classe pode dar a um campo um valor padrão, que uma instância pode deixar intocado ou substituir.
namespace Func
class Greet (α : Type) where
label : String := "item"
instance : Greet Bool where
instance : Greet ℕ where
label := "number"
#eval (Greet.label (α := Bool))
#eval (Greet.label (α := ℕ))
end Func
Example 6. O ∈ da Aula 2 é o método da classe Membership, resolvido pelo tipo do contêiner.
#check @Membership.mem
Example 7. Lean pode construir algumas instâncias automaticamente com deriving, aqui a igualdade e uma forma textual para um tipo finito.
namespace Func
inductive Coin where
| heads
| tails
deriving Repr, DecidableEq
#eval Coin.heads
end Func
Example 8. A igualdade derivada permite a decide resolver uma desigualdade concreta.
namespace Func
example : Coin.heads ≠ Coin.tails := ⊢ Coin.heads ≠ Coin.tails All goals completed! 🐙
end Func
Example 9. Um método de classe carrega um argumento de instância implícito, que #check exibe.
namespace Func
#check @Size.size
end Func
Example 10. A associatividade e a comutatividade que ac_rfl consultou na Aula 4 são instâncias de Std.Associative e Std.Commutative.
#check @Std.Associative
#check @Std.Commutative