Type error in an Idris exercise

Question

There's an Idris exercise where the task is to extend a stack calculator program from supporting just addition to also supporting subtraction and multiplication. I tried to complete it by generalizing the functions that operate on the stack. However, I'm hit with a type error between my two central functions:

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 is supposed to take a binary function and generate a sequence of actions that would apply it to that stack, while tryOp takes in such a sequence of actions and integrates it into the the IO sequence.

The error is the following:

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

The functions are called like this:

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

And that results in an error as well:

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

The error messages seem simple enough to understand, but I don't know how to approach fixing them.

Additionally this is how StackIO and bind are defined:

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

xash xash · Accepted Answer · 2018-07-31T19:06:30

Your doOp has the implicit argument height. So doOp (+) {height=5} and doOp (+) {height=10} are different StackCmds, even if the result is the same. That leads to a problem here:

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

h and height can be different. You could have a StackCmd that only operates on a stack with height = 10, while hinit has h = 5. Things you can do: change tryOp to tryOp : StackCmd () (S (S height)) (S height) -> StackIO (S (S height)). This is then a function that will always succeed.

This might have not the intended functionality, as tryOp seems to mean that it can fail. If this is the case, you have to check 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"
                     …

The Just Add => tryOp (doOp (+)) part has most likely the same problem; in the context there is not enough information on how big the stack currently is. If you need further help, you need to provide all the definitions.

All of the three parts will then need different StackCmds for all possible stack sizes. This is not really a problem, but a nicer (I think) but bit more complicated (as you might need to apply some algebra rules) solution would lift the variable height from StackCmd. Then the arguments are only the difference in the stack size after applying the operation:

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"
                           …

with

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

Type error in an Idris exercise

1 Answers