我的问题

absurd是处理impossible情况的一种替代方法，我们可以用另一种方法重写一种用法吗？还是它们通常是处理根本不同问题的方法？

详细信息

在使用Idris进行类型驱动的开发中 ch。参考图9，Brady通过编写一个在证明元素位于Vect中的条件下引导用户从Vect中删除元素的功能。他到了这一点

import Data.Vect

removeElem : (value: a) -> (xs: Vect (S n) a) -> (prf: Elem value xs) -> Vect n a
removeElem value (value :: ys) Here = ys
removeElem {n = Z} value (y :: []) (There later) = ?removeElem_rhs_1
removeElem {n = (S k)} value (y :: ys) (There later)
                                          = y :: removeElem value ys later

在孔上进行类型搜索的地方

  a : Type
  value: a
  y : a
  later: Elem value []
---------------------------
removeElem_rhs_1 : Vect 0 a

他解释

以前，您使用过impossible关键字来排除不进行类型检查的情况。这种情况会 进行类型检查，因此您不能使用impossible。但是，您将永远不会拥有类型Elem value []的值作为输入，因为无法构造这种类型的元素。

因此他使用absurd从要构建的输入中构建Vect 0 a

removeElem {n = Z} value (y :: []) (There later) = absurd later

我遵循这是如何完成功能的，但是我不明白他为什么说我们不能使用impossible，就好像我在later上拆分时一样，编辑器会自动填充它

removeElem {n = Z} _ (_ :: []) (There Here) impossible
removeElem {n = Z} _ (_ :: []) (There (There _)) impossible

这使我认为我认为他在无法构造的值与未进行类型检查的案例之间进行区分的重点在于表示，而不是基本内容。因此，absurd只是处理impossible案例的另一种方式。我特别想知道我的想法是否普遍适用，或者这是特例。

我对此进行了更多的思考，可以添加更多内容，但不想淹没您的笔记