Idris2+WebGL, part #7: Short code quality update

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 expression f x is linear if either f or x are linear, and as such the expression f x y is linear if either f x or y 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 interfaced HasGL and HasAllocator, with a monad Graphics 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 a
makeTriangle 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 Drawable
makeTriangle = 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.