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：空列表的回头和尾部

回答

相关问题