理解'不可能'

Question

使用Idris进行类型驱动开发:

twoPlusTwoNotFive : 2 + 2 = 5 -> Void
twoPlusTwoNotFive Refl impossible

以上是功能还是价值？如果它是前者,那么为什么没有变量参数,例如

add1 : Int -> Int 
add1 x = x + 1

特别是,我在缺乏困惑=在twoPlusTwoNotFive.

Answer 1

impossible调用了很多,不可能的参数组合.伊德里斯赦免了你无法在案件无法提供右手边的责任.

在这个例子中,我们正在编写一个类型的函数(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

我喜欢它,因为有时你只是在对参数做一些进一步的模式匹配后才知道一个案例是不可能的; 当不可能的东西被埋下几层时,有一个视觉辅助来帮助你找到它的位置是很好的.