Getting back into it

I’ve had a few months without progress. This project had started to get frustrating so I gravitated towards other hobbies and ideas.

Among other things, I was working on a WebGL app in JavaScript, but the explosive complexity caused by a lack of static types drove me up the walls. So many easily preventable bugs… It was a good reminder of why I want to use WebGL in Idris in the first place.

In the meanwhile, a version 0.4 of Idris was released, and with it, two features I rather like. First, do-notation now uses the >> operator as well as the >>= operator. This allows the safe discarding linear units, as >> consumes them. Where previously I had to write:

do
  () <- clearColor 0 0 0 1
  () <- clear (GL_COLOR_BUFFER_BIT + GL_DEPTH_BUFFER_BIT)

just to pattern-match / consume the linear unit value, now I can just write

do
  clearColor 0 0 0 1
  clear (GL_COLOR_BUFFER_BIT + GL_DEPTH_BUFFER_BIT)

additionally, the FFI with JavaScript has changed, so that I need far fewer conversion to and from BigInt. Nice.

Finally, I found a rather essential bit of information I was ignorant of: with linear typing comes not one, but two new functors!. This in itself wasn’t groundbreaking, but it made me realize, more than I did before, that linear types require fundamentally different control structures. Were I was previously struggling to find the right type declaration for a linear Traversable typeclass, so that I could make a for function, without knowing if it iterates over linear or constant values… now I decided to simply make 2 foldM functions for lists only:

foldM : LMonad m => ((1 _ : b) -> (1 _ : a) -> m b) -> (1 _ : b) -> (1 _ : List a) -> m b
foldM' : LMonad m => ((1 _ : b) -> a -> m b) -> (1 _ : b) -> List a -> m b

Problems gone! I can think about Traversable typeclasses after I get a better understanding of the abstract subject matter and its practical use.

I plan to focus a little less on getting as much of the WebGL spec exactly in the type system and more on making an actual app in tandem. To go for the “eat your own dog food” approach. I still want to end up with a spec that completely encompasses the documentation in the types, but I might drop or rework certain functions that just don’t make a lot of sense.