Polimorfismo

Neste capítulo, continuamos nosso desenvolvimento de conceitos básicos de programação. Nossos novos princípios essenciais são o polimorfismo (funções de abstração sobre o tipos de dados que eles manipulam) e funções de ordem superior (funções de tratamento como dados). Começamos com o polimorfismo.

Listas Polimórficas

Nos últimos dois capítulos, trabalhamos com listas polimórficas, você pode só não ter percebido. Obviamente, programas interessantes também precisam ser capazes de manipular listas com elementos de outros tipos – listas de strings, listas de booleanos, listas de listas, etc. Poderíamos apenas definir um novo tipo de dados indutivo para cada um deles, por exemplo...

type BoolList {
   nil 
   cons (head: Bool) (tail: List Bool) 
}

.. mas isso rapidamente se tornaria tedioso, em parte porque temos que compensar nomes de construtor diferentes para cada tipo de dados, mas principalmente porque também precisamos definir novas versões de todas as nossas funções de manipulação de listas (length, rev, etc.) para cada nova definição de tipo de dados.

Para evitar toda essa repetição, o Kind suporta definições de tipos indutivos polimórficos. Por exemplo, aqui está um tipo de dados de lista polimórfica e que já vimos no capítulo anterior:

type List (t) {
   nil 
   cons (head: t) (tail: List t) 
}

Esse tipo já exite no Kind e podemos perceber que ele é idententico ao BoolList , mas com um tipo a, esse tipo recebe qualquer outro tipo, seja Nat, Bool, Maybe e etc. Não precisamos criar um tipo de lista para cada um dos tipos de dados, podemos usar esse que adota todas as formas existentes.

Que tipo de coisa é a própria Lista? Uma boa maneira de pensar sobre isso é que List é uma função de Tipos para defi nições indutivas; ou, em outras palavras, List é uma função de Tipos para Tipos. Para qualquer tipo específico x, o tipo List x é um conjunto indutivamente definido de listas cujos elementos são do tipo x.

Com esta definição, quando usamos os construtores List.nil e List.cons para construir listas, precisamos dizer ao Kind o tipo dos elementos nas listas que estamos construindo - isto é, que List.nil e List.cons agora são construtores polimórficos. Observe os tipos de construtores:

record Pair (a) (b) {
  fst : a
  snd : b
}

Nosso tipo Pair recebe outros dois tipos, o a e o b e retorna um par dos dois tipos. Não foi necessário definir se o par era de números naturais, booleanos, listas, bits ou outros pares, nós deixamos a função apta a tratar todos os pares possíveis e isso é graças ao polimorfismo.

Agora podemos voltar e fazer versões polimórficas de todas as listas de processamento funções que escrevemos antes. Aqui está a repetição, por exemplo:

Repeat <a: Type> (x: a) (count: Nat) : List a
Repeat a x Nat.zero                  = List.nil
Repeat a x (Nat.succ count)          = List.cons x (Repeat x count)

Tal como acontece com List.nil e Contras, podemos usar repeat aplicando-o primeiro a um tipo e depois a seu argumento de lista:

Test_repeat1 : Equal (Repeat 4n 2n) (List.cons 4n (List.cons 4n List.nil))
Test_repeat1 = Equal.refl

Para usar repeat para construir outros tipos de listas, simplesmente instanciamos com um parâmetro de tipo apropriado:

Test_repeat2 : Equal (Repeat Bool.false 1n) (List.cons Bool.false List.nil)
Test_repeat2 = Equal.refl

Inferência de anotação de tipo

Vamos escrever a definição do repeat novamente, mas dessa vez omitindo o tipo, mas atenção, essa não é uma boa prática usar o hole, servirá apenas para compreender o poder do Kind e como ele pode ajudar o usuário a encontrar o que deseja.

Repeat (x: _) (count: Nat) : List _
Repeat x Nat.zero          = ?

Ao rodar o Type Check o terminal nos retorna:

+ INFO  Inspection.

   • Expected: (List _) 

   • Context: 
   •   x : _ 

   Repeat x Nat.zero = ?
                       ┬
                       └Here!

Para o caso do contador ser zero, que é o nosso ponto de parada, nós precisamos retornar uma lista do tipo não definido. Como fizemos quando nosso tipo era definido, estamos criando uma lista que não repete o termo nenhuma vez, retornamos um List.nil, depois nós verificamos para o caso de uma lista que repetirá o valor count vezes, para isso nós usaremos a recursão por meio do Nat.succ pred, isto é, o nosso count é igual ao sucessor do predecessor dele.

Repeat x (Nat.succ count) = ?

E o o Type Check nos retorna:

+ INFO  Inspection.

   • Expected: (List _) 

   • Context: 
   •   x     : _ 
   •   count : Nat 

   Repeat x (Nat.succ count) = ?
                               ┬
                               └Here!

Agora basta construir a lista com o valor e chamar a função para o predecessor de count, assim construindo a lista até que chegue a zero.

Repeat (x: _) (count: Nat) : List _
Repeat x Nat.zero          = List.nil
Repeat x (Nat.succ count)  = List.cons x (Repeat x count)

Podemos perceber que, apesar de não definir o tipo de x, o Kind é poderoso para descobrir o tipo que é nosso x quando usamos o hole _. Embora seja possível e possa até facilitar construir uma aplicação inteira usando essa notação, não é uma boa prática, já que, a depender do caso, pode ser inferido um tipo diferente do que o desejado. É interessante sempre definir o tipo do nosso elemento, mesmo que seja um tipo polimórfico.

No primeiro caso, quando definimos o tipo a, já abarcamos todos os tipos possíveis, não sendo necessário o uso do hole e essa é a mágica do polimorfismo, ele nos permite usar uma mesma função para diversos tipos diferentes.

Para usar uma função polimórfica, nós precisamos passar um ou mais tipos em adição aos outros argumentos. Por exemplo, no caso do repeat, nós passamos o tipo <a: Type> e que cada elemento da nossa lista é desse tipo. Fizemos o mesmo com o tipo Pair, que recebia como argumento dois tipos a e b.

Agora fica muito mais fácil compreender os exemplos que usamos no capítulo anterior, quando apresentamos funções como a de length e append:

Length <a> (xs: List a) : Nat
Length (List.nil t)            = Nat.zero
Length (List.cons t head tail) = (Nat.succ (Length tail))

Concat <a: Type> (xs: List a) (ys: List a) : List a
Concat (List.nil)                     ys = ys
Concat (List.cons head tail)          ys = List.cons head (Concat tail ys)

Perceba, há duas notações, uma onde apenas usamos <a> e outra onde usamos <a: Type>, podemos usar qualquer uma delas, o Kind é capaz de compreender as duas formas, será de escolha do desenvolvedor qual ele usará e da complexidade do que será desenvolvido, uma vez que, em códigos muito complexos, talvez seja interessante deixar explícito a outros programadores o que é cada coisa.

Agora é a hora de implementar nossas funções com o tipo implícito, usando o hole e sugar syntax:

Concat_implicito (xs: List _) (ys: List _) : List _
Concat_implicito []                     ys = ys
Concat_implicito (List.cons head tail)  ys = List.cons head (Concat_implicito tail ys)

Aqui nós aprendemos mais uma coisa, o sugar syntax para uma lista vazia e que é apenas [], mas isso está errado, uma vez que o sugar syntax no kind não funciona no lado esquerdo do escopo da função, somente do lado direito funciona. Ao usar o sugar syntax errado, o que o Kind apresenta como erro:

- ERROR  Unexpected token '['.
    Concat_implicito []  ys = ys
                  ┬
                  └Here!

Portanto, é sempre importante saber exatamente o que está sendo feito, ainda mais quando usamos sugar syntax, ela serve pra facilitar a nossa vida, mas pode causar alguns problemas quando usada de forma indevida e isso serve igualmente para o hole e tipos polimórficos nos auxiliam a escrever um programa mais seguro e, ao mesmo tempo, capaz de servir para inúmeros casos.

Outra função que podemos reescrever é a de reverse:

Rev <a> (xs: List a) : List a
Rev List.nil              = [] // sugar syntax de List.nil
Rev (List.cons head tail) = Concat (Rev tail) [head] // sugar syntax de (List.cons head List.nil)

Length <a> (xs: List a) : Nat
Length List.nil              = 0n // sugar syntax de Nat.zero
Length (List.cons head tail) = Nat.succ (Length tail)

Feito isso, basta apenas provar que nossas funções são verdadeiras:

Test_rev1 : Equal (Rev [1,2,3]) [3,2,1]
Test_rev1 = Equal.refl

Test_rev2 : Equal (Rev [Bool.true]) [Bool.true]
Test_rev2 = Equal.refl

Test_length1 : Equal (Length [1,2,3]) 3n
Test_length1 = Equal.refl

Exercícios polimórficos

Aqui estão alguns exercícios simples, semelhantes aos da seção de Listas, para praticar o polimorfismo. Complete as provas abaixo.

Concat_nil_r <a> (xs: List a) : Equal (Concat xs List.nil) xs
Concat_nil_r xs = ?

Concat_assoc <a> (xs: List a) (ys: List a) (zs: List a) : Equal (Concat xs (Concat ys zs)) (Concat (Concat xs ys) zs)
Concat_assoc xs ys zs = ?

Concat_length <a> (xs: List a) (ys: List a) : Equal (Length (Concat xs ys)) (Plus (Length xs) (Length ys))
Concat_length xs ys = ?

Mais exercícios polimórficos

Aqui estão alguns um pouco mais interessantes...

Rev_app_distr <a> (xs: List a) (ys: List a) : Equal (Rev (Concat xs ys)) (Concat (Rev ys) (Rev xs))
Rev_app_distr xs ys = ?

Rev_involutive <a> (xs: List a) : Equal (Rev (Rev xs)) xs
Rev_involutive xs = ?

Pares polimórficos

Seguindo o mesmo padrão, a definição de tipo que demos no último capítulo para pares de números podem ser generalizados para polimórficos pares:

record Pair (a) (b) {
  fst : a
  snd : b
} 

Essa é exatamente a primeira definição de pares que vimos no capítulo anterior e, agora, podemos compreender perfeitamente o que são os tipos a e b na definição do tipo Pair.

Nós podemos refazer as funções de Pares, mas agora para tipos polimórficos:

Fst <a> <b> (pair: Pair a b) : a
Fst (Pair.new fst snd) = fst

Snd <a> <b> (pair: Pair a b) : b
Snd (Pair.new fst snd) = snd

A seguinte função recebe duas listas e combina elas numa lista de pares. Nas linguagens funcionais, isso é comumente chamada de Zip.

Zip <a> <b> (xs: List a) (ys: List b) : (List (Pair a b))
Zip [] ys = []
Zip xs [] = []
Zip (List.cons xs.h xs.t) (List.cons ys.h ys.t) = List.cons (Pair.new xs.h xs.t) (Zip xs.t ys.t)

Check

Sem rodar o programa, tente responder a seguinte pergunta:

• O que a combinação de [1, 2] e [Bool.true, Bool.false, Bool.false, Bool.true] retornará?

Agora rode o código e veja se acertou.

Split

A função Split é o inverso da Zip, ela recebe uma lista de pares e retorna um par de listas. Em muitas linguagens funcionais ela é chamada de Unzip.

Preencha a definição de divisão abaixo. Certifique-se de que ela passe no teste unitário fornecido.

Split <a> <b> (xs: List (Pair a b)) : Pair (List a) (List b)
Split xs = ?

Test_split : Equal (Split [(Pair.new 1 Bool.false), (Pair.new 2 Bool.false)]) (Pair.new ([1, 2]) ([Bool.false, Bool.false]))
Test_split = ?

Polimorfismo com maybe

No capítulo anterior, nós também vimos o tipo Maybe, só que para tipos naturais, entretanto, como vimos no capítulo atual, nossas estruturas de dados podem ser polimórficas, o que significa que o tipo Maybe também é polimórfico e é isso o que veremos agora.

type Maybe (t) {
  none 
  some (value: t)
}

Dessa forma, podemos escrever a função do enésimo erro para ele ser usado com todos os tipos de listas:

Nth_error <a> (n: Nat) (xs: List a) : Maybe a
Nth_error a n List.nil              = Maybe.none
Nth_error a n (List.cons head tail) =
  let ind = Nth_error (Pred n) tail
  Bool.if (Eql n 0n) (Maybe.some head) (ind)


Test_nth_error1 : Equal (Nth_error 0n [4n,5n,5n,7n]) (Maybe.some 4n)
Test_nth_error1 = Equal.refl

Test_nth_error2 : Equal (Nth_error 2n [Bool.true]) Maybe.none
Test_nth_error2 = Equal.refl

Test_nth_error3 : Equal (Nth_error 1n [[1n],[2n]]) (Maybe.some [2n])
Test_nth_error3 = Equal.refl

Hd_error

Complete a definição de uma versão polimórfica da função Hd_error do último capítulo. Certifique-se de que ele passe nos testes de unitários abaixo.

Hd_error <a> (xs: Lista a) : Maybe a
Hd_error xs = ?

Test_hd_error1 : Equal (Hd_error [1, 2]) (Maybe.some 1)
Test_hd_error1 = ?

Test_hd_error2 : Equal (Hd_error [[1], [2]]) (Maybe.some [1])
Test_hd_error2 = ?