Agda : 빈 목록의 머리와 꼬리를 되 돌린다

Question

나는 agda를 배우고 더 나은 이해를 얻기 위해 목록에 연습하고있다. 지금은 목록에 함수를 작성하려고합니다. 빈 목록의 머리와 꼬리를 반환하는 방법에 대해 혼란 스럽습니다.

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

그러나 머리와 꼬리 값을 반환하는 방법에 대해서는 여전히 혼란 스럽습니다. 어떻게해야합니까?

P.S 배정되지 않았습니다. 클래스의 물건보다 앞서서의 마일

Answer 1

Agda에서 함수는 총계입니다 : head : {A : Set} -> list A -> A 인 경우 모든 목록에 대해 정의해야합니다. 그러나 head []을 위해 당신은 어떤 임의의 유형 A을위한 요소 (head ([] : list Void) 상상 ...)

문제는 그 head 약속의 당신의 유형 너무 많이를 연상 할 수 없습니다. 사실, 어떤 목록의 첫 번째 요소를 반환 할 수는 없습니다. 비어 있지 않은 목록에 대해서만이 작업을 수행 할 수 있습니다. 그래서 당신은에 head을 변경하거나 비 emptiness의 separate proof을, 또는 인수로 non-empty list를 취할 필요가 :

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!