Idris2+WebGL, part #6: Bye IO monad, hello GL monad
Tags: idris, functional, linearity, qtt
Published: 2021-01-24 12:08:06

---
title: Idris2+WebGL, part #6: Bye IO monad, hello GL monad
published: true
series: Idris2 and WebGL
tags: #Idris, #functional, #linearity, #QTT
canonical_url: https://drbearhands.com/idris-webgl/part6/
---

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:

```Idris
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:

```Idris
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:


```Idris
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:

```Idris
clearColor : Double -> Double -> Double -> Double -> GL ()
```

which produces code like this:

```Idris
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](https://www.type-driven.org.uk/edwinb/papers/idris2.pdf), section 2.5), as I knew it uses linear types under the hood.

```Idris
-- 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:

- 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:

```Idris
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:

```Idris
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`.

```Idris
-- 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:

```Idris
%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:

```Idris
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:

```Idris
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:

- `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](http://conal.net/blog/posts/the-c-language-is-purely-functional) 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.