Агда: вернуть голову и хвост пустого списка

Question

Я изучаю агду и практикуюсь в списках, чтобы лучше понять. Прямо сейчас я пытаюсь написать функции для списка. Я запутался в том, как вернуть голову и хвост пустому списку. Вот мой код:

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

Обход, который я нашел, заключался в том, что вместо возврата первого и последнего членов я возвращаю список, содержащий первый и последний элементы, который выглядит следующим образом:

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 ∷ [])

Но я все еще не понимаю, как вернуть значения головы и хвоста. Как я могу это сделать?

PS Не задание. Мили впереди этого материала в классе

Answer 1

В Agda функции являются общими: если у вас есть head : {A : Set} -> list A -> Aтогда его нужно будет определить по всем спискам. Однако для head [] Вы не можете вызвать в воображении элемент для некоторого произвольного типа A (представить head ([] : list Void)...)

Проблема в том, что ваш тип head обещает слишком много. На самом деле это не так, что вы можете вернуть первый элемент любого списка; Вы можете сделать это только для непустых списков. Так что вам нужно изменить head либо взять отдельное доказательство не пустоты, либо взять непустой список в качестве аргумента:

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!

Answer 2

Это неправильно, это последнее, что вы хотели, чтобы не хвост, и для правильной функции хвоста, вы могли бы просто посмотреть на падение в Data\List\Base.agda стандартной библиотеки:

drop : ∀ {a} {A : Set a} → ℕ → List A → List A
drop zero    xs       = xs
drop (suc n) []       = []
drop (suc n) (x ∷ xs) = drop n xs
--e.g. drop 1
tail : ∀ {a} {A : Set a} → List A → List A
tail []       = []
tail (x ∷ xs) = xs