对同一表达式中的不同 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

发生了什么？

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

如何更好地表达这个逻辑？

您可以合并两个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。

我能否在不将它们转换为前缀形式 (-) 的情况下为中缀运算符（例如 -）提供隐式参数？

不！