Idris的类型驱动开发提出了：
twoPlusTwoNotFive : 2 + 2 = 5 -> Void
twoPlusTwoNotFive Refl impossible
以上是函数或值吗？如果是前者，那么为什么没有可变参数，例如
add1 : Int -> Int
add1 x = x + 1
特别是，我对=in的缺乏感到困惑twoPlusTwoNotFive。
impossible调用参数组合，这是不可能的。伊德里斯（Idris）放任您在案件无法解决时提供右侧帮助的责任。
在这种情况下，我们正在编写type函数(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
我喜欢它，因为有时您仅对参数进行了进一步的模式匹配后，才发现不可能出现个案。当不可能的东西埋在几层下时，最好有一个视觉辅助工具来帮助您发现它所在的位置。
本文收集自互联网，转载请注明来源。
如有侵权，请联系[email protected] 删除。
我来说两句