在同一个表达式中对不同的 Nat 变量调用 (-) 两次需要显式证明注释

Question

考虑这个定义：

h : Nat -> Nat -> Nat
h x y = case 1 `isLTE` x of
              (Yes prf)   => case 1 `isLTE` y of
                                (Yes prf') => (x - 1) * 2 + (y - 1)
                                (No contra) => ?sr_3
              (No contra) => ?h_2

虽然看起来很无辜，但它不会进行类型检查。

   |
14 |                                 (Yes prf') => (x - 1) * 2 + (y - 1)
   |                                                               ^
...
When checking an application of function Prelude.Interfaces.-:
        Type mismatch between
                Nat (Type of y)
        and
                LTE 1 x (Expected type)

由于某种原因，它无法找到正确的 prf。 （或者还有其他事情发生？） 再次出于某种原因，这个错误虽然出现在第二个被加数中，但可以通过注释第一个中的减号来修复。编译：

h : Nat -> Nat -> Nat
h x y = case 1 `isLTE` x of
              (Yes prf) => case 1 `isLTE` y of
                                (Yes prf') => ((-) {smaller = prf} x 1) * 2 + (y - 1)
                                (No contra) => ?sr_3

我的问题：

发生了什么事？
如何更好地表达这个逻辑？
我能否为中缀运算符提供隐式参数，例如 -，而不将它们转换为前缀形式 (-)？

Answer 1

What is happening?

我猜这似乎是统一中的一个错误。它应该能够正确地推断出一切，但对于系统来说，它显然不清楚你想使用哪种类型。 +、*都是Num a => a -> a -> a，-甚至有两个定义；一个带有 Nat 和证明，另一个也采用 Num 格式。因此，每当出现奇怪的类型不匹配时，只需澄清类型即可。 (x - 1) * 2 `plus` (y - 1) 也可以。

How can I express this logic better?

您可以加入两个 case 语句：

g x y = case (1 `isLTE` x, 1 `isLTE` y) of
    (Yes lte1x, Yes lte1y) => (x - 1) * 2 `plus` (y - 1)
    _ => ?h

更好的是，如果您只需要减一，只需通过模式匹配即可：

i (S x) (S y) = x * 2 + y
i x y = ?h

此外，Nat 并不总是适合计算；它更适合类型系统的结构信息（如 Vect Nat a）。如果您打算执行 x - 321 * y + 100 之类的操作并且不需要类型中的结果，出于性能原因，只需下降到 Integer。

Can I supply implicit arguments to infix operators, such as -, without converting them to prefix form (-)?

不！

在同一个表达式中对不同的 Nat 变量调用 (-) 两次需要显式证明注释

Invoking (-) two times on different Nat variables within the same expression requires explicit proof annotation

idris

我的问题：