dependent-type - 了解“不可能”

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

我喜欢它，因为有时您仅在对参数进行了一些模式匹配之后才了解到不可能出现个案。当不可能的东西埋在几层下时，最好有一个视觉辅助工具来帮助您发现它所在的位置。