Effects in Idris: how to create them and a use for them to force proofs

I’ve been deep diving idris for a while, and the way certain dependently typed structures change type over time has been something I haven’t had a great handle on. I have a tutorial on the ST monad coming, but I’d like to first talk about the way (as I understand it) idris’ dependent types apply to monads which we mutate (at least conceptually) through the flow of imperative-like code.

Example: https://github.com/prozacchiwawa/idris-effect-example/blob/master/Artyssert/Assert.idr

For lack of better ways of stating it, I’m going to use the terminology used in pursecript and think of the effect list as a collection of independent row types. This probably isn’t strictly accurate (for example, it’s possible for these “rows” to have ids named by types as I understand it, unlike purescript), but the analogy holds pretty well when they aren’t noted by IDs since each row type matches an item of compatible type in the collection of rows.

With Effect, there are basically these states:

• Pre-application of our monad; there are no matching items in the rows. If no other effects are being used, the left hand list of EFFECT equals []. In any case, an EFFECT for the Effect we’re interested in hasn’t been introduced yet. One can think of “Eff () []” as the expected Effect state.
• Running of our monad; an EFFECT exists in the Eff monad’s EFFECT list that is compatible with our Effect. One can think of “Eff () [OUREFFECT Initialized]” as the expected Effect state if Initialized is the state we want to start OUREFFECT in. I’ll talk about effect states a bit later.
• Finish of our monad; an EFFECT exists in the expected end state in the Eff monad’s EFFECT list and it is provably compatible with the expected end state. This proves that we have satisfied conditions for the monad’s use.

That’s complicated, and I’ll try to explain the various parts necessary for this to function.

The form of the effects given in the idris examples have the following general outline:

• 0: An ordinary datum in ADT or record form that contains actual PoD information regarding the state the effect has been left in. It is modified in a way that I’ll explain in a bit.
• 1: A GADT Type wrapper for the above data.
• 2: An Effect ADT with elements whose type is built by the ‘sig’ function in idris’ effects package. sig takes 3 or 4 arguments and I’ll try to explain what it’s doing in a bit. Just note that the cases in this ADT represent the actions that can be taken in this Effect (everything you can order it to do) and contain expected precondition states and expected postcondition states for the Effect in terms of Types.
• 3: A GADT yielding EFFECT which is basically the same as PROCESS, CONSOLE, EXCEPTION, AFF, SIGNAL etc in purescript. It is constructed by MkEff from Effects and given a datum of our effect’s content type (0 above) combines it with the type wrapper (1 above) and the effect methods (2 above). This is the name we’ll use everywhere else to refer to our effect in the code.
• 4: A Handler implementation for (2) that carries out actual actions in a more primitive monad, such as IO. These could be FFI functions that do mutations outside idris, ST actions that modify state data or even empty actions on the universe that serve only to change the Type of the effect state.
• 5: A Default implementation for the Type that is taken on by (2) that the EFFECT starts life in. When a do block requiring one of these as a precondition is encountered and there is no active EFFECT (4) in the list maintained by Eff for the preconditions of the environment surrounding the block, the “default” method of the “Default” instance will yield a Type to be inserted into the preconditions automatically.
• 6: End user accessible functions which invoke “call” on one of the data constructors in (2).

whew!!*

After that, we’ve got an EFFECT we can use. You can write a do block in the regime of your effect.

Now I’ll explain the code in more detail. First, what was the goal of all this? I’m interested in idris as a venue for software verification and using formal proof for writing code. In particular, I was curious after my previous experiments with modelling dynamic state in monads (which, while successful, also makes for very complex proofs), I could simplify what needs to be done by requiring that imperative code containing assertions also contains proof that the assertions never fire. This take distributes proof obligations, and should make proofs more modular. I had to start by discovering how effects work in idris, since I wanted the state of the assertions to be kept track of by the type system. Since reading the ‘door’ examples and hangman examples existing for idris, an effect seemed a natural way to make idris aware of my intentions.

doTryAssert : Eff () [ASSERTION NotFailed] [ASSERTION NotFailed]
doTryAssert =
  do
    let x = True -- Not well typed if x is False
    assert x (trueEqualsTrue x)
    let y = 2 /= 3 -- Not well typed for 3 /= 3
    assert y (twoIsLessThanThree)

In my case, I was interested in modelling assertions in imperative code as an effect that always has an expected state of ASSERTION NotFailed. Therefore, if any assert can get False, the outcome state will possibly be ASSERTION Failed and the code won’t compile. Idris must believe that each assertion receives True at the call site via proof.

It can be invoked by the ugly but usable:

runAssertions : Eff () [ASSERTION NotFailed]
runAssertions = do
  doTryAssert
main : IO ()
main = run runAssertions

Figuring out the appropriate magic to set this up took a lot of time and punching compile errors. I still don’t fully understand the interplay between Default and Eff here.

So starting with (0)

data AssertionState = NotFailed | Failed

Nothing could be simpler than a piece of data we want idris to keep track of.

On to (1)

data AssertionInfo : AssertionState -> Type where
     DI : AssertionInfo s

Very usual idris code to cause each state that can be taken by AssertionState to turn into a Type we can use for Type level code.

On to (2)

data AssertionEff : Effect where
     FailAssertion : 
       sig AssertionEff () 
         (AssertionInfo NotFailed)
         (AssertionInfo Failed)
     OkAssertion : 
       sig AssertionEff ()
         (AssertionInfo NotFailed)
         (AssertionInfo NotFailed)

This sets out the methods of our effect, that is; what it can do and the pre and post-conditions of each method. Note that there is a 3-argument form of sig that does not take a precondition. I did not need to use it here. Using a function to give the type of a GADT label isn’t common in most code, but a bit of thinking indicates that any function yielding Type would be fine.

(3)

ASSERTION : AssertionState -> EFFECT
ASSERTION t = MkEff (AssertionInfo t) AssertionEff

This heavily reminds me of effect types from purescript, pre 0.12. The constructor takes a datum that we defined in (0), wraps it as (1) and throws in (2) to the MkEff constructor to give it all the info it needs. ASSERTION will appear in code our hypothetical user uses.

(4)

implementation Handler AssertionEff IO where
  handle res FailAssertion k = do
    putStrLn "Assertion failed"
    k () DI
  handle res OkAssertion k = do
    k () DI

An implementation of the Handler typeclass for AssertionEff (2) in which we take actions (in this case, writing a message when we hit a failed assertion) and also changing to a new state (k takes two arguments, the returned, “residual status” from scsi parlance, a value that is picked up by “<-” in monadic captures; a string for getline for example), and a Type that represents the state of the Effect system after this command is complete. In an audio system, this might indicate that the system is in a buffer full state and can’t take more samples, or that the buffer is below the low water mark and new samples are needed. That the video system is late for a deadline and that draw calls marked low priority will be dropped, that the bank represented by the other end of a websocket is close to overdraw and we can’t do more transactions. Anything the imagination can come up with. In our case, it just indicates whether the most recent assertion failed. To do this, we “call” the FailAssertion alternative of (2) to cause it’s effect to happen, which includes a postcondition of ASSERTION Failed. Since we’re expecting ASSERTION NotFailed, this is an impossible state and the program will not compile.

(5)

implementation Default (AssertionInfo NotFailed) where
  default = DI

This an implementation of the Default typeclass for (AssertionInfo NotFailed), in general, it will return the start state of the effect when one isn’t present in the Eff environment to begin with. If variables or arguments were present in our effect state, we’d have to supply them concretely here.

(6) finally

assert : (x : Bool) -> (prf : (x = True)) -> Eff () [ASSERTION NotFailed] [ASSERTION (if x then NotFailed else Failed)]
assert False _    = call FailAssertion
assert True  Refl = call OkAssertion

A function for each method we can use in our effect. These are normal functions that carry the actual outcome states of the effect. In my case, I gave a proof that assert False is uninhabited so we can guarantee that assert never transitions the effect to ASSERTION Failed. We leave the possibility open that some code might want to use assert in a different way, and a different method of ASSERTION might not take this proof.

So there we have a program that is well typed only if every instance of assert comes with a proof that the assertion input is True. I believe this will be a help in actually using idris for formal verification as it can be used in a really incremental way like this.