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:

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

export
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
  where
    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

export
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
  = GL_ARRAY_BUFFER
  | GL_ELEMENT_ARRAY_BUFFER
  | GL_PIXEL_PACK_BUFFER
  | GL_PIXEL_UNPACK_BUFFER
  | GL_COPY_READ_BUFFER
  | GL_COPY_WRITE_BUFFER
  | GL_TRANSFORM_FEEDBACK_BUFFER
  | GL_UNIFORM_BUFFER

bufferTargetStr : GLBufferTarget -> String
bufferTargetStr target =
  case target of
    GL_ARRAY_BUFFER => "ARRAY_BUFFER"
    GL_ELEMENT_ARRAY_BUFFER => "ELEMENT_ARRAY_BUFFER"
    GL_PIXEL_PACK_BUFFER => "PIXEL_PACK_BUFFER"
    GL_PIXEL_UNPACK_BUFFER => "PIXEL_UNPACK_BUFFER"
    GL_COPY_READ_BUFFER => "COPY_READ_BUFFER"
    GL_COPY_WRITE_BUFFER => "COPY_WRITE_BUFFER"
    GL_TRANSFORM_FEEDBACK_BUFFER => "TRANSFORM_FEEDBACK_BUFFER"
    GL_UNIFORM_BUFFER => "UNIFORM_BUFFER"

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

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

export
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:

Check the performance hit caused by the current approach
Use types for JS values like JSNumber, make them drop-in replaceable with native Idris values by changing just the WebGL bindings for a future performance comparison.
The gl context may be more suited to being a record of closures, much as it is in JS. The syntax would be closer to JS and it would allow using native values for enums. Performance may again suffer for it
Perhaps some native JS optimization step would work for code compiled from Idris as well. Inlining might help for one.

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

overview