I am learning agda and practicing on lists to get a better understanding. Right now I am trying to write functions for list. I am confused on how to return the head and tail of an empty list. Here is my code:
data list (A : Set) : Set where
[] : list A
_∷_ : A → list A → list A
Null : {A : Set} → (list A) → Bool
Null [] = true
Null (x ∷ a) = false
tail : {A : Set} → (list A) → A
tail [] = {!!}
tail (x ∷ []) = x
tail (x ∷ a) = tail a
head : {A : Set} → (list A) → A
head [] = {!!}
head (x ∷ a) = x
A work around that I found was that instead of returning the first and last members I return a list containing the first and last members which is as follows:
tail : {A : Set} → (list A) → (list A)
tail [] = []
tail (x ∷ []) = x ∷ []
tail (x ∷ a) = tail a
head : {A : Set} → (list A) → (list A)
head [] = []
head (x ∷ a) = (x ∷ [])
But I am still confused about how to return the head and tail values. How can I do this?
P.S Not an assignment. Miles ahead of this stuff in class
In Agda, functions are total: if you have head : {A : Set} -> list A -> A, then it will need to be defined over all lists. However, for head [] you can't conjure up an element for some arbitrary type A (imagine head ([] : list Void)...)
The problem is that your type of head promises too much. It is not, in fact, true that you can return the first element of any list; you can only do it for non-empty lists. So you need to change head to either take a separate proof of non-emptiness, or to take a non-empty list as argument:
module SeparateProof where
open import Data.List
open import Data.Bool
open import Data.Unit
head : {A : Set} → (xs : List A) → {{nonEmpty : T (not (null xs))}} → A
head [] {{nonEmpty = ()}} -- There's no way to pass a proof of non-emptiness for an empty list!
head (x ∷ xs) = x
module NonEmptyType where
open import Data.List.NonEmpty hiding (head)
head : {A : Set} → List⁺ A → A
head (x ∷ xs) = x -- This is the only pattern matching a List⁺ A!