Idris2+WebGL, part #17: A Hoare state failure

As explained in the last log entry, I set out to use decorated state monads to prove certain properties of a program.

Since I have once already, somewhat unsuccesfully, used indexed monads in Haskell, I decided to aim big and tackle Hoare state monads. I've changed a few details since writing that article, such as adding a >> operator and replacing my custom exists function with a standard dependent pair (both are existential quantification, but the latter has nicer syntactic sugar).
While I did manage to get Hoare state monads working in Idris, I found their use rather frustrating. The main problem is that the type checker is strugling to find proofs, requiring manual proofs from the programmer. What's more, vague error messages in Idris 2 and the unability to put holes in some places makes the job substantially harder.

For example, consider the following code:

init0 : HoareStateMonad Nat Top () (\_, _, s => s = 0)
init0 = MkHSMonad $ \_ => MkPostS () 0

increment : HoareStateMonad Nat Top () (\s1, _, s2 => s2 = s1 + 1)
increment = MkHSMonad $ \s => MkPostS () (s + 1)

init1 : HoareStateMonad Nat Top () (\_, _, s => s = 1)
init1 = init0 >> increment

Remember that HoareStateMonad s pre a post considers a state s, a precondition pre : s -> Type over an input state of type s, a return-type a and a postcondition post : s -> a -> s -> Type over input state, return type, and output state.

As such, init0 changes the state of a Nat, works for any input state (Top holds for any value), returns a unit, and guarantees that the output state is 0. Similarly, the increment function guarantees that the output state is the input state + 1. It is obvious to a human that the postcondition of init1, which first sets the state to 0 and then adds 1 to it, is that the output state is 1.

For the typechecker, this is a little harder. First is the simple issue of how the bind (>>=) operation has been defined, the type signatures end in:

HoareStateMonad s p1 a q1
-> ((x : a) -> HoareStateMonad s (p2 x) b (q2 x))
-> HoareStateMonad s (bind_pre p1 q1 p2) b (bind_post q1 q2)

so idris excepts the resulting postconditions to be bind_post q1 q2, which specifically results in

(x : a ** (s2 : s ** (q1 s1 x s2, q2 x s2 y s3)))

and not any arbitrary thing that can be derived from bind_post q1 q2. In our case, the typechecker will conclude:

(x : a ** (s2 : s ** (s2 = 0, s3 = s2 + 1)))

rather than

s3 = 1

Nevertheless, since we can prove the latter from the former, we want the typechecker to accept this. A similar, but contravariant rather than covariant, situation occurs for the precondition.

So I've experimented with a simplify function:

simplify : {0 s : Type} 
        -> {0 a : Type}
        -> {0 preA : s -> Type}
        -> {0 preB : s -> Type}
        -> {auto 0 fPre : {s1 : s} -> preB s1 -> preA s1}
        -> {0 postA : s -> a -> s -> Type} 
        -> {0 postB : s -> a -> s -> Type} 
        -> {auto 0 fPost : {s1 : s} -> {x : a} -> {s2 : s} -> postA s1 x s2 -> postB s1 x s2} 
        -> HoareStateMonad s preA a postA
        -> HoareStateMonad s preB a postB

I can use this explicitely:

init1 : HoareStateMonad Nat Top () (\_, _, s => s = S Z)
init1 = simplify {fPost=fPost} $ init0 >> increment
  where
    fPost : {s2 : Nat} 
          -> (((e1 : () ** (e2 : Nat ** (e2 = Z, s2 = S e2)))))
          -> (s2 = S Z)
    fPost (() ** (e2 ** (p1, p2))) = replace {p = \e => s2 = S e} p1 p2

but this is not a particularly easy task. Expecting programmers to provide these proofs all throughout the code base is not realistic. I have not found a way to derive them automatically (although I believe it could theoretically be done).

This, for now, concludes my forray into Hoare state monad. The conclusion being that it is too cumbersome in the current state of Idris 2. Perhaps language updates will change things. If you want to mess with it yourself you can get the code in the hoare-state branch of my idris-linear repository (there is no actual linear variant of the Hoare state monad yet), and in particular the latest commit at the time of writing in that branch.