Hello triangle, first thoughts

I decided to explore the practical implications of dependent types by creating a type-safe WebGL application in Idris 2.

The endeavor is somewhat harebrained. WebGL is still rather close to metal - though not as much as, say, Vulkan - whereas advanced type systems are mostly tied into human reasoning. I will therefore mostly be adding restrictions to existing commands. In general, I’d oppose this approach, arguing that we should let the compiler control hardware and let the programmer express business logic, but it seems like a good exercise with plenty of complicated cases to test the power and actual difficulty of dependent typing.

FFI basics

Compiling to JavaScript is fairly straightforward and well-documented. Set export IDRIS2_CG=javascript and we’re done.

Calling JS code is also simple enough. We only need to define a lambda expression in JavaScript and give it a name and type in Idris.

%foreign "browser:lambda: (gl, r, g, b, a) => gl.clearColor(r,g,b,a)"
prim__glClearColor : AnyPtr -> Double -> Double -> Double -> Double -> PrimIO ()

Of course, since JavaScript does not really have types the type notation is a matter of “just trust me”.

We can then use the primitive functions through primIO:

clearColor : HasIO io => GLContext -> Double -> Double -> Double -> Double -> io ()
clearColor (GLContextWrapper gl) r g b a = primIO $ prim__glClearColor gl r g b a

Idris’ FFI is a bit too restrictive for my taste. The list of supported types is very limited. This is on purpose, as it is easier to create new backends when only few types need to be supported. In practice it means I’ll have to jump through hoops to use e.g. booleans and typed arrays and that the final application may be rather slow because of it.

data BufferDataSource = BufferDataSourceWrapper AnyPtr

%foreign "browser:lambda: size => new Float32Array(Number(size))"
prim__new_Float32Array_size : Int -> PrimIO AnyPtr

%foreign "browser:lambda: (a, i, v) => a[Number(i)] = v"
prim__set_Float32Array_at : AnyPtr -> Int -> Double -> PrimIO ()

-- NOTE: this could probably have been more succinct with a forM_ or similar. Haven't dived too deeply in the Idris packages yet.
fill_Float32Array : HasIO io => AnyPtr -> Vect _ Double -> io ()
fill_Float32Array f32a = fill_Float32Array_recursive 0
    fill_Float32Array_recursive : Int -> Vect _ Double -> io ()
    fill_Float32Array_recursive idx vect =
      case vect of
        Nil => pure ()
        (v :: vs) => do
          primIO $ prim__set_Float32Array_at f32a idx v
          fill_Float32Array_recursive (idx + 1) vs

float32Array : HasIO io => {size : _} -> Vect size Double -> io BufferDataSource
float32Array vs = do
  typedArrayAnyPtr <- primIO $ prim__new_Float32Array_size (cast size)
  fill_Float32Array typedArrayAnyPtr vs
  pure $ BufferDataSourceWrapper typedArrayAnyPtr

I personally disagree with the decision. When using a foreign function we are already binding our program to a specific backend, so it would make more sense to me to let that backend dictate available types than use a restricted list of broadly supported ones to support backends we’re not using anyway.

For enums I’m using Idris sum types and converting them to string to pass onto JS:

public export
data GLBufferTarget

bufferTargetStr : GLBufferTarget -> String
bufferTargetStr target =
  case target of

%foreign "browser:lambda: (gl, targetName, buffer) => gl.bindBuffer(gl[targetName], buffer)"
prim__bindBuffer : AnyPtr -> String -> AnyPtr -> PrimIO ()

bindBuffer : HasIO io => GLContext -> GLBufferTarget -> WebGLBuffer -> io ()
bindBuffer (GLContextWrapper gl) target (WebGLBufferWrapper buffer) =
  primIO $ prim__bindBuffer gl (bufferTargetStr target) buffer

For most functions I’m getting values from JS / WebGL as AnyPtr and wrapping them in an abstract data type to get some very basic type safety.

I’m considering doing this for (nearly) every JS value, including e.g. Number and Bool, so I don’t need additional conversions. I’d be using e.g.:

data JSNumber = JSNumberWrapper AnyPtr

with FFI bindings for arithmetic etc.

Ultimately a performance test will be necessary as I’m not sure if the additional foreign function calls will outweigh the time saved on conversions.

Hello triangle

With the above in mind I’ve created bindings for a couple of functions, just enough to get a triangle on the screen.


Future worries

A few worries come to mind, mostly performance:

A lot of work still to do simply drawing a bit more and starting to implement the rules that are documented but not typed.