Idris2+WebGL, part #13: Slow and frustrating progress
Tags: idris, functional
Published: 2021-03-10 12:22:07

---
title: Idris2+WebGL, part #13: Slow and frustrating progress
published: true
series: Idris2 and WebGL 
tags: #Idris, #functional
canonical_url: https://drbearhands.com/idris-webgl/part13/
---


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

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

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

```Idris
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 `glenum`s.
In the WebGL / OpenGL spec `glenum`s are just `int`s, with specific names bound to specific values (see [WebGL constants on MDN](https://developer.mozilla.org/en-US/docs/Web/API/WebGL_API/Constants)). 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:
```Idris
-- 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 `Int`s:

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

```Idris
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](https://www.reddit.com/r/dependent_types/comments/ay7d86/what_can_refinement_types_do_that_dependent_types/), 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:

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

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

```Idris
Program Linked pid
```

vs

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

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