Idris2+WebGL, part #8: Baby's first dependent type
Tags: idris, functional
Published: 2021-01-31 12:41:42

---
title: Idris2+WebGL, part #8: Baby's first dependent type
tags: #Idris, #functional
published: true
canonical_url: https://drbearhands.com/idris-webgl/part8/
series: Idris2 and WebGL
---

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.

```Idris
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:

```Idris
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.

```C
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:

```Idris
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

```Idris
-- 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:

```Idris
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.

```Idris
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.

```Idris
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.