Maybe

Suponha que a gente queira escrever uma função que retorna o enésimo número de uma lista. Nós então definimos um número que é aplicado a uma lista de naturais e então retorna o número que ocupa essa posição. Dessa forma, nós precisamos definir um número para ser retornado caso o número seja maior do que o tamanho da lista.

Nth_bad (n: Nat) (xs: List Nat)            : Nat
Nth_bad n List.nil                         = 42n // Valor arbitrário 
Nth_bad Nat.zero (List.cons head tail)     = head
Nth_bad (Nat.succ n) (List.cons head tail) = Nth_bad n tail

Esta solução não é tão boa: se nth_bad retornar 0, não podemos dizer se esse valor realmente aparece na entrada sem processamento adicional. Uma alternativa melhor é para alterar o tipo de retorno de nth_bad para incluir um valor de erro como um possível resultado. Chamamos esse tipo Maybe, pois ele pode ou não ter algo, se tiver é um Maybe.some desse algo, se não tiver, é um Maybe.none.

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

type NatMaybe {
  none 
  some (value: Nat)
}

ou

type NatMaybe { 
  Maybe Nat
}

Podemos então alterar a definição acima de nth_bad para retornar None quando a lista for muito curto e Some a quando a lista tem membros suficientes e aparece na posição n. Chamamos essa nova função de nth_error para indicar que pode resultar em um erro.

Essa prova ainda serve pra nos apresentar outro recurso do Kind, expressões condicionais, o if e else

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

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

Test_nth_error2 : Equal (Nth_error 3n [4n,5n,6n,7n]) (Maybe.some 7n)
Test_nth_error2 = Equal.refl

Test_nth_error3 : Equal (Nth_error 9n [4n,5n,6n,7n]) Maybe.none
Test_nth_error3 = Equal.refl

Extract (d: Nat) (o: Maybe Nat) : Nat
Extract d (Maybe.some k)        = k
Extract d (Maybe.none)          = d

Head_error

Usando a mesma ideia, corrija a função Head de antes para que não tenhamos que passar um elemento padrão para o caso List.nil

Head_error (xs: List Nat) : Maybe Nat
Head_error xs = ?

Test_head_error1 : Equal (Head_error List.nil) Maybe.none
Test_head_error1 = ?

Test_head_error2 : Equal (Head_error [1n]) (Maybe.some Nat 1n)
Test_head_error2 = ?

Test_head_error3 : Equal (Head_error  [5n,6n]) (Maybe.some Nat 5n)
Test_head_error3 = ?

Opcional: Extract_head

Este exercício relaciona sua novo Head_error para o antigo Head.

Extract_head (l: List Nat) (default: Nat) : Equal Nat (Head default l)  (Extract default (Head_error l))
Extract_head l default = ?