Agda：空列表的回頭和尾部

我正在學習agda並在列表上練習以獲得更好的理解。現在我正在嘗試爲列表編寫函數。我很困惑如何返回空列表的首尾。這裏是我的代碼：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不是任務。里程數

來源

2017-02-16 danny

空表沒有頭和尾。你不能退還不存在的東西。 –

@AndrásKovács這是否意味着我從不在agda中寫這樣的函數？除了返回列表之外，還有其他解決方法嗎？在Agda中 – danny

函數的類型是非常字面的。一個'A - > B'函數爲每個'A'返回一個'B'，它永遠不會循環，永遠不會拋出異常，除了返回一個'B'外不會做任何事情。如果您發現某個類型沒有實現，則必須更改該類型。在這種情況下，您可能有'head：{A：Set} - > list A - > Maybe A'，或者使用'Data.Vec'中的'Vec'來支持'head'和'tail'以獲得非空向量。 –

在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!

來源

2017-02-17 03:26:30 Cactus

Agda：空列表的回頭和尾部

回答

相關問題