3.4. Polimorfismo e Argumentos Implícitos🔗

Uma definição pode receber um tipo como argumento. A função abaixo concatena duas listas sobre um tipo α qualquer, dado explicitamente em cada chamada, e o _ de Lean pede ao elaborador que o infira. O elaborador é a etapa de Lean que transforma o texto que escrevemos em um termo da linguagem núcleo, e a inferência é parte do seu trabalho, junto com a resolução de instâncias de classes de tipos e a execução de táticas. A Figura 1.1 o situa entre os demais componentes. Escrever _ afirma, portanto, que o argumento está determinado pelo resto da chamada, e o elaborador o recupera por unificação.

def append (α : Type) : List α → List α → List α
  | List.nil,       ys => ys
  | List.cons x xs, ys => List.cons x (append α xs ys)

[3, 1, 4, 1, 5]#eval append ℕ [3, 1] [4, 1, 5]

As chaves tornam o argumento de tipo implícito, inferido a cada uso. O prefixo @ restaura a forma explícita quando necessário.

def appendImplicit {α : Type} : List α → List α → List α
  | List.nil,       ys => ys
  | List.cons x xs, ys => List.cons x (appendImplicit xs ys)

[3, 1, 4, 1, 5]#eval appendImplicit [3, 1] [4, 1, 5]
@appendImplicit : {α : Type} → List α → List α → List α#check @appendImplicit

A notação de listas de Lean escreve List.nil como [], List.cons x xs como x :: xs, e cadeias de cons como [x₁, x₂, x₃]. Com ela, a definição se lê como a sua própria especificação.

def appendPretty {α : Type} : List α → List α → List α
  | [],      ys => ys
  | x :: xs, ys => x :: appendPretty xs ys

A reversão segue a mesma forma, concatenando a cabeça na outra ponta.

def reverse {α : Type} : List α → List α
  | []      => []
  | x :: xs => appendPretty (reverse xs) [x]

3.4.1. Exemplos🔗

Os exemplos abaixo comparam argumentos de tipo explícitos e implícitos e definem funções polimórficas sobre listas e pares.

Exemplo 1. Com um argumento de tipo explícito, o tipo aparece na assinatura como um argumento comum.

append : (α : Type) → List α → List α → List α#check @append

append : (α : Type) → List α → List α → List α

Exemplo 2. As chaves marcam o argumento como implícito, e @ o exibe.

@appendPretty : {α : Type} → List α → List α → List α#check @appendPretty

@appendPretty : {α : Type} → List α → List α → List α

Exemplo 3. Na chamada, o argumento implícito vem do tipo das listas.

[1, 2, 3]#eval appendPretty [1, 2] [3]

[1, 2, 3]

Exemplo 4. A mesma definição serve a outro tipo sem mudança alguma.

["a", "b"]#eval appendImplicit ["a"] ["b"]

["a", "b"]

Exemplo 5. O prefixo @ restaura a forma explícita, útil quando a inferência não tem com o que trabalhar.

[1, 2]#eval @appendImplicit ℕ [1] [2]

[1, 2]

Exemplo 6. A função identidade é polimórfica e devolve o seu argumento inalterado.

def idPoly {α : Type} (x : α) : α := x

@idPoly : {α : Type} → α → α#check @idPoly

@idPoly : {α : Type} → α → α

Exemplo 7. Construir uma lista de um elemento funciona em todo tipo.

def singletonList {α : Type} (x : α) : List α := [x]

[5]#eval singletonList 5

[5]

Exemplo 8. Uma definição pode receber dois argumentos de tipo. A troca das componentes de um par as intercambia.

def swapPair {α β : Type} : α × β → β × α
  | (x, y) => (y, x)

("x", 1)#eval swapPair (1, "x")

("x", 1)

Exemplo 9. O comprimento de uma lista ignora os elementos, então o argumento de tipo não aparece no resultado.

def lengthPoly {α : Type} : List α → ℕ
  | []      => 0
  | _ :: xs => lengthPoly xs + 1

3#eval lengthPoly ["a", "b", "c"]

Exemplo 10. Uma lista vazia não carrega elemento algum do qual inferir, e uma anotação de tipo fixa o argumento implícito.

[] : List ℕ#check ([] : List ℕ)

[] : List ℕ