Idris2+WebGL, part #5: Linearity continued

Sifting through Idris' literature on quantitative type theory I discovered that the issues with linearity I had in my last log are not just a complete misunderstanding on my part.

One of the larger underlying issues is a lack of polymorphism over quantities, which Edwin Brady points out explicitly in the paper. This is a bit annoying by itself (see my previous log entry) but also causes troubles with do-notation as the >>= operator is non-linear. Specifying a linear variant of >>= solves this issue as Idris allows for overloaded operators:

(>>=) : (1 act : IO a) -> (1 k : a -> IO b) -> IO b
(>>=) = io_bind

This is noted somewhat as an afterthought at the end of section 3 of the paper. IMO it should be more prominently displayed in the Idris crash course. I'm making a mental note to make a merge request once I have linear types figured out.

I'm still fuzzy on why quantities seem to only be defined on negative positions, forcing programmers to use continuations, but think I'm starting to understand, though not necessarily agreeing.

If we have a function f : (1 _ : A) -> B, and some 1 x : A, then in order to ensure x is consumed only one, we must ensure f x is only consumed once, since it "contains" x. So the result of application of a function to a linear argument results in a linear value either way. Noting linearity for all outputs while currying seems excessive:

f : (1 _ : A) -> (1 _ : (B -> 1 _ : C))

-- vs

f : (1 _ : A) -> B -> C

On the other hand - and this is where I lose track of things a bit - it is possible, and necessary, to have non-linear outputs for destructors:

destroyA : (1 _ : A) -> IO ()

Which isn't entirely non-linear of course since the "world" inside IO is linear.
Similarly, it's possible to mix linear with non-linear data:

data MyComplexType : Type where
  -- the first argument to MkMyComplexType is non-linear, the second is linear
  MkMyComplexType : (valConst : A) -> (1 valLin : B) -> MyComplexType

which can be a return type. Well fuck me...

It looks like linear type systems have some fundamental, near-philosophical questions to answer. Is a function from linear to non-linear data valid? It seems quite acceptable in principle to have a function consume a resource and create knowledge. But this breaks referential transparency. What about lazy evaluation? That would ensure f x would be evaluated only once anyway. Perhaps there's something to be said for dumping functions as first-class citizens in favor of linear types? We might have the mathematics, but not yet, I believe, the practical insights.

With that said, I did manage to use linear types in my WebGL program so that it compiles / type checks. Unfortunately there are still some issues left on the FFI front. For instance, some functions, such as glAttachShader, will consume / modify 2 linear values. It makes sense to then return them in a tuple:

attachShader : GLContext -> (1 _ : GLProgram) -> (1 _ : GLShader) -> (GLProgram, GLShader)

However, the FFI does not support tuples! So we have to use a continuation again. This seems ugly and inefficient. Ugly because of excessive nesting, and inefficient because it loses optimization opportunities, the compiler cannot know that values are merely modified and would have to treat the "new" linear value as though it were really new. At least not without knowledge of the backend. I therefore remain of the opinion that some form of "inout" notation to denote modified values would have value in FFI definitions at least.

We can at least get rid of the uglyness of continuations, but I have a feeling this is a bit naughty and it has already led to problems. Rather than having an IO () return value, we use a polymorphic return type and create a tuple in a wrapper function:

%foreign "browser:lambda: (type, gl, program, shader, cbk) => {gl.attachShader(program, shader); return cbk(program)(shader);}"
prim__attachShader2 : AnyPtr
  -> (1 _ : AnyPtr)
  -> (1 _ : AnyPtr)
  -> (1 _ : (1 _ : AnyPtr) -> (1 _ : AnyPtr) -> a)
  -> a

export
attachShader2 : GLContext -> (1 _ : GLProgram) -> (1 _ : GLShader) -> (GLProgram, GLShader)
attachShader2 (GLContextWrapper gl) (GLProgramWrapper program) (GLShaderWrapper shader) =
  prim__attachShader2 gl program shader $ \program', shader' =>
    (GLProgramWrapper program', GLShaderWrapper shader')

This will avoid deep indentation in the context of a larger program:

  -- create program, vs, and fs
  let
    (program', vs') = attachShader2 gl program vs
    (program'', fs') = attachShader2 gl program' fs
    program''' = linkProgram gl program''
  in do
    -- delete vs' and fs' and "return" program'''

vs

  -- create program, vs, and fs
  attachShader gl program vs $ \program', vs' =>
    attachShader gl program' fs $ \program'', fs' =>
      let
        program''' = linkProgram gl program''
      in do
        -- delete' vs and fs' and "return" program'''

AFAIK we still need continuations when creating resources, but at least that does not happen as often.

Now you may have noticed the little type argument in the JavaScript definition for the polymorphic function. This took me a while to figure out. When you have polymorphism, Idris code compiled to JS will pass the type (undefined in this case) to the function as the first argument. This makes perfect sense for a dependently typed language when you think about it, but was definitely a gotcha when receiving runtime "undefined is not a function" exceptions... not what you want when using a type-safe language. I am unsure if I can use quantitative types again in this case, but this time with 0 quantity, to remove this type argument at runtime; it certainly sounds like the purpose of erasure. Either way, this way of defining foreign functions seems rather off-spec, but I've decided to go with it anyway because of the effect on code readability.

I've learned a lot about linear typing in Idris, and not all that information is easy to find, but this log was never meant as a tutorial, so I will probably write one in the near future.

And now I have the boring task of redoing all my foreign function bindings to apply what I learned...