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 showusing 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

I can't embed WebGL on dev.to AFAIK. You'll have to check my blog if you really want to see an unlit spinning white triangle.

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.