Ensuring uniforms belong to bound program

To pass variable data to a shader, WebGL / OpenGL uses uniforms and attributes. To use them, we must first get the location of a uniform in a program by its name, then pass that location with the data we want to “put” there.

The relevant C functions are the following (WebGL variants are similar):

GLint glGetUniformLocation(
  GLuint program,
  const GLchar *name
);

void glUniform1fv(
  GLint location,
  GLsizei count,
  const GLfloat *value
);

The location is just an integer, and different programs may use the same location for different things. It’s an error to pass the uniform from one program to another but there’s nothing keeping us from doing it. I’d like to make this error impossible using types, which is going to be quite a challenge.

I should note that efficient WebGL applications would prefer using uniform buffer objects, as it allows passing multiple uniforms at once and keeping uniforms between programs, but that seems even more complicated so I’ll cross that bridge when I get there.

There are two aspects to this problem. First, we need to express that a uniform location belongs to a certain shader program. Second, we need a way to keep track of which program is currently bound so that we can verify that the location passed to uniform function belongs to the currently bound program. I also want to stay away from runtime checks. Runtime checks would add overhead and these functions are called inside the critical loop so they should be as efficient as we can make them.

I’ve previously tried making OpenGL typesafe in Haskell. This feature, in particular keeping track of which program is currently bound, is what made me give up. The precise reason will become clear further on in this post.

Binding locations to a program

Existential types

When I tried to make this feature in Haskell I settled on using existential types to relate a location to a specific program. At a high level, I’m using a phantom type (a type that only really exists at type level) as an argument to a program. glGetUniformLocation would generate locations with the same phantom type as the program. But createProgram only specifies that a phantom type exists, not what it is. No other function gives a value to this inner phantom type of programs, and constructors are not exported. Therefore, if the inner types of a location and program match, it must come from a glGetUniformLocation.

So how can we express this in Idris? First we add phantom types to program and uniform location:

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

export
data UniformLocation : Type -> Type where
  MkUniformLocation : AnyPtr -> UniformLocation p

Then we need to adapt createProgram. To my knowledge we cannot specify an existential type directly. However, an existential type in a positive position is equivalent to a universal type in a negative position. Or in simpler terms: if all that we know of something is that it exists, we can only apply it to functions that work on anything. In code:

createProgram : HasGL gl => (forall p . Program p Unlinked -> gl a) -> gl a

alternatively it’s possible to create a new type that has the universal quantifier in a negative position in its constructor:

data ProgramCont : Type -> Type where
  WithProgram : ((forall p . (Program' p s -> a)) -> a) -> ProgramCont s

createProgram : HasGL gl => gl ProgramCont Unlinked

We can save the relation between program and location in a datatype:

data ProgramLocationPair : Type where
  MkPLP : Program' p Linked -> UniformLocation' p -> ProgramLocationPair

Dependent type trickery?

The above approach has two drawbacks. First, I just don’t like continuations. An existential type may be mathematically equivalent to the inverse of a universal type, but the two do not express the same thinking. I also dislike the extra indentation. It is artificial complexity. Second, we’ve only achieved type safety through abstract data types. I.e. it is safe because the exported operations cannot lead to faulty state. That’s a pretty difficult thing to keep track of.

Perhaps there is something that can be done using Idris’ dependent types, I’m not familiar enough with them to tell for sure, but I don’t think so. Since I don’t want to use run-time values, to avoid overhead, constructions like DPair from my last log entry are a no-go. On the other hand, compile-time values, what I usually think of as types, don’t vary AFAIK between multiple invocations of the same code, so we cannot rely on knowledge of a type, only ignorance. But I’m new at this and my reasoning could be wrong.

One thing I could do is create a proof datatype that a location belongs to a certain program:

data LocationInProgram : Location -> Program -> Type
  MkLocationInProgram : LocationInProgram l p

and have that proof returned by getUniformLocation. I can’t imagine this working well with linear types though.

Keeping track of bound programs

While OpenGL 4 has a a function that sets uniform for a specific program, WebGL only has functions that set uniform locations in the program currently in use. If I want to achieve type safety in this area I’m going to have to somehow keep track of what program is bound.

linearity

Since our program is linear we could add the “is use” as a phantom type. useProgram would then swap the “in use” inner phantom type between two programs. E.g.:

useProgram : HasGL gl =>
  (1 _ : Program p1 Linked InUse) ->
  (1 _ : Program p2 Linked NotInUse) ->
  gl (LPair (Program p1 Linked NotInUse) (Program p2 Linked InUse))

I’d then have to pass the program as a proof to uniform functions:

uniform1fv : HasGL gl => (1 _ : Program p Linked InUse) -> UniformLocation p -> (1 _ : Float32Array 1) -> Int -> Int -> gl (LPair (Float32Array 1, Program p Linked InUse))

However, it’s perfectly fine to have no program in use, and that is in fact the initial state. There might be acceptable workarounds to this, like having a special “null” program, but I don’t like how this is changing function calls from the original WebGL specification. It also creates the weird situation where we’d like to use both erasure and linearity since we don’t actually want to pass the program at runtime…

It would also be possible to pass just a witness to the program being in use:

useProgram : HasGL gl =>
  (1 _ : ProgramWitness p1) ->
  (1 _ : Program p2 Linked) ->
  gl (LPair (ProgramWitness p2) (Program p2 Linked))

But by-and-large that has the same problems, although the type can be a unit so that a smart compiler could optimize it away. The Idris JS backend compiler is not that smart yet AFAIK. I’d also rather not force the programmer to keep track of all kinds of state witnesses.

State monads

Using state monads only vary in their value and would therefore require runtime checks, so I’m not considering them.

Indexed monads

When I tried to keep track of which program is bound in Haskell I went for indexed state monads. These are essentially state monads where the type of the state can vary. An indexed monad has, besides the “value” type of regular monads, 2 more type variables: the input state type and the output state type, which form the “indices”. We can only compose two indexed monads if the output index of the first matches the input index of the second.

This was my Haskell code:

-- | Indexed counterpart of the functor
class IxFunctor k f | f -> k where
  -- | Indexed variant of @`Data.Functor.fmap`@, retains the indices of the
  -- input IxMonad
  imap :: forall (s1 :: k) (s2 :: k) a b . (a -> b) -> f s1 s2 a -> f s1 s2 b


-- | Indexed monad m with index kind k
class IxFunctor k m => IxMonad k m | m -> k where
  -- | indexed variant of the @`Control.Monad.return`@ function, does not alter
  -- the index
  return :: forall (s :: k) a . a -> m s s a
  -- | indexed variant of the bind operator @`Control.Monad.>>=`@.
  (>>=) :: forall (s1 :: k) (s2 :: k) (s3 :: k) a b. m s1 s2 a -> (a -> m s2 s3 b) -> m s1 s3 b
  -- | indexed variant of the @`Control.Monad.>>`@ operator.
  (>>) :: forall (s1 :: k) (s2 :: k) (s3 :: k) a b . m s1 s2 a -> m s2 s3 b -> m s1 s3 b
  (>>) v w = v >>= \_ -> w

The problem with this approach was that indices have a precise state. I’d like to represent knowledge instead. Knowledge can be forgotten, precise state has to be altered manually. Sometimes we just don’t know what program is bound at the end of a loop and don’t care either. With indexed monads the programmer would have to explicitly call a forgetProgram function, which was somewhat obnoxious.

Knowledge monads

I’m still not sure if this is even possible, but after indexed monads I tried to represent knowledge as knowledge rather than precise state, using different rules for the bind operation. While in all honesty I don’t remember the specifics, the result was that there where multiple “paths” between input type and output type after binding multiple “knowledge monads”. The compile did not like this kind of nondeterminism one bit.

I’m not super enthusiastic about repeating this experiment because it was rather complicated and I’m not sure the Idris compiler would like it any better.

Hoare state monad

Since what I want to do is essentially Hoare logic, I went searching online for ways to achieve this in a functional context and found an article about the Hoare state monad. The solution is in Coq and cannot be implemented in Haskell (to my knowledge). I’m still working out how / if this can be expressed in Idris, if it can help me get around the fully defined state type problem of indexed monads, and if doing so will incur runtime costs.

In conclusion

My head hurts.

previous
overview
next