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 sortof 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 nonlinear 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:
 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
Unfortunately I can't really make GL
a Monad
, as Monad
expects nonlinear 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 donotation 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:

requestAnimationFrame
, which has to utilizeIO ()
, 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 CPUbound.
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 catchall type %World
. It is like using "dynamic" types or matching on any errors in a catch function; it does not fit well with typesafety.
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 catchalls IO
or %World
should exist in either Prelude or Base, as I can now only consider them antipatterns.
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 FFIspecific solution.
There are also some things we currently express with IO monads that should probably not be monadic. Nondeterminism is a good example. Presuming, for the moment, that we are not relying on random tables or similar deterministic tricks to generate pseudorandoms, there is no inherent order to nondeterministic operations, so forcing it with monads works but is inaccurate.
Discussion (0)