Idris2+WebGL, part #15: Restricting arguments to a list
Tags: idris, functional, webgl
Published: 2021-08-07 11:08:14

---
published: true
title: Idris2+WebGL, part #15: Restricting arguments to a list
tags: #Idris, #functional, #webgl
canonical_url: https://drbearhands.com/idris-webgl/part15/
series: Idris2 and WebGL 
---

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:

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

```Idris
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](https://idris2.readthedocs.io/en/latest/tutorial/miscellany.html?highlight=auto#auto-implicit-arguments), 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:

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

```Idris
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 `GLenum`s, 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.