Idris2+WebGL, part #8: Baby's first dependent type

Idris2 was recently updated to version 0.3. This required a fair bit of refactoring, but that's boring stuff that isn't really worth writing about.

Instead I'm going to log how I used dependent types to ensure only valid shader programs could be used.

In regular WebGL / OpenGL, the programmer is supposed to link a shader program, then check if it succeeded and only use the program if / while it is valid. Linking will not throw an error if it fails and nothing is preventing the programmer from using a deleted program.

I would like to be able to specify that certain functions, such as useProgram, require a program to be valid. Since deletion is no longer a risk thanks to linear types, that primarily means verifying the program's link status. So I added link status as a phantom type to programs.

public export
data ProgramStatus
  = Unlinked
  | Linked

export
data Program : ProgramStatus -> Type where
  MkProgram : (1 _ : AnyPtr) -> (Program s)

Now we can have a Program Unlinked or a Program Linked with the same internal representation. To keep this safe, I again rely on creating an Abstract Data Type (that is, not exporting the constructor of Program, thereby relying on exposed functions), so that new programs are Unlinked and cannot be used until they are linked:

createProgram : HasGL gl => gl (Program Unlinked)
useProgram : HasGL gl => (1 _ : Program Linked) -> gl (Program Linked)

I still need to actually link the program. According to the spec, linking a program does not give any indication of success, we need to query for that afterward.

void linkProgram(Object program);

// pname: DELETE_STATUS, LINK_STATUS, VALIDATE_STATUS, ATTACHED_SHADERS, ACTIVE_{ATTRIBUTES, UNIFORMS}, ACTIVE_UNIFORM_BLOCKS, TRANSFORM_FEEDBACK_BUFFER_MODE, TRANSFORM_FEEDBACK_VARYINGS
any getProgramParameter(WebGLProgram? program, enum pname);

There is a lot here that I hate from a clean code perspective, but so be it...

I've implemented linkProgram in Idris as such:

linkProgram : HasGL gl => (1 _ : Program s) -> gl (Program Unlinked)

This should look off. The function takes a program with unknown state s, and produces an unlinked program, which sounds like the opposite of what we wanted. The issue is that we do not know if the program was linked successfully after invoking this function. But we do know the state has changed, so we know that it is not s. I'm defining Unlinked to mean "not known to be linked", rather than "known not to be linked". I should probably think of a better name.

Unfortunately we cannot use a variable here to indicate uncertainty. E.g. a program created using the following

-- wrong!
linkProgram : HasGL gl => (1 _ : Program s1) -> gl (Program s2)

would match either Program Linked or Program Unlinked, since s2 is polymorphic / universally quantified.

Now there is such a thing as existential types, which would be a slightly more accurate fit. Using existential types we can express "I know a state for this exists, but do not know what it is". We can express them with continuation and universally quantified inputs:

linkProgram : HasGL gl => (1 _ : Program s1) -> (1 _ : Program s2 -> gl a) -> gl a

but I find this overly complex, so I'm resigned to a link function that returns an unlinked program.

Now onto the meat of the matter, getProgramParameter.

The definition of getProgramParameter is a problem. It corresponds to the C / OpenGL function GetProgramiv, which returns a rather type-unsafe int. In JS, it abuses dynamic types. I do believe I could express this behavior using dependent types, by letting the return type depend on the input type, but that would be quite mad. Nobody wants to pass pname as a variable, the function should really have been split into separate concerns.

So, I'll simplify the problem for myself and create a getProgramLinkStatus function instead.

getProgramLinkStatus : HasGL gl => (1 _ : Program s) -> gl (DPair.Res Bool (\linked => Program (if linked then Linked else Unlinked)))
getProgramLinkStatus (MkProgram p) = liftGL $
  MkGL $ \gl =>
    prim__getProgramLinkStatus gl p \status, p, gl =>
      MkGLRes ((status /= 0) # MkProgram p) gl

Yep, that's a lambda expression inside a type declaration. A DPair.Res is a dependent pair where the type of the second element depends on the value of the first. It's similar to how in Go programmers often return pairs of errors and values, but with added type-safety that ensures we check for errors.

program           <- createProgram
linkOk # program  <- getProgramLinkStatus program
if linkOk
  then ?do_something_with_linked_program
  else ?do_something_else

here in the type hole do_something_with_linked_program, program will have type Program Linked and in do_something_else it will have type Program Unlinked.

We could of course have achieved the same effect with sum types. This little excursion into dependent types has left me rather underwhelmed. Hopefully a more relevant use case will pop up soon.

On the other hand, while performing the changes above, linear type restrictions caught several would-be bugs, such as forgetting cleanup outside happy-flow. Linear types are a real keeper as far as I'm concerned.