Troubles with linearity

One of the features that got me interested in Idris is its support for linear types. Much like the constant types follow “regular” logic to prove that things are computable, linear types follow linear logic to prove that resources are managed correctly. This like ensuring allocated memory is freed (without relying on garbage collection), connections are closed, etc.

I’ve actually encountered this as a real issue in WebGL development. In many early WebGL tutorials and examples, created shaders were never deleted. For a while, Apple didn’t even properly support the operation, forcing us to potentially create a memory leak, even though the garbage collector would probably catch it (as a side note: Apple has been terrible when it comes to WebGL support in general and I will never willingly support their OS ever again). JS has garbage collection, so it’s probably not a big issue there, but cross-compiling between C++/OpenGL and JS/WebGL is a thing that happens.

What programmers were supposed to do was something like this:


function shaderProgramFromSource(gl, vSrc, fSrc) {
  function shaderFromSource(shaderType, shaderSrc) {
    var shader = gl.createShader(shaderType);
    gl.shaderSource(shader, shaderSrc);
    gl.compileShader(shader);
    // pretend we're doing some error checking here
    return shader;
  }
  var vs = shaderFromSource(gl.VERTEX_SHADER, vSrc);
  var fs = shaderFromSource(gl.FRAGMENT_SHADER, fSrc);
  var program = gl.createProgram();
  gl.attachShader(program, vs);
  gl.attachShader(program, fs);
  gl.linkProgram(program);
  // pretend we're doing some error checking here

  //the following 4 lines were often missing:
  gl.detachShader(program, vs);
  gl.detachShader(program, fs);
  gl.deleteShader(vs);
  gl.deleteShader(fs);

  return program;
}

By the spec, after the program is linked, it is just supposed to work, referencing its own compiled code independently from any shaders. So shaders should / could be detached and destroyed.

In my own type-safe WebGL bindings I want to express this using linear types. A linear value has to be consumed exactly once. We can use this to safely “modify” a value, by consuming it and producing a new, slightly different, linear value.

For shaders, this means the createShader function should produce a linear shader type, and deleteShader should consume a linear shader type, whereas shaderSource, compileShader, attachShader, and detachShader should do both. There’s some other shader-related function that I will ignore for now.

Unfortunately, I have, after investing 3 mornings into it, been unable to express linearity in Idris in a useful way. This might quite possibly be due to a lack of understanding on my part. I have not yet read the paper on quantitative type theory. However, I’m fairly confident in stating that with the current state of the documentation, using multiplicity 1 (linear) types in Idris is not a realistic goal for most software-development companies. This old xkcd comic on Haskell seems somewhat applicable…

So what is the issue?

Idris expresses linearity in its functions, not my preference, as I believe data is inherently either knowledge or a resource, but not a huge issue. This is how we’d define it:

compileShader_linear : GLContext -> (1 _ : GLShader) -> GLShader

This function takes a constant GLContext, consumes a linear GLShader and produces… a constant GLShader? Nope, the output is a linear type too. I find this notation confusing and am not sure how/why the result it determined to be linear. I expect this lack of understanding lies at the basis for all my troubles, but let’s move on…

The new definition of compileShader_linear requires us to also return a GLShader so I need to add some further inefficiencies in the FFI:

%foreign "browser:lambda: (gl, shader) => {gl.compileShader(shader); return shader;}"
prim__compileShader_linear : AnyPtr -> (1 _ : AnyPtr) -> AnyPtr

This is slightly annoying but not a huge deal. Not yet anyway.

Now for another part that I find somewhat obnoxious but probably has a good reason for being the way it is; creating a linear type:

createShader_linear : GLContext -> GLShaderType -> (1 _ : (1 _ : GLShader) -> IO a) -> IO a

Since Idris can define inputs as linear but not outputs, we must instead resort to using the input of an input. Rather than specifying something in the positive position (an output), we specify it in the negative position (input) of a negative position, making it positive again. This might be a fine mathematical property but it’s a pain to work with. It does not properly express most developers’ thought process: we want to create a thing, not read a function that creates something. Even though the two are technically somewhat the same, it ads additional mental load. The point of adding type-level clarity is, in my opinion, avoiding mental load.

You may also have noticed the use of IO rather than HasIO io. That’s because we now have to pass a callback to a primitive function.

deleting shaders is probably the most straightforward aspect:

deleteShader_linear : HasIO io => GLContext -> (1 shader : GLShader) -> io ()

So far, things at least appear to work, but it’s at putting everything together where I got well and truly stuck:

createShaderProgram : WebGL2.GLContext -> String -> String -> IO WebGL2.GLProgram
createShaderProgram gl vertexSrc fragmentSrc =
  createShader_linear gl WebGL2.GL_VERTEX_SHADER $ \vertexShader =>
    let vertexShader' = shaderSource_linear gl vertexShader vertexSrc
        vertexShader'' = compileShader_linear gl vertexShader' in
      do
        fragmentShader <- createShaderFromSource gl WebGL2.GL_FRAGMENT_SHADER fragmentSrc
        program <- WebGL2.createProgram gl
        WebGL2.attachShader_linear gl program vertexShader''
        WebGL2.attachShader gl program fragmentShader
        WebGL2.linkProgram gl program
        deleteShaderLinear vertexShader''
        errorMsg <- WebGL2.getProgramInfoLog gl program
        consoleLog errorMsg
        pure program

which gives the error:

main.idr:55:47--55:61:While processing right hand side of createShaderProgram at main.idr:47:1--66:1:
Trying to use linear name vertexShader'' in non-linear context at:
55          WebGL2.attachShader_linear gl program vertexShader''
                                                  ^^^^^^^^^^^^^^

Warning: compiling hole Main.createShaderProgram
Uncaught error: INTERNAL ERROR: (CRASH "Encountered undefined name Main.createShaderProgram")

Obviously I did some naughty things like using constant and linear shader functions mixed together, but that does not appear to be where the compiler’s problem lies. Linear types and do blocks don’t seem to play nice together. I think it has something to do with the resulting IO WebGL2.GLProgram not being linear, putting us at risk of running the same IO x multiple times even though the linear resources were consumed, but have ultimately no clue how to solve this issue.

What I’d like, maybe

I think a few changes may be in order to make linear types more accessible. That said, many of these ideas are likely a result of some form of misunderstanding or oversight on my part, so take them as nothing more than the naive first instincts of a frustrated developer, which is what they are.

First, I think it would be good to have linearity notation in positive positions. It would do a lot to clarify intention, even if there is a very good reason for making positive positions linear based on negative positions.

Second, I don’t think (1 _ : A) -> A is a good way of expressing resource mutation in non-trivial cases even with explicit linearity in positive positions. Consider attaching shaders. Currently I’ve only attempted to use linearity on shaders, but it makes sense to use it on programs too, and perhaps the gl context, though I’m more inclined to using a monad for that one. This would quickly add boilerplate, as all input types would have to be returned in a tuple:

attachShader_linear : (1 _ : GLContext) -> (1 _ : GLProgram) -> (1 _ : GLShader) -> (GLContext, GLProgram, GLShader)

This is verbose, but also detached from what a programmer’s though process is like. We’re not producing new values here, just reading or modifying existing ones. I find what glsl does more elegant:

void attachShader(in GLContext gl, inout GLProgram program, in GLShader shader)

by specifying types as in, out, or inout, much of the same resource management information can be expressed without having to resort to the verbosity of tuples. Of course this would have to be extended with a variant of in, e.g. consumed, to specify that a resource is deleted:

void deleteShader(in GLContext gl, consumed GLShader shader)

We’re getting closer to separation logic here, which can also help us (or ideally the compiler) better identify how code could be parallelized.

Third, I’d also like linear types to play nicer with monads. Linear types might be, in part, a replacement for monads, but not fully, and I expect the two will have to be used together quite a bit. For instance, it would be incorrect to express a GLContext as a linear type, it should be a monad, since a context loss can occur at any time and beyond the control of our program, therefore we truly do operate in a Kleisli category, and don’t just use monads as a hack solution to express mutation. However, I don’t understand the problem going on here well enough to say much.

Finally, some polymorphism between linear and constant types would be welcome. Consider the following bit of code I’m using:

public export
interface JSNative a where
  asAnyPtr : a -> AnyPtr

export
unwrap2AnyPtrs : JSNative a => JSNative b =>
  (AnyPtr -> AnyPtr -> x) -> a -> b -> x
unwrap2AnyPtrs fun v1 v2 = fun (asAnyPtr v1) (asAnyPtr v2)

This is a great help in reducing code boilerplate for the various wrappers around AnyPtr when calling foreign functions. It allows me to specify functions like this:

export
uniform1fv : HasIO io => GLContext -> WebGLUniformLocation -> Float32Array -> Int -> Int -> io ()
uniform1fv gl location srcData offset length =
  primIO $ (unwrap3AnyPtrs prim__uniform1fv) gl location srcData offset length

However, these helper functions expect all arguments to be constant. Making them for each combination of linear and constant arguments seems excessive.

Now what?

I think I will let my adventures in linearly-typed land stew for a bit longer and focus on something else. Then, after a cool-off period, go to the literature and see if that helps.

previous
overview
next