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