Idris2+WebGL, part #16: Binding programs again

It's time to take up the issue I've been avoiding since part 9. The compiler somehow needs to more-or-less know what program is bound in order to determine whether certain commands are correct. This sucks, because it means we have to keep track of state statically, which is traditionally hard to do. But let's first take a step back.

My initial idea was to use existential types to bind programs and uniform locations together. I realize now this was a bad idea. A quick recap.

given the (simplified) types:

export
data Program : ProgramID -> Type where
  ...

export
data UniformLocation : ProgramID -> Type where
  ...

We can define functions to work on a Program pid and UniformLocation pid, requiring that pid values are the same. There is a trick we can pull with this:

someFunction : forall a . (forall pid . Program pid -> UniformLocation pid -> a) -> a

because forall pid is part of the first argument, the first argument for someFunction must be a function able to handle any value of pid. Because of that, it cannot know anything about pid other than that it exists and it's the same between Program and UniformLocation. This way it's possible to tie specific variables together in their type.

The problem is that this is not the correct restriction.

When we call e.g. unifom2fv, the rule is that the passed location in the bound program must be for a 2-element array of floats. It's perfectly fine to have the same uniform locations for different programs. While that seems silly for individual uniforms, WebGL2 introduced uniform blocks, which can be shared between programs to improve performance.

Rather than typing programs with a phantom ID, I should type them by their attributes and uniforms. So long as they match our expectations, everything is fine, wherever we got a uniform location from.

The program type signature should therefore be something like:

public export
Attribute = (String, Int32, GLEnum) --name, size, type

public export
Uniform = (String, Int32, GLEnum) -- same

export
data Program : List Attribute -> List Uniform -> Type where
  ...

The real code is a bit more complicated, for instance to ensure only correct GLEnum values can be used, but that's the gist of it.

This still leaves the problem of keeping track of what program is in use, to which I have no nice solution.

When we call e.g. uniform2fv, we know the location and type of the passed variable, but not the program (not at compile time). This means we cannot compare the passed data to the inputs of the program, and a runtime type mismatch is possible. OpenGL4 allows for binding uniforms to specific programs, which circumvents the need of keeping track of used program. Unfortunately WebGL2 does not have these nice new functions. I could emulate them, but that's overhead I'm loathe to add.

So we're back to indexed state monads, hoare monads, and passing linear values around.

Consider the function to use a program:

useProgram : MonadState WebGL2.WebGLRenderingContext m =>
  (1 _ : WebGLProgram attributes uniforms) ->
  m (WebGLProgram attributes uniforms)

A naive approach is to add a phantom type to the program to denote if it was bound:

useProgram : MonadState WebGL2.WebGLRenderingContext m =>
  (1 _ : WebGLProgram  attributes uniforms NotInUse) ->
  m (WebGLProgram  attributes uniforms InUse)

(We could do something even fancier with dependent types that does not require changing our type definitions, but that's not particularly relevant here)

This would allow us to do something rather cool with erased implicit arguments:

uniform1fv : MonadState WebGL2.WebGLRenderingContext m =>
  WebGLUniformLocation uniformType ->
  {auto 0 prf : WebGLProgram attributes uniforms InUse} ->
  Float32Array ->
  m ()

which would check if a WebGLProgram that has been marked as InUse (by useProgam) exists at all in the current context.

The problem is that we can call useProgram twice, getting 2 programs that are InUse, even though only the last one actually is.

So, one way or another, useProgram must "consume" some form of program status when invoked.

What's even worse, I'm not trying to prevent the user from binding to non-existing inputs. That's actually fine, even useful when debugging, and can be ignored. The problem is not binding values that are used. So we also need to keep track of what inputs have been bound.

Because of that, I'm currently inclined to think some form of indexed monads are inevitable. I'm not very happy about that because it makes things a bit more complicated for the end-user. Indexed monads are not all that common after all.