为什么这些声明（针对相同的模式）满足类型检查器的要求？

Question

我正在跟随令人惊叹的 TDDwI，写一个简单的 removeElem。

关于它的四个问题：

为什么我可以为同一个模式写 3 个声明？
absurd和impossible有什么区别？
在第三种情况下 returns [], [] 是一个值，因此...证明 xs 有一个 a 删除，然后...对吗？
如果我删除所有 3 个，功能仍然是完整的，而且我有一种莫名的痒痒，感觉有些奇怪的事情正在发生。？。（我认为这是一个问题）

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) = absurd later -- ??
removeElem {n = Z} value (y :: []) (There later) impossible     -- ??
removeElem {n = Z} value (y :: []) (There later) = []           -- ??
removeElem {n = (S k)} value (y :: ys) (There later) = 
  y :: removeElem value ys later

Answer 1

这种情况是不可能的，所以无论你做什么都无所谓。如果一等于二，那么月亮是奶酪做的是一个正确的陈述，因为一不等于二。 absurd 是类型 Uninhabited t => t -> a 的函数。伊德里斯知道这种情况是不可能的，所以你不必处理它。

你甚至可以 return 字符串 "Hi" 通过证明 Vect 0 a = String

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) = absurd later -- ??
removeElem {n = Z} value (y :: []) (There later) impossible     -- ??
removeElem {a} {n = Z} value (y :: []) (There later) = rewrite (the (Vect 0 a = String) (absurd later)) in "Hi"           -- ??
removeElem {n = (S k)} value (y :: ys) (There later) = y :: removeElem value ys later

Answer 2

why can I write 3 declarations for the same pattern?

因为在这种情况下 (y :: []) 您正在处理单元素向量。这意味着 later 的类型为 Elem value []，即空列表中有一个元素 value，即 absurd。回想一下 absurd 的类型 Uninhabited t => t -> a，读作 "if a type t is uninhabited and you have an inhabitant of that type, then you can construct an inhabitant of an arbitrary type a"。因此，您只需要 Elem x [] 来实现该接口（它是 here）。这就是 absurd later 起作用的原因。

impossible 有效是因为 Idris 能够自行执行上述所有推理。

what's the difference between absurd and impossible?

impossible关键字可以用来排除不进行类型检查的情况，而absurd只是一个引理，所以如果你使用它，所有的东西都必须进行类型检查。

in that 3rd case that returns [], [] is a value, therefore... proof that xs had an a to remove, and did... right?

是的，这是正确的。 removeElem 取一个值，一个正长度的向量，该值属于该向量的证明，return 是一个长度减一的向量。如果采用单元素向量，则可以忽略值和证明并立即 return 空向量。我的意思是你不必使用证明，它给了你额外的保证，但你可以随意忽略它们。

if I remove all 3 of them, the function is still total, and I have an inexplicable tickle that something weird's going on

一切都很好，函数仍然有效 -- Idris 让您可以忽略不可能的情况：

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

为什么这些声明（针对相同的模式）满足类型检查器的要求？

Why do these declarations (for the same pattern) satisfy the type checker?

types

idris

proof-of-correctness