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:
<- createShaderFromSource GL_VERTEX_SHADER vertexSrc
vsRes case vsRes of
Err err => pure {m=Graphics} $ Err err
Ok vs => LMonad.do
<- createShaderFromSource GL_FRAGMENT_SHADER fragmentSrc
fsRes case fsRes of
Err err => LMonad.do
<- deleteShader vs
() =Graphics} $ Err err
pure {mOk fs => LMonad.do
<- createProgram
programC $ \program => LMonad.do
programC # vs <- attachShader program vs
program # fs <- attachShader program fs
program <- linkProgram program
program # program <- detachShader program vs
vs # program <- detachShader program fs
fs <- deleteShader vs
() <- deleteShader fs
() # program <- getProgramLinkStatus program
linkOk if linkOk
then pure {m=Graphics} (Ok (\f => f program))
else do
# program <- getProgramInfoLog program
log <- deleteProgram program
() =Graphics} (Err $ MkLinkError log) pure {m
I would like to use a monadic style to make the happy-flow easier to read:
<- createShaderFromSource GL_VERTEX_SHADER vertexSrc
vs <- createShaderFromSource GL_FRAGMENT_SHADER fragmentSrc
fs <- createProgram
programC $ \program => LMonad.do
programC # vs <- attachShader program vs
program # fs <- attachShader program fs
program <- linkProgram program
program # program <- detachShader program vs
vs # program <- detachShader program fs
fs <- deleteShader vs
() <- deleteShader fs
() <- getProgramLinkStatus program |> handleLinkError
program =Graphics} $ Ok $ \f => f program pure {m
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:
<- createShaderFromSource GL_VERTEX_SHADER vertexSrc
vsRes -- assume vsRes = Ok vs
<- createShaderFromSource GL_FRAGMENT_SHADER fragmentSrc
fsRes -- assume fsRes = Ok fs
<- createProgram
programC $ \program => LMonad.do
programC # vs <- attachShader program vs
program # fs <- attachShader program fs
program <- linkProgram program
program # program <- detachShader program vs
vs # program <- detachShader program fs
fs <- deleteShader vs
() <- deleteShader fs
() # program <- getProgramLinkStatus program
linkOk -- assume linkOk
=Graphics} (Ok (\f => f program)) pure {m
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.