Probably the worst monad example in Idris; using monads to simulate side effects
I’ve been thinking and working a lot on some code, and stealing tiny amounts of time here and there thinking about and trying out Idris with regard to helping with some real code. In this case, some Kotlin code that implements an offline BTree. It is necessary to use a side-effecting external store for this both because the size of the tree can be considered to be infinite over a long time, and also because RAM is at a bit of a premium.
I’ve written pretty good tests, so I’m confident that the code is mostly correct, and the tests have, except for a few cases I believe are impossible, full coverage of the insert methods (the only ones that modify the tree), but 2 days ago I hit an assertion failure in the code; it had slipped my mind that a certain case might not be a new insert but a reinsert which causes the newly emitted tree to have the same number of keys with a changed value. The relevant assertion failure was one that required the splitting node plus the new insert to add up to 2 * branchingFactor + 1 total pointers. The bug would only have caused a premature split of the tree and wasn’t difficult to fix, but it was a good excuse to take stock of where I am with Idris.
I have been transcribing some of the code from Kotlin to Idris in times when waiting for other things. The code thus transcribed is too awful to reference, but most of it type checks, such as it is.
I came to the point where I wanted to emulate the external database, specifically to be able to prove things about the data stored within. One obvious way is to use the State monad, which in Idris even undergoes type changes as it is modified, allowing type errors about the about simulated side effects to surface at compile time. This is really neat, but admittedly I haven’t digested the relevant documentation and examples well enough to use it yet. I did realize after watching John De Goes’ live coding exercise in functional IO here:
That it’d be possible to use a monad instance to create a function that simulates the external store. Armed with an incomplete understanding of the monad laws and basically nothing else I decided to dive in with the goal of making a function that runs a test case and then transforms a start state to and end state based on the simulated IO function it returns.
If this sounds confusing, a simple example will likely help:
module Counter{- addCounter, getCounter, counterSysRun -}
import CounterMonad
double : () -> CounterOps ()
double _ = do
ctr <- getCounter ()
addCounter ctr
pure ()make4 : () -> CounterOps ()
make4 _ = do
addCounter 1
double ()
double ()
pure ()tryit : () -> Int
tryit _ =
counterSysRun 0 make4tryitReturns4 : tryit () = 4
tryitReturns4 = Refl
In this example, I’ve made an IO system that knows about a single integer (you could imagine this simulating a system that can read and write an external register). There is only one output operation, addCounter, which takes an integer and does … something external (namely adding the new value to the counter), but also contains a getCounter function that can return the current value of the counter.
In the example, there is a double () function under the CounterOps monad that is purely side-effecting in context; it retrieves the counter value and then adds it back, always doubling the value that was present before.
The make4 function causes the start value of the counter (0) to become 4 by first adding 1, then doubling the counter value twice, all using side effects. It kind of feels a bit spooky.
This example would not work (and in fact tryitReturns4 would be ill-typed) if we weren’t building up a function that represents the operations this code does on the invisible external counter. The signatures here should be generalized, but right now they’re adequate for a test harness.
This is a pretty big win if you want Idris to force you to prove things about code with side effects, as I do.
The ugly but surprisingly general implementation
So what’s in CounterMonad anyway?
First off, with apologies for the lack of generality, the type of this monad is:
public export
data CounterOps a =
Pure a
| IOP (Int -> Int) (Int -> CounterOps a)Or simply, a value representing a simple value returned from a side-effecting function, and a value representing a side effect, whether input or output. The IOP constructor bears some explaining:
One might think of it as “IOP transform goOn” where transform is a function that updates the external state in whatever way this mutation step wants, and goOn is a function that carries any computation the user code does that depends on the previous side effects.
Some background on these type class instances: in Idris, Monad, Applicative and Functor have basically one important method each, namely (>>=), (<*>) and map, and they kind of build on each other:
public export
Functor CounterOps where
map f sysops =
case sysops of
Pure a => Pure (f a)
IOP op a => IOP op (\sys => map f (a (op (sys))))
public export
Applicative CounterOps where
pure a = Pure a
(<*>) f a =
case f of
Pure g => map g a
IOP op g => IOP op (\sys => (g (op sys)) <*> a)public export
Monad CounterOps where
(>>=) sysops f =
case sysops of
Pure a => f a
IOP op g =>
IOP
op
(\sys => g (op sys) >>= f)
In other words, map simply unwraps and rewraps Pure or applies f inside the continuation function carried with IOP, applicative does map while unwrapping the function as well, and (>>=) feeds the previous computation’s result into the next, respecting the monad type. How the monad one works was tricky to reason out, but the main thing is that we need to ensure that when an older state is fed to f in the IOP case, we need to apply whatever operation that IOP represents and let the IOP’s continuation run before feeding the result to f, thus ensuring that if g represents a read, it reads the most recent value built up of all the previous mutations through op. This assumes that there are no read/write/modify operations as I’m uncertain whether the sequencing would be right in that case, however you can always simulate such operations with distinct read and write operations, as in the case of “double” above.
Side effecting operations are required; we model them as IOP values. Here the code is more or less exactly like what John De Goes was writing. In each case, we differentiate the computation that simulates the side effect and the one that allows the overall user computation to continue. Each of the goOn functions will be layered in the end; each later one will receive the result of an earlier one. So too will the functions that simulate side effects be composed.
public export
addCounter : Int -> CounterOps ()
addCounter n =
IOP (\sys => sys + n) (\sys => Pure ())public export
getCounter : () -> CounterOps Int
getCounter _ =
IOP (\sys => sys) (\sys => Pure sys)
And finally we need an interpreter. This part was a bit scary but not too bad:
the main machinery of this is that Interp recurses, computing the side effect by repeatedly composing each IOP’s t (for transform) function on the external side effect state and eventually just throwing away any excess computation.
public export
counterSysRun : Int -> (() -> CounterOps ()) -> Int
counterSysRun sys f =
let firstRun = Pure () >>= f in
interp firstRun sys
where
interp : CounterOps a -> Int -> Int
interp v sys =
case v of
Pure a => sys
IOP t g => interp (g (t sys)) (t sys)What to take away from this perhaps
I started out wondering whether I could use Idris to be more certain that some intricate code actually works, and I feel that goal is closer, although Idris itself is still a fairly foreign language to me. In this example, I’ve run through how to make a monad that, while itself an ordinary value, allows code written in do notation to simulate side effects, which can be very valuable for writing tests. In addition, it is possible to use the full power of Idris’ prover on the result.
Ensuring that functions transforming GADTs work properly with this monad is a likely TODO so more information can be available at proof time.
