No linearity with monadic errors (for now)

I’ve come back on the idea of implementing more monadic error handling. I wasn’t entirely convinced about the App approach proposed with the introduction of QTT in idris2; it’s not as composable as monad transformers and if I understand correctly it deals with errors in linear protocols by not allowing errors in linear protocols. On the other hand, I’m starting to think using monads is only hiding the problem behind abstractions rather than actually fixing it, and it’s come to bite us in the butt with linearity.

To recap, the problem is that with the introduction of linear types, we can no longer use monad transformers to handle errors. The type (SomeError | b) is a monad for regular b’s, but not if b is linear. Linear values must always be consumers, but sum types add uncertainty: we do not know if the inner type of a monad even exists so how do we know if we can/must consume it?

Take a look at the following code:

vsRes <- createShaderFromSource GL_VERTEX_SHADER vertexSrc
case vsRes of
  Err err => pure {m=Graphics} $ Err err
  Ok vs => LMonad.do
    fsRes <- createShaderFromSource GL_FRAGMENT_SHADER fragmentSrc
    case fsRes of
      Err err => LMonad.do
        () <- deleteShader vs
        pure {m=Graphics} $ Err err
      Ok fs => LMonad.do
        programC          <- createProgram
        programC $ \program => LMonad.do
          program # vs      <- attachShader program vs
          program # fs      <- attachShader program fs
          program           <- linkProgram program
          vs # program      <- detachShader program vs
          fs # program      <- detachShader program fs
          ()                <- deleteShader vs
          ()                <- deleteShader fs
          linkOk # program  <- getProgramLinkStatus program
          if linkOk
            then pure {m=Graphics} (Ok (\f => f program))
            else do
              log # program <- getProgramInfoLog program
              ()            <- deleteProgram program
              pure {m=Graphics} (Err $ MkLinkError log)

I would like to use a monadic style to make the happy-flow easier to read:

vs        <- createShaderFromSource GL_VERTEX_SHADER vertexSrc
fs        <- createShaderFromSource GL_FRAGMENT_SHADER fragmentSrc
programC  <- createProgram
programC $ \program => LMonad.do
  program # vs  <- attachShader program vs
  program # fs  <- attachShader program fs
  program       <- linkProgram program
  vs # program  <- detachShader program vs
  fs # program  <- detachShader program fs
  ()            <- deleteShader vs
  ()            <- deleteShader fs
  program       <- getProgramLinkStatus program |> handleLinkError
  pure {m=Graphics} $ Ok $ \f => f program

But this is wrong. The first snippet is correct. It checks for errors once, when they can appear, and handles them, including freeing resources. The second snippet unnecessarily puts the entire code in a more complex/permissive Kleisli category.

The fact that it isn’t as readable isn’t inherent to the program structure, but to how we chose to represent it as a single, unfolded, static string of characters. We could instead chose to display a single branch at a time. An IDE could display the first as:

vsRes <- createShaderFromSource GL_VERTEX_SHADER vertexSrc
-- assume vsRes = Ok vs
fsRes <- createShaderFromSource GL_FRAGMENT_SHADER fragmentSrc
-- assume fsRes = Ok fs
programC          <- createProgram
programC $ \program => LMonad.do
  program # vs      <- attachShader program vs
  program # fs      <- attachShader program fs
  program           <- linkProgram program
  vs # program      <- detachShader program vs
  fs # program      <- detachShader program fs
  ()                <- deleteShader vs
  ()                <- deleteShader fs
  linkOk # program  <- getProgramLinkStatus program
  -- assume linkOk
  pure {m=Graphics} (Ok (\f => f program))

Where we could “unfold” each assume comment into a list of cases to change which branch is shown.

It further seems that Elm is doing great without any do notation and monadic error handling. It results in very nice code and seems quite beginner-friendly. The subject matter probably has a lot to do with it though. My WebGL API in particular is based around an inherently procedural specification, so some monadic style is probably beneficial… but I’m starting to doubt even that.

Since I’m no longer sure monad transformers for error handling are such a good idea (especially in the linear case), I’m postponing the decision on if/how to use them until the code base has gotten larger, so that I have a better grip on both the problem and Idris in general.

overview