Working with linearly typed Haskell has been really interesting, and I have
leveraged a linear monad
for much of my endeavours. This has been neat in combination with
XRebindableSyntax
to get donotation to plugandplay, but not everything
has been a smooth experience. In this post I will discuss a few of the
annoying usability issues that have surfaced when working with linear types in a
practical setting.
Broken flow control
There are some issues with flow control when using the linear extension.
Albeit a temporary problem, there is no linear case
and let
implemented
yet. This means that even if you thread your things linearly through these
constructs, they will lead to errors because the linearity checker sees you
passing a linear variable to an unrestricted context:
Both these examples will work eventually, and linear versions of both case
and let
will indeed be implemented later. For now, one can work around these
hurdles through adding where
functions and doing the case
logic through
pattern matching there. There are a few silly constraints like that, but
also real problems so let’s take a look at a few of those.
Mixing monad classes
So, XRebindableSyntax
made using a redefined monad a real hoot. Until you
need to mix different kinds of monads in the same module… Then you run into
trouble, because the do
notation can only be bound to the functions of one
of the monad classes and the others need to use qualified infix monadic
operators. This could be a common issue, because you possibly do not care
about linearity everywhere, but only in parts of your code. When
do
notation only works for one of your monads, you have a few unsatisfactory
choices like:

Figure out which of your monads you need to write the simplest code for, then write that without
do
notation using qualified infix monadic operators in a sea of lambdas. This only to later realise that it got more complex than you anticipated, so you change your mind and have to rewrite that code indo
notation and change the other code to qualified infix riddled spaghetti instead. 
Split up a logically sound module into two separate ones, one for linear and one for unrestricted code. Then you get screwed over by recursive dependencies, confused by your own code base and/or bullied in code review.
A solution approach
It should be possible to solve this issue by creating a sort of “monad umbrella”, allowing different multiplicity monads to share a common interface. This could then be used for functions that want to support all of them. I have been trying hard (with excellent help from the guys at Tweag) to write a proper implementation that the type checker accepts, using a plethora of different approaches, but in vain. Anyway, this sketch should show you the idea:
If we made something like this, we could bind the do
notation to the
functions provided by MonadWithWeight
and automagically get the correct
implementation depending on which monad we are currently typed with! Cool.
Though, this does not actually work, which could be from fundamental limits in
the compiler. It is a bit early to speculate but we did it anyway; our best
guess is that the type of >>=
is inferred in isolation, and rebindabledo
requires it to have a function type. So even if GHC unfolds the type family
early enough, >>=
doesn’t in isolation have a specified multiplicity and
hence not yet a decided function arrow.
A temporary workaround
While the above solution would definitely be better, there is actually a
working solution, but it’s not very pretty: pack your favourite monad in a
record and take it with you! Unpack it and override do
notation locally,
both practical and fun:
The reason this works is that we don’t pollute the global scope with different
monadic operators, but hide them in a function returning a record type. This
allows us to import that function globally and unpack them from the record
locally where we need them, shadowing the operators only in the scope of that
where
clause!
It is worth noting that this is not specific to linear things but rather the
XRebindableSyntax
extension overall, possibly contributing to its seemed
unpopularity. This might be a reason for indexed and relative monads not
seeing so much use either, since the handling of syntax gets so clunky.
Multiplicity polymorphism for monads
How can we get functions to work with both linear and nonlinear abstractions?
To solve the issues with repeatable effects in the streaming
library, I
redefined it to work with the linear monad. This is great and all, but now the
code only supports linear monads and no longer the good ol’ unrestricted
monad. It would be practical to be able to write functions on monads with
different multiplicity constraints, otherwise we will have to write lots of
duplicate code to support the different monads! Unfortunately, general
multiplicity polymorphism requires a lot more work, and will likely not happen
before the monomorphic linear types are merged.
IfThenElse
The arguaby nastiest issue is related to the ifthenelse
construct, and is
much worse than case
and let
. The core syntax is implemented linearly,
but clashes with XRebindableSyntax
; as soon as this extension is activated,
the internal ifthenelse
goes out of scope and you have to provide an
implementation of ifThenElse :: a > b > c > d
yourself. As you can see,
XRebindableSyntax
assumes this is the type we need, an assumption not
compatible with linear types. This is really bad news, because the linear
ifThenElse
has a different type and different semantics, that
cannot be implemented as a user.
The consequence of this is that merely by activating a compiler extension,
previously legitimate code ceases to be able to compile, which is horrible
since we straight up lose welltyped code. Adding insult to injury, there is
even no way to reconcile the two different types, so an internal fix of this
for linearity would just reverse the issue by causing the same problems for
the regular, less constrained ifThenElse
.
Thanks for reading! Feel free to drop a comment in the reddit discussion thread!