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
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
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
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
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
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
Another solution is to just use
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
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
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
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
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.