While writing my previous dev log I realized switching over to the GL monad might allow me to use linear types without continuations. Indeed it does.

Idris determines linearity from types in negative position, that is, inputs. The expressionf x is linear if eitherf orx are linear, and as such the expressionf x y is linear if eitherfx ory are linear etc. Using GADTs we can however specify linearity in constructor functions, which is exactly what I have done in the GL monad. This has allowed me to get rid of most continuations in favor of "regular" return values.

I'm also moving towards interfaces and MTL-like functionality, though I'm not committing until I've gathered a bit more experience with dependent type programming.
For now, I have interfacedHasGL andHasAllocator, with a monadGraphics that implements both, but no real monad transformers yet.

The combination of these changes has made the code far more readable. From:

makeTriangle : (1 _ : (1 _ : Drawable) -> GL a) -> GL amakeTriangle p =  createShaderProgram vertexShaderSource fragmentShaderSource $ \program =>    createBuffer $ \buffer =>      float32Array [ -1,-1, 1, -1, 0, 1 ] $ \triangleData => do          positionAttribLocation @@ program <- getAttribLocation program "aPosition"          scaleUniformLocation @@ program <- getUniformLocation program "xScale"          buffer <- bindBuffer GL_ARRAY_BUFFER buffer          triangleData <- bufferData GL_ARRAY_BUFFER triangleData GL_STATIC_DRAW          () <- deleteArray triangleData          p $ MkDrawable program buffer positionAttribLocation scaleUniformLocation

to what I have now:

makeTriangle : Graphics DrawablemakeTriangle = do  triangleData                      <- float32Array [ -1,-1, 1, -1, 0, 1 ]  program                           <- createShaderProgram vertexShaderSource fragmentShaderSource  buffer                            <- createBuffer  positionAttribLocation @@ program <- getAttribLocation program "aPosition"  scaleUniformLocation @@ program   <- getUniformLocation program "xScale"  buffer                            <- bindBuffer GL_ARRAY_BUFFER buffer  triangleData                      <- bufferData GL_ARRAY_BUFFER triangleData GL_STATIC_DRAW  ()                                <- deleteArray triangleData  pure $ MkDrawable program buffer positionAttribLocation scaleUniformLocation

Now, one might say that this is very close to just doing procedural programming, so why use Idris rather than C? It's true that we're essentially doing procedural programming, but we have won a lot in terms of type-safety. The WebGL / OpenGL specs are written specifically for procedural programming, so this was inevitable. When building an actual graphics engine, I might create something similar to The Elm Architecture to return to a more traditionally functional code style. For low-level-ish operations such as controlling drivers, procedural style and lots of linear types seems like the right way of doing things to me.