I've had a few months without progress. This project had started to get frustrating so I gravitated towards other hobbies and ideas.
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)
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.