DEV Community

DrBearhands
DrBearhands

Posted on • Originally published at drbearhands.com

2

Idris2+WebGL, part #10: 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'
Enter fullscreen mode Exit fullscreen mode

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'
     |              ^^^^^^^^^^^^^^^^^^
Enter fullscreen mode Exit fullscreen mode

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))))
Enter fullscreen mode Exit fullscreen mode

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)
Enter fullscreen mode Exit fullscreen mode

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
Enter fullscreen mode Exit fullscreen mode

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.

Google AI Education track image

Build Apps with Google AI Studio 🧱

This track will guide you through Google AI Studio's new "Build apps with Gemini" feature, where you can turn a simple text prompt into a fully functional, deployed web application in minutes.

Read more →

Top comments (0)

Google AI Education track image

Work through these 3 parts to earn the exclusive Google AI Studio Builder badge!

This track will guide you through Google AI Studio's new "Build apps with Gemini" feature, where you can turn a simple text prompt into a fully functional, deployed web application in minutes.

Read more →

👋 Kindness is contagious

Dive into this insightful article, celebrated by the caring DEV Community. Programmers from all walks of life are invited to share and expand our collective wisdom.

A simple thank-you can make someone’s day—drop your kudos in the comments!

On DEV, spreading knowledge paves the way and strengthens our community ties. If this piece helped you, a brief note of appreciation to the author truly counts.

Let’s Go!