idris - 我如何说服 Idris 中的总体检查器我没有使用变量？

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

乍一看， idris 似乎无法验证 l 和 r 在结构上小于 (App l r)。也许以下会起作用？

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

现在我不知道如何说服 idris ，在最后一个例子中， repl真的不会干扰整体。有谁知道如何使这项工作？

Answer 1

结果证明这是总体检查器中的一个错误，它认为您在左侧所指的“repl”是库中定义的用于制作简单交互式循环的那个。显然不是 - 这只是名称查找中的一个错误 - 解决这个问题很简单。

这在 git master 中已修复，因此将在下一个版本中修复。同时，使用与 'repl' 不同的名称也可以(我意识到这有点烦人，但是你去......)