Maybe

Suppose we want to write a function that returns the nth number of a list. We then define a number that is applied to a list of naturals and returns the number that occupies that position. Therefore, we need to define a number to be returned if the number is greater than the size of the list.

Nth_bad (n: Nat) (xs: List Nat)            : Nat
Nth_bad n List.nil                         = 42n // arbitrary value 
Nth_bad Nat.zero (List.cons head tail)     = head
Nth_bad (Nat.succ n) (List.cons head tail) = Nth_bad n tail

This solution is not so good: if nth_bad returns 0, we cannot tell if that value actually appears in the input without further processing. A better alternative is to change the return type of nth_bad to include an error value as a possible result.

We call this type Maybe, because it may or may not have something; if it has, it is a Maybe.some of that something, if it does not have, it is a Maybe.none.

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

We can then change the above definition of nth_bad to return None when the list is too short and Some when the list has enough members and appears at the position n. We call this new function nth_error to indicate that it may result in an error.

This proof also serves to introduce us to another feature of Kind, conditional expressions, the if and 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

Using the same idea, correct the Head function from before so that we don't have to pass a default element for the case 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

This exercise relates your new Head_error to the old Head.

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