Oh yes this is awesome.
Many WebGL functions take a GLenum value, secretly an integer Number in JavaScript. The problem with this is that it's not a compile error to pass an invalid value, even though this could be statically determined. For instance:
glCreateShader GL_POINTS
is valid at compile time, even though it is nonsensical. glCreateShader wants a shader type, not a draw mode.
Typically, we would remedy this by creating a sum type:
data ShaderType = GL_VERTEX_SHADER | GL_FRAGMENT_SHADER
But this still has a few problems: some values belong to different input sets, and we have added overhead to convert from ShaderType to Int and vice-versa.
While these problems can be fixed, the solution is not particularly elegant.
So, I've been diving into Idris2 library code to find one of its less well-documented features (it's there, it's just not very obvious if you don't already know what it is). I found exactly what I was looking for in auto proofs. I will illustrate with a simplified version of the glCreateShader function. This is the (simplified) regular version:
glCreateShader : GLenum -> GL ()
This function signature pretend to accept any GLenum, but will cause errors on anything that is not a GL_VERTEX_SHADER or GL_FRAGMENT_SHADER. With auto proofs we can write:
glCreateShader : (shaderType : GLenum) -> {auto 0 prf : Elem shaderType [GL_VERTEX_SHADER, GL_FRAGMENT_SHADER]} -> GL ()
There's a few things going on here.
(shaderType : GLenum) is not substantially different from GLenum, but it gives a name to the variable in the type signature, so that we can use it there.
Then we have {auto 0 prf : Elem shaderType [GL_VERTEX_SHADER, GL_FRAGMENT_SHADER]}, let's ignore auto for now, {0 prf : X} indicates we have a variable prf of type X that only exists at compile time (it has multiplicity 0). Elem x xs is the type for a proof that x is in the list xs. By prepending auto, we tell Idris to find the proof automatically, rather than relying on the programmer. So, {auto 0 prf : Elem shaderType [GL_VERTEX_SHADER, GL_FRAGMENT_SHADER]} is a proof that shaderType is a value found in [GL_VERTEX_SHADER, GL_FRAGMENT_SHADER], the proof only exists at compile time, is constructed automatically if possible, and we don't have to pass it explicitly.
To call glCreateShader, we can still write glCreateShader GL_VERTEX_SHADER, but if we try glCreateShader GL_POINTS, the Idris compiler will complain that it cannot find an implementation (an implementation is a proof) for Elem GL_POINTS [GL_VERTEX_SHADER, GL_FRAGMENT_SHADER].
There remains the situation where we want to pass a variable to glCreateShader with a value unknown at compile time. I find that these cases are rare, but when they occur, the programmer simply has to provide the proof, or create a context from which the proof can be automatically derived. While this is a restriction, that was exactly the point, not just trusting the programmer is always right, because we're really not.
I am really happy I discovered this feature. Not only does it fix this annoying issue I had with GLenums, but I believe it was the missing piece for a couple of problems I've had in the past, e.g. the creation of open sums and open products.
Top comments (0)