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 ()

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

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)

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 ()

which produces code like this:

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

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

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:

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

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

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'

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

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'

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

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

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.

previous
overview
next