Slow and frustrating progress

Progress since my last dev log has been rather frustrating. There are a few nasty roadblocks on the marriage between Idris and WebGL that I’m not sure are really surmountable.

First, there’s my never ending battle with Idris’s limited FFI. I’ve complained about it way back in my first dev log entry and it still bugs me. In short: the supported types are limited but still biased and dealing with linear values in FFI is unnecessarily complex. However, I have managed to improve things a bit, just not as much as I would like.

Rather than using AnyPtr in every FFI and using an abstract data type with hidden constructor I use aliases for AnyPtr:

export
WebGLRenderingContext : Type
WebGLRenderingContext = AnyPtr

export
WebGLProgram : Type
WebGLProgram = AnyPtr

export
%foreign "browser:lambda: (rtype, gl, cbk) => cbk(gl.createProgram())(gl)"
prim__createProgram : (1 _ : WebGLRenderingContext) -> (1 _ : (1 _ : WebGLProgram) -> (1 _ : WebGLRenderingContext) -> rtype) -> rtype

Since all data types are export, not public export, other modules do not know WebGLProgram = AnyPtr, just that some WebGLProgram exists and that it should be passed to prim__createProgram. That’s still an abstract data type, but a somewhat more efficient one (in Haskell we would do this using newtype).

Unfortunately, I can’t combine this trick with phantom types in practice, as it somehow results in a lot of unresolved holes, which are obnoxious to specify. For instance, if I were to declare:

export
WebGLProgram : ProgramStatus -> Type
WebGLProgram status = AnyPtr

I would have to specify the value for status all over the place. I’m not sure what is causing this. The following, on the other hand, is fine:

export
data WebGLProgram : ProgramStatus -> Type where
  MkWebGLProgram : AnyPtr -> WebGLProgram status

So I will be using somewhat superfluous data constructors after all. At least this will probably allow me to have interchangeable fast and safe modules.

Still on the subject of FFI, I’ve partially resolved the problems I had with glenums. In the WebGL / OpenGL spec glenums are just ints, with specific names bound to specific values (see WebGL constants on MDN). There are several ways I could deal with this issue, and I like none of them.

Use the abstract data strick as with other types:

-- shaders
export
ShaderType : Type
ShaderType = AnyPtr

export
%foreign "browser:lambda: () => 0x8B30"
GL_FRAGMENT_SHADER : ShaderType

But this breaks if I ever need to match on glenums, as is the case for getProgramParameter

Another solution is to just use Ints:

export
ShaderType : Type
ShaderType = Int

export
GL_FRAGMENT_SHADER : ShaderType
GL_FRAGMENT_SHADER = 0x8B30

Which is what I have currently, but again, if I want to case-match, I need to make the values public export, which breaks type-safety through abstract data types.

Refinement types would be absolutely great here. I’d like to do:

public export
GLEnum = Int

public export
GL_FRAGMENT_SHADER : GLEnum
GL_FRAGMENT_SHADER = 0x8B30


export
%foreign "browser:lambda: (aType, gl, type, callback) => callback(gl.createShader(Number(type)))(gl)"
prim__createShader : IsElem shaderType [GL_VERTEX_SHADER, GL_FRAGMENT_SHADER] => (1 _ : WebGLRenderingContext) -> (shaderType : GLEnum) -> (1 _ : (1 _ : WebGLShader) -> (1 _ : WebGLRenderingContext) -> a) -> a

And while you can express refinements in a dependently typed language, the result is verbose, and requires the end-user to pass proofs. I don’t find that acceptable. I’m fine with making the inner working of my library as complicated as it gets, but the API should be clean. That’s rather the point of this whole experiment. E.g. for something like the above, the end-user would have to write:

createShader (There Here) gl GL_FRAGMENT_SHADER

The There Here part being the proof, which gets longer in tandem with the list of accepted glenum values.

The last option I can think of, and the one I will probably go with, is to go back to the basics and take the performance hit: use sum types and create conversion functions to/from AnyPtr or Int.

data ShaderType
  = GL_VERTEX_SHADER
  | GL_FRAGMENT_SHADER

toShaderType : Int -> Maybe ShaderType
toShaderType i = case i of
  0x8B30 => Just GL_FRAGMENT_SHADER
  0x8B31 => Just GL_VERTEX_SHADER
  _ => Nothing

Stepping out of the world of FFI, there is an interesting, and rather annoying, issue in the design of the WebGL API concerning linear types, that is when passing null as a resource.

For example, this happens in the function bindVertexArray. It generally takes a WebGLVertexArrayObject, but will accept null as a value, which will bind the “default” vertex array object. It’s even recommended to pass null to bindVertexArray, as it will prevent code that is out of scope from overwriting a specific vao if it assumes the default one is bound. For now I’ll ignore the question if that recommendation is a weak solution for what should have been type-safety.

The point being, passing null is valid, but using linear values for WebGLVertexArrayObject means that null would be linear too, and bindVertexArray would return it to us! We would then have to pass null to deleteVertexArray. I’m fairly confident this is resolvable, if nothing else by creating a function unbindVertexArray, but it’s an interesting design issue. For now I want to tackle other type-safety concerns I have with VAOs before delving into this one, as I suspect they may influence each other.

More specifically, the other type-safety issues with VAOs concerns ensuring it matches a program. With vertex attributes, I just requires an attribute to be gotten from a specific program, and put program ids in a phantom types. This was never an entirely accurate solution, as a programmer could manually specify locations for attributes, ensure programs used the same locations, and bind attributes to static locations. With VAOs, this problem becomes larger, as a VAO does not necessarily match any particular program. There is no getAttribLocation variant for a VAO, it’s just createVertexArray. I could add an artificial restriction to match a vao to a specific program, but I don’t want that, it would require creating as many VAOs as there are programs, which is annoying and inefficient.

Instead, I will probably switch from using program ids to putting all attributes in the program types. This seems a lot more verbose at first:

Program Linked pid

vs

Program Linked [attributeType0, attributeType1, attributeType2...] [uniformType0, uniformType1, uniformType2]

But I expect these program types to be limited in users final code, so we can alias them like:

BlinnPhongProgram : Type
BlinnPhongProgram = Program Linked [...] [...]

The downside of this approach is that it’s going to be harder to pass attributes gotten through getAttribLocation. How would enableVertexAttribArrayand vertexAttribPointer know that the passed location variable is valid for the program, since it’s unknown at compile-time? That said, using VAOs is the preferred way of writing WebGL programs, so I will focus on that.

All in all I have a lot of work ahead of me, none of it easy.

previous
overview
next