Agda:返回列表的最后一个元素

Question

当我签入agda-stdlib/src/Data/List/Base.agda时，我看到没有last函数，但在agda-stdlib/src/Data/Vec/Base.agda中看到了last的一个函数。

当我尝试使用它时，我得到一些类型错误，我不确定我是否理解。

我就是这么称呼它的：last (fromList todos)

哪里

todos : List Todo

和

record Todo : Set where
  field
    text      : String
    completed : Bool
    id        : ℕ

我得到的错误是

Data.List.foldr (λ _ → suc) 0 todos != suc _n_31 of type ℕ
when checking that the expression fromList todos has type
Data.Vec.Vec Todo (1 + _n_31)

我猜这与last有这个签名有关：

last : ∀ {n} → Vec A (1 + n) → A

但是我很困惑，因为当我做C-c C-l时：

last (fromList ?)

我实现了这个目标

?0 : List Todo

我觉得todos很满意。

我应该在这里更改什么以使它通过这个错误？或者有其他方法获取List的最后一个元素

谢谢!

编辑

我尝试了一种不同的方法，并决定用Vec替换List。然而，当我尝试去做的时候，我发现了另一个我不太明白的错误

  Todo.completed (last (todos ∷ʳ record { text = text ; completed = false ; id = 1 }))
≡⟨⟩
  Todo.completed (record { text = text ; completed = false ; id = 1 })

false !=
Todo.completed
(last
 (todos ∷ʳ record { text = text ; completed = false ; id = 1 })
 | Data.Vec.initLast
   (todos ∷ʳ record { text = text ; completed = false ; id = 1 }))
of type Bool
when checking that the inferred type of an application
  false ≡ _y_45
matches the expected type
  Todo.completed
  (last
   (todos ∷ʳ record { text = text ; completed = false ; id = 1 }))
  ≡ false

我不知道错误信息在这里说了什么。

编辑

我试图把这个问题进一步简化到

AddNat : ∀ {n : ℕ} → (Vec ℕ n) → (Vec ℕ (1 + n))
AddNat numbers = numbers ∷ʳ 1

AddNatLastAddedElementIsNat :
  ∀ {n : ℕ} (numbers : Vec ℕ (1 + n)) →
    last (AddNat numbers) ≡ 1
AddNatLastAddedElementIsNat numbers =
  begin
    last (AddNat numbers)
  ≡⟨⟩
    last (numbers ∷ʳ 1)
  ≡⟨⟩
    1
  ∎

但我仍然有一个类似的错误：

1 != (last (numbers ∷ʳ 1) | Data.Vec.initLast (numbers ∷ʳ 1)) of
type ℕ
when checking that the expression 1 ∎ has type
last (numbers ∷ʳ 1) ≡ 1

为什么last (numbers ∷ʳ 1)会显示为(last (numbers ∷ʳ 1) | Data.Vec.initLast (numbers ∷ʳ 1))类型？|是否表明它是和类型，并且我需要在这两种情况下进行模式匹配？谢谢!

Answer 1

fromList ?0中的目标确实有List Todo类型，但是由于fromList ?0有类型Vec _ (length ?0)，所以如果打字机得出不能存在n这样的错误，那么length ?0 (确切地说)等于1 + n。在您的情况下，当您说?0 := todos时，就会发生类似?0 := x ∷ todos之类的事情。

通常，像last这样的函数需要知道列表或向量是非空的，另一种方法是定义一个返回Maybe A而不是A的函数。