idris - 为什么我不能使用匹配变量而不是变量值？

Question

这是来自 here 的示例.代码如下所示:

sum : (single : Bool) -> isSingleton single -> Nat
sum True x = x
sum False [] = 0
sum False (x :: xs) = x + sum False xs

我尝试在最后一行使用 single 而不是 False。但它失败了。我认为问题在于 sum single xs 的类型是 Nat 或 List Nat，但是 + 需要只有 Nat 操作数。但是我们在一个子句中，无论哪种方式，single 都等于 False。 idris 不应该推断吗？为什么我不能在这里使用 single？有什么原因吗？

这里是错误:

main.idr:14:23-41:
   |
14 | sum False (x :: xs) = x + (sum single xs)
   |                       ~~~~~~~~~~~~~~~~~~~
When checking right hand side of Main.sum with expected type
        Nat

When checking argument single to Main.sum:
        No such variable single

更新:看起来这里的问题是我无法直接从类型定义中访问变量。然后我尝试使用这样的隐式参数:

sum : (single : Bool) -> isSingleton single -> Nat
sum True x = x
sum False [] = 0
sum {single} False (x :: xs) = x + sum single xs

这也无济于事。也许我用错了。我也尝试过最简单的变体:

sum : (single: Bool) -> isSingleton single -> Nat
sum s list = case s of 
    True => list
    False => case list of
        [] => 0
        (x::xs) => x + (sum s xs)

但它也不编译:

   |
16 |         (x::xs) => x + (sum s xs)
   |                         ~~~~~~~~
When checking right hand side of Main.case block in case block in sum at main.idr:12:19 at main.idr:14:19-22 with expected type
        Nat

When checking an application of Main.sum:
        Type mismatch between
                List Nat (Type of xs)
        and
                isSingleton s (Expected type)

对我来说这看起来有点奇怪，因为 Idris 从一方面可以证明许多有趣和复杂的事情，而从另一方面来说，这样简单的事情是不可用的。或者我做错了。

Answer 1

与其说它不能推断出 single 的类型，还不如说 single 不在 RHS 的范围内。您可以在 LHS 上使用带有 single 的命名模式

sum : (single : Bool) -> isSingleton single -> Nat
sum True x = x
sum False [] = 0
sum single@False (x :: xs) = x + sum single xs

在这种情况下，我看不到避免命名模式的方法，只能使用

sum single (x :: xs) = x + sum single xs

因为 Idris 不会推断它是一个没有 False 的 List Nat。我明白了

  |
8 | sum single (x :: xs) = x + sum single xs
  | ~~~~~~~~~~~~~~~~~~~~
When checking left hand side of Main.sum:
When checking an application of Main.sum:
        Can't disambiguate since no name has a suitable type: 
                Prelude.List.::, Prelude.Stream.::