Implicit arguments & monad transformers

I found something interesting while implementing existentially quantified phantom types as explained in my last log entry. Note the last line of the createProgram function:

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

public export
programCont : ProgramStatus -> Type -> Type
programCont s a = (1 _ : forall p . (1 _ : Program p s) -> a) -> a

export
createProgram : MonadLState GLContext m => m (programCont Unlinked a)
createProgram =
  state $ \gl =>
    prim__createProgram gl $ \prog, gl' =>
      (\f => f $ MkProgram { p=() } prog) # gl'

The MkProgram constructor, in its definition, appears to only take an AnyPtr as argument. In actuality, it also needs to know the type values for p and s in order to construct a Program p s. These arguments are implicit. In most common cases the values p and s can be derived from context, but not always, and not on this line. We need to specify the value for p, set to the unit type in this case. Without it, we get the following error:

Error: Unsolved holes:
JSFFI.WebGL2.{p:1210} introduced at:
JSFFI/WebGL2.idr:309:14--309:32
     |
 309 |       (\f => f $ MkProgram prog) # gl'
     |              ^^^^^^^^^^^^^^^^^^

Knowledge that p=() is lost outside the scope of the function, so we retain the functionality of using p as an existential type.

In contrast, Haskell is fine with leaving a phantom type unspecified:

glCreateProgram :: MonadGL m => GLIO m s s (ProgramContinuation i)
glCreateProgram = LessSafe.glCreateProgram >>= (\prog -> return (ProgCont (\f -> f (Program prog))))

Where Program is a similar constructor with unknown phantom type. Perhaps Haskell’s type checker is more advanced, but I expect having types as first class citizens inevitably requires more specificity.

In this particular case the implicit argument is hidden in a fairly deep layer of code so I’m not concerned, but “unresolved holes” have started popping up more and more, and I’m not really happy about having to specify what applicative I intend to use on every other use of pure.

I’ll see how this develops, particularly after cleaning up the code base.

Speaking of cleaning up the code base, I failed to realize in part 6 that the specialized monads I use to replace IO, and really even IO itself, are just linear variants of the State monad. So I made a linear state monad transformer. The code is pretty straightforward if you’re familiar with monad transformers and linear types, so I won’t post it here. Here’s the repository at the relevant commit if you want to check it out yourself.

The change took a while but was pretty good for code quality. I no longer need to define weird lifting functions for specialized monads (like GL and Alloc). It’s just:

Graphics : Type -> Type
Graphics =
  LStateT Allocator (LState GLContext)

and things just work.

An interesting problem is how to deal with errors. My current approach is to return linear variants of Either, but that has a big problem: a sum of a linear value is not a linear monad or functor. Consider the following:

public export
data LResult : Type -> Type -> Type where
  Err : (_ : e) -> LResult e a
  Ok : (1 _ : a) -> LResult e a


export
LFunctor (LResult e) where
  map fn res = case res of
    Err e => Err e
    Ok val => Ok $ fn val

This code will not type check! In the map function, fn is linear, but it is not consumed in the Err case branch. That’s not allowed.

We can still use LResult as a return type without relying on monadic composition, but the resulting code will be far more nested. Our happy flow will become contaminated with edge-case handling… not the best.

Apparently the author of Idris has already considered the problem of error handling in conjunction with linear types and has a solution, which I look forward to reading about and sharing next time.

overview