了解 'impossible'
Understanding 'impossible'
Type-Driven Development with Idris 礼物：
twoPlusTwoNotFive : 2 + 2 = 5 -> Void
twoPlusTwoNotFive Refl impossible
以上是函数还是值？如果是前者，那为什么没有可变参数，例如
add1 : Int -> Int
add1 x = x + 1
特别是，我对 twoPlusTwoNotFive 中缺少 = 感到困惑。
impossible 调用了不可能的参数组合。 Idris 免除了您在不可能的情况下提供右侧的责任。
在本例中，我们正在编写一个 (2 + 2 = 5) -> Void 类型的函数。 Void 是一个没有值的类型，所以如果我们成功地实现了这样一个函数，我们应该预料到它的所有情况都是不可能的。现在，= 只有一个构造函数（Refl : x = x），它不能在这里使用，因为它要求 = 的参数在定义上是相等的——它们必须是 一样x。所以，自然是impossible。任何人都无法在运行时成功调用此函数，而且我们不必证明某些不正确的事情，这本来是一个很大的问题。
这是另一个例子：你不能索引一个空向量。仔细检查 Vect 并发现它是 [] 告诉我们 n ~ Z；由于 Fin n 是小于 n 的自然数类型，因此调用者无法使用任何值来填充第二个参数。
at : Vect n a -> Fin n -> a
at [] FZ impossible
at [] (FS i) impossible
at (x::xs) FZ = x
at (x::xs) (FS i) = at xs i
很多时候你可以完全忽略不可能的情况。
对于相同的概念，我稍微更喜欢 Agda 的表示法，它使用符号 () 来明确指出输入表达式的哪一位是不可能的。
twoPlusTwoNotFive : (2 + 2 ≡ 5) -> ⊥
twoPlusTwoNotFive () -- again, no RHS
at : forall {n}{A : Set} -> Vec A n -> Fin n -> A
at [] ()
at (x ∷ xs) zero = x
at (x ∷ xs) (suc i) = at xs i
我喜欢它，因为有时你只会在对参数进行进一步的模式匹配后才知道一个案例是不可能的；当不可能的东西被埋在几层下面时，有一个视觉辅助工具可以帮助你找到它的位置是很好的。
Type-Driven Development with Idris 礼物：
twoPlusTwoNotFive : 2 + 2 = 5 -> Void
twoPlusTwoNotFive Refl impossible
以上是函数还是值？如果是前者，那为什么没有可变参数，例如
add1 : Int -> Int
add1 x = x + 1
特别是，我对 twoPlusTwoNotFive 中缺少 = 感到困惑。
impossible 调用了不可能的参数组合。 Idris 免除了您在不可能的情况下提供右侧的责任。
在本例中，我们正在编写一个 (2 + 2 = 5) -> Void 类型的函数。 Void 是一个没有值的类型，所以如果我们成功地实现了这样一个函数，我们应该预料到它的所有情况都是不可能的。现在，= 只有一个构造函数（Refl : x = x），它不能在这里使用，因为它要求 = 的参数在定义上是相等的——它们必须是 一样x。所以，自然是impossible。任何人都无法在运行时成功调用此函数，而且我们不必证明某些不正确的事情，这本来是一个很大的问题。
这是另一个例子：你不能索引一个空向量。仔细检查 Vect 并发现它是 [] 告诉我们 n ~ Z；由于 Fin n 是小于 n 的自然数类型，因此调用者无法使用任何值来填充第二个参数。
at : Vect n a -> Fin n -> a
at [] FZ impossible
at [] (FS i) impossible
at (x::xs) FZ = x
at (x::xs) (FS i) = at xs i
很多时候你可以完全忽略不可能的情况。
对于相同的概念，我稍微更喜欢 Agda 的表示法，它使用符号 () 来明确指出输入表达式的哪一位是不可能的。
twoPlusTwoNotFive : (2 + 2 ≡ 5) -> ⊥
twoPlusTwoNotFive () -- again, no RHS
at : forall {n}{A : Set} -> Vec A n -> Fin n -> A
at [] ()
at (x ∷ xs) zero = x
at (x ∷ xs) (suc i) = at xs i
我喜欢它，因为有时你只会在对参数进行进一步的模式匹配后才知道一个案例是不可能的；当不可能的东西被埋在几层下面时，有一个视觉辅助工具可以帮助你找到它的位置是很好的。