在条件语句分支中告诉依赖函数条件为真

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调用一个需要的函数,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)

这不是我们可以轻易做到的布尔人.