Idris2+WebGL, part #2: some animation

My next milestone was cleaning up and getting a bit of animation in. The changes themselves are not particularly interesting, but brought a few interesting realizations.

Interfaces

I started using interfaces, which work pretty much like Haskell’s typeclasses. I don’t dislike the change of terminology as it’s in line with what OOP programmers are familiar with. One thing I love (but didn’t get to use yet) is named implementations of interfaces. Haskell’s approach of fixing specific functions to a type for a given interface feels a bit like a mistake to me. In mathematics, there may be many monoids for a specific set. This is not purely a theoretical point as it has caused some issues for me in the past.

requestAnimationFrame

Implementing animation required using requestAnimationFrame, which requires a callback with arguments. There’s a bit of a gotcha here: a function passed as a callback from Idris may have to be called twice depending on its type. Once to apply arguments and once to “run” the PrimIO. E.g. a function doSomething : PrimIO would be called as doSomething() in JS, but a function doSomething : Double -> PrimIO needs to be called as doSomething(x)(). This makes sense once you think about it, PrimIO should be just a value before you “run” it.

Results

Here is the result:

Code in the state at the time of writing can be found in the repo.

Thoughts

FFI and type wrappers

Idris seems quite fond of FFI. I’m not personally a huge fan of FFI, it ruins proofs and compile-time opportunities, but there’s definite business value in it. This entire projects revolves around it in fact. That said, I think there’s room for improvement.

Some syntactic sugar for creating type-relations between source and target language would be nice. I find myself writing a lot of abstract data types of the form:

export
data GLContext = GLContextWrapper AnyPtr

export
data GLProgram = GLProgramWrapper AnyPtr

export
data AttribLocation = AttribLocationWrapper AnyPtr

%foreign "browser:lambda: (gl, index) => gl.enableVertexAttribArray(Number(index))"
prim__enableVertexAttribArray : AnyPtr -> AnyPtr -> PrimIO ()

export
enableVertexAttribArray : HasIO io => GLContext -> AttribLocation -> io ()
enableVertexAttribArray (GLContextWrapper gl) (AttribLocationWrapper aLoc) =
  primIO $ prim__enableVertexAttribArray gl aLoc

%foreign "browser:lambda: (gl, program, name) => gl.getAttribLocation(program, name)"
prim__getAttribLocation : AnyPtr -> AnyPtr -> String -> PrimIO AnyPtr

export
getAttribLocation : HasIO io => GLContext -> GLProgram -> String -> io AttribLocation
getAttribLocation (GLContextWrapper gl) (GLProgramWrapper program) name = do
  aLoc <- primIO $ prim__getAttribLocation gl program name
  pure $ AttribLocationWrapper aLoc

Which could be sugared using special “wrapper” data declarations:

export
wrapper GLContext

export
wrapper GLProgram

export
wrapper AttribLocation

%foreign "browser:lambda: (gl, index) => gl.enableVertexAttribArray(Number(index))"
prim__enableVertexAttribArray : GLContext -> AttribLocation -> PrimIO ()

export
enableVertexAttribArray : HasIO io => GLContext -> AttribLocation -> io ()
enableVertexAttribArray gl aLoc = primIO $ prim__enableVertexAttribArray gl aLoc

%foreign "browser:lambda: (gl, program, name) => gl.getAttribLocation(program, name)"
prim__getAttribLocation : GLContext -> GLProgram -> String -> PrimIO AttribLocation

export
getAttribLocation : HasIO io => GLContext -> GLProgram -> String -> io AttribLocation
getAttribLocation gl program name = primIO $ prim__getAttribLocation gl program name

This solution seems a bit less error-prone and more readable. The transformation is pretty straightforward for a compiler and I expect it can be made more efficient too as the wrappers only need to exist at compile time (similar to Haskell’s newtype).

Error messages

Error messages in Idris are (still) a little unhelpful. I have no idea if this is due to the nature of linear typing, making it difficult to predict what the programmer may have meant, or if it’s just a matter of missing polish.

As example:

main.idr:73:3--73:76:While processing right hand side of makeTriangle at main.idr:72:1--88:1:
Can't find an implementation for Monad ?m at:
73    program <- createShaderProgram gl vertexShaderSource fragmentShaderSource
      ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

Warning: compiling hole Main.makeTriangle
Uncaught error: INTERNAL ERROR: (CRASH "Encountered undefined name Main.makeTriangle")

The problem turned out to be on the last line of the block (not present in the error message), where I’d written:

pure $ MkDrawable program buffer positionAttribLocation

which missed an argument to MkDrawable.

I find that the only bit of information I can rely on from the compiler is the top-level function in which the error occurs. From what I’ve experienced so far this is the biggest issue I would have for using Idris in production.


If you like my work, please consider buying me a coffee.