我如何说服伊德里斯的整体检查员我没有使用变量？

Question

我一直无法说服Idris整体检查器我的功能是完全的.这是我遇到的问题的简单示例版本.假设我们有一个非常简单的以下形式的表达式:

data SimpleType = Prop | Fn SimpleType SimpleType

data Expr : SimpleType -> Type where
  Var : String -> Expr type
  Lam : String -> Expr rng -> Expr (Fn dom rng)
  App : Expr (Fn dom rng) -> Expr dom -> Expr rng

我想写这个函数

total sub : {a, b : SimpleType} -> String -> Expr a -> Expr b -> Expr b

这将需要一个DecEq实例,SimpleType但没有太多花哨.问题是如何说服类型检查器函数是完全的.例如,考虑实施sub如下:

total sub : {a, b : SimpleType} -> String -> Expr a -> Expr b -> Expr b
sub name repl (App l r) = App (substitute name repl l) (substitute name repl r)
sub _ _ expr = expr

(这是不正确的,但是一个好的起点.)这会产生错误:

Main.sub is possibly not total due to: repl

乍一看,似乎伊德里斯在验证l和r在结构上小于(App lr)时遇到了麻烦.也许下面会有用吗？

total sub : {a, b : SimpleType} -> String -> Expr a -> Expr b -> Expr b
sub name repl expr@(App l r) = App
  (sub name repl (assert_smaller expr l))
  (sub name repl (assert_smaller expr r))
sub _ _ expr = expr

不!

Main.sub is possibly not total due to: repl

事实上,在进一步调查中,据透露,虽然该计划编制:

total sub : {a, b : SimpleType} -> String -> Expr a -> Expr b -> Expr b
sub _ _ expr = expr

这一个没有!

total sub : {a, b : SimpleType} -> String -> Expr a -> Expr b -> Expr b
sub _ repl expr = expr

而现在我不知道如何说服伊德里斯,在最后一个例子中,repl真的不会干扰整体性.有谁知道如何使这项工作？

Answer 1

这在整体检查器中是一个错误,它认为你在左侧引用的'repl'是在库中定义的用于制作简单交互循环的那个.它显然不是 - 它只是名称查找中的一个错误 - 解决这个问题很简单.

这在git master中得到修复,因此将在下一个版本中修复.与此同时,使用与'repl'不同的名称将起作用(我意识到这有点烦人,但你去......)