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.
Top comments (0)