Idris2+WebGL, part #10: Implicit arguments & monad transformers
Tags: idris, functional, types
Published: 2021-02-16 11:15:17

---
title: Idris2+WebGL, part #10: Implicit arguments & monad transformers
tags: #Idris, #functional, #types
canonical_url: https://drbearhands.com/idris-webgl/part10/
series: Idris2 and WebGL
published: true
---

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:

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

```Haskell
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](https://gitlab.com/DrBearhands/idris-webgl/-/tree/fe8bd56b013caf000045788ea4d7580d089baff8/Control) 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:

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

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