Idris2+WebGL, part #11: 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.