DEV Community

DrBearhands
DrBearhands

Posted on • Originally published at drbearhands.com

Idris2+WebGL, part #6: Bye IO monad, hello GL monad

After my last project log I was left with the task of rewriting all functions to use linear types. This process wasn't very interesting, though it did give me some insights into the challenges of creating a linear type system, which I will share at the end of this log.

After the refactor, I was left with many functions of the following form:

clearColor : GLContext -> Double -> Double -> Double -> Double -> IO ()
Enter fullscreen mode Exit fullscreen mode

This sort-of works for now, because while the WebGL context might not quite be a constant, the reference to that context pretty much is. Unfortunately this also chains every function to the IO monad, since we need to establish a clear order between GL functions. If we don't, Idris would rightfully treat each function as pure and might do things in a way that breaks our program.

Working with IO monads and linear types is somewhat obnoxious. We, AFAIK, have no linear variant of pure because the IO constructors are not exported, >>= we have to redefine ourselves somewhere... it's simply non-linear by default. Plus, I find IO to be too broad as a type.

We can get rid of IO by making GLContext linear:

clearColor : (1 _ : GLContext) -> Double -> Double -> Double -> Double -> GLContext
Enter fullscreen mode Exit fullscreen mode

But this adds yet another output value to every WebGL function, adding boilerplate to all graphics code that now needs to pass the GLContext around:

foo : (1 _ : GLContext) -> (1 _ : GLProgram) -> (GLProgram, GLContext)
foo gl program =
  let
    gl = clearColor gl 0 0 0 0
    gl = clear gl
    (program, gl) = useProgram gl program
    ...
  in
    (program, gl)
Enter fullscreen mode Exit fullscreen mode

Instead, I'd like to use my own GL monad, which does not implement the HasIO interface, and have functions like this one:

clearColor : Double -> Double -> Double -> Double -> GL ()
Enter fullscreen mode Exit fullscreen mode

which produces code like this:

foo : (1 _ : GLProgram) -> GL GLProgram
foo program = do
  clearColor 0 0 0 0
  clear
  program <- useProgram program
  ...
  pure program
Enter fullscreen mode Exit fullscreen mode

I took a look at how IO is implemented in Idris (in the paper, section 2.5), as I knew it uses linear types under the hood.

-- A primitive IO action takes a (linear) world state and produces an IO Response
PrimIO : Type  -> Type
PrimIO a = (1 w : %World) -> IORes a

-- an IO Response consists of a value and a new (linear) world state
data IORes : Type -> Type where
  MkIORes : (result : a) -> (1 w : %World) -> IORes a

-- IO is just a wrapper around PrimIO
data IO : Type  -> Type where
  MkIO : (1 fn : PrimIO a) -> IO a
Enter fullscreen mode Exit fullscreen mode

So in essence, a function with type IO a is equivalent to a function with type (1 _ : %World) -> (a, %World) (although a is linear in the second case and not in the first). That's very close to what I want, with a few changes:

  • Rather than passing the entire bloody world around to draw stuff on a canvas, we will pass around only the WebGL context of that canvas element.
  • Many values in WebGL functions are linear, so I will default to linear results and linear monadic operations.

The resulting data types:

data GLRes : Type -> Type where
  MkGLRes : (1 result : a) -> (1 gl : AnyPtr) -> GLRes a

GLAction : Type -> Type
GLAction a = (1 gl : AnyPtr) -> GLRes a

export
data GL : (a : Type) -> Type where
  MkGL : (1 _ : GLAction a ) -> GL a
Enter fullscreen mode Exit fullscreen mode

Unfortunately I can't really make GL a Monad, as Monad expects non-linear types. So new linear variants of interfaces it is:

public export
interface LFunctor f where
  map : (1 m : (1 _ : a) -> b) -> (1 _ : f a) -> f b

public export
interface LFunctor f => LApplicative f where
  pure  : (1 _ : a) -> f a
  (<*>) : (1 _ : f ((1 _ : a) -> b)) -> (1 _ : f a) -> f b

public export
interface LApplicative m => LMonad m where
  (>>=)  : (1 _ : m a) -> (1 _ : (1 _ : a) -> m b) -> m b
Enter fullscreen mode Exit fullscreen mode

This works great in Idris, as do-notation is merely syntactic sugar of bind (>>=) operators, rather than requiring the type in question to be an instance of Monad.

-- LFunctor and LApplicative left out as they were not particularly interesting
export
LMonad GL where
  (>>=) (MkGL action_a) gl_b =
    MkGL $ \gl =>
      let
        MkGLRes result_a gl' = action_a gl
        MkGL action_b = gl_b result_a
      in
        action_b gl'
Enter fullscreen mode Exit fullscreen mode

Then what was left was to adapt all my functions, again, to work with the new GL monad.

Foreign functions are the same as they would be if I'd passed around the GLContext directly as a linear type:

%foreign "browser:lambda: (gl, r, g, b, a) => {gl.clearColor(r,g,b,a); return gl;}"
prim__clearColor : (1 _ : AnyPtr) -> Double -> Double -> Double -> Double -> AnyPtr
Enter fullscreen mode Exit fullscreen mode

the wrapper:

export
clearColor : Double -> Double -> Double -> Double -> GL ()
clearColor r g b a = MkGL $ \gl =>
  let
    gl' = prim__clearColor gl r g b a
  in
    MkGLRes () gl'
Enter fullscreen mode Exit fullscreen mode

Some functions are more complicated because they utilize callbacks to "return" multiple values from JavaScript, but the principle is the same: use MkGL with a function that takes gl as input and produces a GLRes, call the primitive functions somewhere in there.

I'm fairly satisfied with how code utilizing the new GL monad looks:

createShaderFromSource : WebGL2.GLShaderType -> String -> (1 _ : (1 _ : GLShader) -> GL a) -> GL a
createShaderFromSource shaderType shaderSrc p =
  createShader shaderType $ \shader => do
    shader <- shaderSource shader shaderSrc
    shader <- compileShader shader
    p shader

createShaderProgram : String -> String -> (1 _ : (1 _ : WebGL2.GLProgram) -> GL a) -> GL a
createShaderProgram vertexSrc fragmentSrc p =
  createShaderFromSource GL_VERTEX_SHADER vertexSrc $ \vs =>
    createShaderFromSource GL_FRAGMENT_SHADER fragmentSrc $ \fs =>
      createProgram $ \program => do
        (program, vs) <- attachShader program vs
        (program, fs) <- attachShader program fs
        program       <- linkProgram program
        ()            <- deleteShader vs --we need to consume the returned unit because it is linear...
        ()            <- deleteShader fs
        p program
Enter fullscreen mode Exit fullscreen mode

The main concerns I have left are about how the code currently looks:

  • requestAnimationFrame, which has to utilize IO (), because it runs a function at some point in the future rather than returning a value. We cannot "run" a linear WebGL context.
  • Bloody continuations everywhere a linear value is created. Now I think about it I need to check if I even still need them given how GL works.
  • I want ephemeral typed arrays to avoid expensive allocations. This can be done using linearity. In fact it's one of the motivations behind them. I'd like to do something similar to the GL monad, but there is no explicit resource to pass around, no "allocator" object.

I was a little concerned about the performance consequences of constructing GL and GLRes values all over the place, which isn't optimized away (yet) by Idris, but it does not appear to have any noticeable effect on performance. My guess is that either the browser's JS engine / compiler managed to implement this optimization step or performance is not yet CPU-bound.

Consequences of linear types for IO monads

As a post by Conal Elliot jokingly points out, working in the IO monad is basically equivalent to doing procedural programming, which is probably not what you're looking to do if you write e.g. Idris or Haskell.

Idris improves on the IO monad, by defining it in terms of linearity rather than black magic. In doing so it exposes IO's weakness, the usage of a catch-all type %World. It is like using "dynamic" types or matching on any errors in a catch function; it does not fit well with type-safety.

With the inclusion of linear types, it becomes much easier to let the programmer define his own resources: log output, internet connection, HD access; specifying such things is safer, and they can be combined using monad transformers or perhaps even free(r) monads. If no underlying resource to an action exists or the resource cannot be referenced directly (as with typed array allocation), a fake one can be used, an abstract data type over unit. We can effectively end our dependence on the IO monad. As such, I don't think the catch-alls IO or %World should exist in either Prelude or Base, as I can now only consider them anti-patterns.

There are some issues left to be resolved if we get rid of IO, and I'm sure I'm not aware of all of them. First, sometimes things actually just run. This is the case with the requestAnimationFrame example above. But perhaps we should class this as an FFI problem that requires an FFI-specific solution.

There are also some things we currently express with IO monads that should probably not be monadic. Non-determinism is a good example. Presuming, for the moment, that we are not relying on random tables or similar deterministic tricks to generate pseudo-randoms, there is no inherent order to non-deterministic operations, so forcing it with monads works but is inaccurate.

Discussion (0)