Listas de números

Generalizando a definição de pares, podemos descrever o tipo de listas de números assim: “Uma lista ou é a lista vazia ou então um conjunto de um elemento e outra Lista", esse tipo não é composto de um head e uma tail.

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

Como vamos tratar de apenas um tipo, é interessante reescrever o tipo de lista para um definido, o escolhido foi o Nat:

type NatList {
  nil
  cons (head: Nat) (tail: NatList)
}

ou

type NatList {
   List Nat
}

Podemos perceber que em ambas as notações, há um head e um tail, sendo que o head recebe um elemento do tipo Nat e a tail recebe uma lista do tipo Nat.

Por exemplo, uma lista de três números naturais 1n, 2n e 3n seria escrita da seguinte forma:

[1n, 2n, 3n]

O Kind, entretanto, lê de outra forma:

[1n, [2n, 3n]]

onde o 1n é a head e o [2n, 3n] é a tail. Da mesma forma, ao olhar para uma lista de 4 elementos [1n, 2n, 3n, 4n], agora veremos da seguinte forma:

[1n, [2n, [3n, 4n]]]

A lista possui o head 1n e a tail [2n, [3n, 4n]], que, por sua vez, possui a head 2n e a tail [3n, 4n] que também possui sua head 3n e sua tail 4n.

Pode parecer assustador, mas é um monstro amigável:

[fonte da imagem: http://learnyouahaskell.com/starting-out]

Repeat

A função repeat recebe um número n e um valor, retornando uma lista de tamanho n onde todos os elementos é o valor declarado.

// Exemplo: (Repeat 3 Bool.true) -> [True, True, True]
Repeat (x: Nat) (count: Nat) : List Nat
Repeat x Nat.zero            = [] 
Repeat x (Nat.succ count)    = List.cons Nat x (Repeat count x)

Length

A função length calcula o tamanho da lista

// Exemplo: (Length [1,2,3]) -> 3
Length (xs: List Nat) : Nat
Length List.nil              = 0n
Length (List.cons head tail) = (Nat.succ (Length tail))

Concat

A função concat concatena (anexa) duas listas.

Concat (xs: List Nat) (ys: List Nat) : List Nat
Concat (List.nil)            ys = ys
Concat (List.cons head tail) ys = List.cons Nat head (Concat tail ys)

Head e Tail

A função head retorna o primeiro elemento (a “cabeça”) da list, enquanto tail retorna tudo menos o primeiro elemento (a “cauda”). Claro, o lista vazia não tem primeiro elemento, então devemos tratar esse caso com um tipo Maybe, recebendo um Maybe.none caso a lista seja vazia ou um Maybe.some caso tenha um valor.

// Exemplo: (Head 0n [1n,2n,3n]) -> 1n
Head (default: Nat) (xs: List Nat) :  Nat
Head default (List.nil)            = default
Head default (List.cons head tail) = head

// Exemplo: (Tail Nat [1,2,3]) -> [2,3]
Tail (xs: List Nat)        : List Nat
Tail (List.nil)            = []
Tail (List.cons head tail) = tail

Test_head1 : Equal Nat (Head 0n [1n,2n,3n]) 1n
Test_head1 = Equal.refl

Test_head2 : Equal Nat (Head 0n List.nil) 0n
Test_head2 = Equal.refl

Test_head3 : Equal (List Nat) (Tail [1n, 2n, 3n]) [2n, 3n]
Test_head3 = Equal.refl

Exercícios

List_funs

Complete as definições de Nonzeros, Oddmembers e Countoddmembers abaixo. Dê uma olhada nos testes para entender o que essas funções devem fazer.

Nonzeros (xs: List Nat) : List Nat
Nonzeros xs = ?

Test_nonzeros : Equal (List Nat) (Nonzeros [0n,1n,0n,2n,3n,0n,0n]) [1n,2n,3n]
Test_nonzeros = ?

Oddmembers (xs: List Nat) : List Nat
Oddmembers xs = ?

Test_oddmembers : Equal (List Nat) (Oddmembers [0n,1n,0n,2n,3n,0n,0n]) [1n,3n]
Test_oddmembers = ?

CountOddMembers (xs: List Nat)  : Nat
CountOddMembers xs = ?

Test_countoddmembers1 : Equal Nat (CountOddMembers [1n,0n,3n,1n,4n,5n]) 4n
Test_countoddmembers1 = ?

Alternate

Complete a definição de alternate, que “compacta” duas listas em uma, alternando entre os elementos tomados da primeira lista e elementos da segunda. Veja os testes abaixo para mais exemplos específicos.

Alternate (xs: List Nat) (ys: List Nat) : List Nat
Alternate xs ys = ?

Test_alternate1 : Equal (List Nat) (Alternate [1n,2n,3n] [4n,5n,6n]) [1n,4n,2n,5n,3n,6n]
Test_alternate1 = ?

Test_alternate2 : Equal (List Nat) (Alternate [1n] [4n,5n,6n]) [1n,4n,5n,6n]
Test_alternate2 = ?

Test_alternate3 : Equal (List Nat) (Alternate  [1n,2n,3n] [4n]) [1n,4n,2n,3n]
Test_alternate3 = ? 

Test_alternate4 : Equal (List Nat) (Alternate [] [20n,30n]) [20n,30n]
Test_alternate4 = ?

Functions

Complete as seguintes definições para as funções count, sum, add, e member das listas de naturais

Count (v: Nat) (xs: List Nat) : Nat
Count v xs = ?

Test_count1 : Equal Nat (Count 1n [1n,2n,3n,1n,4n,1n]) 3n
Test_count1 = ?

Test_count2 : Equal Nat (Count 6n [1n,2n,3n,1n,4n,1n]) 0n
Test_count2 = ?

Sum (xs: List Nat) (ys: List Nat) : List Nat
Sum xs ys = ?

Test_sum1 : Equal Nat (Count 1n (Sum [1n,2n,3n] [1n,4n,1n])) 3n
Test_sum1 = ?

Add (n: Nat) (xs: List Nat) : List Nat
Add n xs = ?

Test_add1 : Equal Nat (Count 1n (Add 1n [1n,4n,1n])) 3n
Test_add1 = ?

Test_add2 : Equal Nat (Count 5n (Add 1n [1n,4n,1n])) 0n
Test_add2 = ?

Member (v: Nat) (xs: List Nat) : Bool
Member v xs = ?

Test_member1 : Equal Bool (Member 1n [1n,4n,1n]) Bool.true
Test_member1 = ?

Test_member2 : Equal Bool (Member 2n [1n,4n,1n]) Bool.false
Test_member2 = ?

More_functions

Aqui estão mais algumas funções de List Nat para você praticar. Quando remove_one é aplicado a uma lista sem o número a ser removido, ele deve retornar a mesma lista inalterada

Remove_one (v: Nat) (xs: List Nat) : List Nat
Remove_one v xs = ?

Test_remove_one1 : Equal Nat (Count 5n (Remove_one 5n [2n,1n,5n,4n,1n])) 0n
Test_remove_one1 = ?

Test_remove_one2 : Equal Nat (Count 5n (Remove_one 5n [2n,1n,4n,1n])) 0n
Test_remove_one2 = ?

Test_remove_one3 : Equal Nat (Count 4n (Remove_one 5n [2n,1n,5n,4n,1n,4n])) 2n
Test_remove_one3 = ?

Test_remove_one4 : Equal Nat (Count 5n (Remove_one 5n [2n,1n,5n,4n,5n,1n,4n])) 1n
Test_remove_one4 = ?

Remove_all (v: Nat) (xs: List Nat) : List Nat
Remove_all v xs = ?

Test_remove_all1  : Equal Nat (Count 5n (Remove_all 5n [2n,1n,5n,4n,1n])) 0n
Test_remove_all1  = ?

Test_remove_all2  : Equal Nat (Count 5n (Remove_all 5n [2n,1n,4n,1n])) 0n
Test_remove_all2  = ?

Test_remove_all3  : Equal Nat (Count 4n (Remove_all 5n [2n,1n,5n,4n,1n,4n])) 2n
Test_remove_all3  = ?

Test_remove_all4  : Equal Nat (Count 5n (Remove_all 5n [2n,1n,5n,4n,5n,1n,4n,5n,1n,4n])) 0n
Test_remove_all4  = ?

Subset (xs: List Nat) (ys: List Nat)  : Bool
Subset xs ys = ?

Test_subset1 : Equal Bool (Subset [1n,2n] [2n,1n,4n,1n]) Bool.true
Test_subset1 = ?

Test_subset2 : Equal Bool (Subset [1n,2n,2n] [2n,1n,4n,1n]) Bool.false
Test_subset2 = ?

Theorem

Anote um teorema interessante, envolvendo as funções count e add e prove-o. Note que, como este problema é um pouco aberto, é possível que você venha com um teorema que seja verdadeiro, mas cuja prova requer técnicas que você ainda não aprendeu. Sinta-se à vontade para pedir ajuda se ficar preso!

Theorem : ?