Блог

Когда я регистрируюсь, 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 , был удовлетворен.

Что я должен изменить здесь, чтобы он передавал эту ошибку? Или есть другой способ получить последний элемент a 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)) ? | Указывает ли это на тип суммы, и мне нужно будет сопоставить шаблон в обоих случаях? Спасибо!

Цель в fromList ?0 имеет тип List Todo , но поскольку fromList ?0 имеет тип Vec _ (length ?0) , вы получите сообщение об ошибке, если средство проверки типов придет к выводу, что не может быть n такого, которое length ?0 (по определению) равно 1 n . В вашем случае это происходит, как только вы это говорите ?0 := todos ?0 := x ∷ todos , вместо этого сработало бы что-то вроде.

Обычно функция like last должна знать, что список или векторы непустые, альтернативой является определение функции, которая возвращает Maybe A вместо A though .