Idris 练习中的类型错误

Question

有一个 Idris 练习，其中的任务是将堆栈计算器程序从仅支持加法扩展到还支持减法和乘法。我试图通过概括在堆栈上操作的函数来完成它。但是，我遇到了两个中心函数之间的类型错误：

doOp : (Integer -> Integer -> Integer) ->
       StackCmd () (S (S height)) (S height)
doOp f = do val1 <- Pop
            val2 <- Pop
            Push (f val1 val2)

tryOp : StackCmd () (S (S height)) (S height) ->
        StackIO hinit
tryOp cmd {hinit = (S (S h))}
    = do cmd
         result <- Top
         PutStr (show result ++ "\n")
         stackCalc

doOp 应该采用二进制函数并生成一系列将其应用于该堆栈的操作，而 tryOp 接受这样的一系列操作并将其集成到IO序列。

错误如下：

When checking an application of function Main.StackDo.>>=:
        Type mismatch between
                StackCmd () (S (S height)) (S height) (Type of cmd)
        and
                StackCmd () (S (S h)) (S height) (Expected type)

        Specifically:
                Type mismatch between
                        height
                and
                        h

函数是这样调用的：

Just Add => tryOp (doOp (+))
Just Subtract => tryOp (doOp (-))
Just Multiply => tryOp (doOp (*))

这也会导致错误：

Can't infer argument height to tryOp, Can't infer argument height to doOp

错误信息看起来简单易懂，但我不知道如何修复它们。

此外，StackIO 和绑定是这样定义的：

data StackIO : Nat -> Type where
  Do : StackCmd a height1 height2 ->
       (a -> Inf (StackIO height2)) -> StackIO height1

namespace StackDo
  (>>=) : StackCmd a height1 height2 ->
       (a -> Inf (StackIO height2)) -> StackIO height1
  (>>=) = Do

Answer 1

您的 doOp 具有隐式参数 height。所以doOp (+) {height=5}和doOp (+) {height=10}是不同的StackCmd，即使结果一样。这导致这里出现问题：

tryOp : StackCmd () (S (S height)) (S height) ->
        StackIO hinit
tryOp cmd {hinit = (S (S h))}

h 和 height 可以不同。您可以有一个 StackCmd 仅在具有 height = 10 的堆栈上运行，而 hinit 具有 h = 5。您可以做的事情：将 tryOp 更改为 tryOp : StackCmd () (S (S height)) (S height) -> StackIO (S (S height))。这就是一个永远成功的函数。

这可能没有预期的功能，因为 tryOp 似乎意味着它可能会失败。如果是这种情况，您必须检查 decEq h height.

tryOp : StackCmd () (S (S height)) (S height) ->
        StackIO hinit
tryOp cmd {height} {hinit = (S (S h))} with (decEq h height)
    | Yes Refl = do cmd
                    …
    | No contra = do PutStr "Not enough values on stack"
                     …

Just Add => tryOp (doOp (+))部分很可能有同样的问题；在上下文中，关于堆栈当前有多大的信息不足。如果您需要进一步的帮助，您需要提供所有的定义。

所有这三个部分将需要不同的 StackCmds 用于所有可能的堆栈大小。这不是真正的问题，但更好（我认为）但更复杂（因为您可能需要应用一些代数规则）的解决方案会将变量 height 从 StackCmd 提升。然后参数只是应用操作后堆栈大小的差异：

doOp : (Integer -> Integer -> Integer) ->
       StackCmd () 2 1
doOp f = do val1 <- Pop
            val2 <- Pop
            Push (f val1 val2)

tryOp : StackCmd () 2 1 ->
        StackIO hinit
tryOp cmd {hinit = S (S n)} = do cmd
                                 …
tryOp cmd {hinit = m} = do PutStr "Not enough values on stack"
                           …

与

data StackIO : Nat -> Type where
  Do : StackCmd a prev next ->
       (a -> Inf (StackIO (next + height))) -> StackIO (prev + height)

namespace StackDo
  (>>=) : StackCmd a prev next ->
       (a -> Inf (StackIO (next + height))) -> StackIO (prev + height)
  (>>=) = Do

Idris 练习中的类型错误

Type error in an Idris exercise

idris

dependent-type