idris - 告诉条件语句分支中的依赖函数条件为真

Question

我有一个带有类型签名的函数(x, y : SomeType) -> (cond x y) = True -> SomeType。当我检查 if-then-else/case/with 语句中的条件时，如何将条件为真这一事实传递给相应分支中的函数？

Answer 1

您可以使用它DecEq来简化此操作：

add : (x, y : Nat) -> x + y < 10 = True -> Nat
add x y _ = x + y

main : IO ()
main =
  let x = S Z
  in let y = Z
  in case decEq (x + y < 10) True of
          Yes prf => print (add x y prf)
          No _ => putStrLn "x + y is not less than 10"

但你不应该。

使用布尔值（通过=或So）可以告诉你某事是真的，但不能告诉你为什么。如果您想将证明组合在一起或将它们分开，那么为什么非常重要。想象一下，如果add调用一个需要的函数x + y < 20——我们不能仅仅通过我们的证明，x + y < 10 = True因为 Idris 对操作一无所知，只是它是真的。

相反，您应该使用包含其正确性的数据类型来编写上述内容。LTE是一种用于小于比较的类型：

add : (x, y : Nat) -> LTE (x + y) 10 -> Nat
add x y _ = x + y

main : IO ()
main =
  let x = S Z
  in let y = Z
  in case isLTE (x + y) 10 of
          Yes prf => print (add x y prf)
          No _ => putStrLn "x + y is not less than 10"

现在，如果add调用需要 a 的函数，LTE (x + y) 20我们可以编写一个函数来扩大约束：

widen : a `LTE` b -> (c : Nat) -> a `LTE` (b + c)
widen LTEZero c = LTEZero
widen (LTESucc x) c = LTESucc (widen x c)

这不是我们可以用布尔值轻松完成的事情。