Idris2+WebGL, part #16: Binding programs again
Tags: idris, functional, webgl
Published: 2021-08-20 14:27:08

---
title: Idris2+WebGL, part #16: Binding programs again
tags: #Idris, #functional, #webgl
canonical_url: https://drbearhands.com/idris-webgl/part16/
published: true
series: Idris2 and WebGL 
---

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:

```Idris
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:

```Idris
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:
```Idris
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](https://www.khronos.org/registry/OpenGL-Refpages/gl4/html/glProgramUniform.xhtml), 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:
```Idris
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:

```Idris
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:

```Idris
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.