The issues I am trying to tackle with
streaming are rooted in the fact
that usage of references to old stream states can repeat monadic effects
that was performed to yield earlier values. When solving this, the need
for a linear monad class arose. This would allow relying on the type
system to ensure that a monadic value can only be used once by forcing the
>>=) to consume its first argument (disallowing multiple uses of
earlier stream references), effectively making the
runtime errors impossible.
This was interesting because monads and their accompanied
very tightly coupled with Haskell as a language, but the GHC extension
-XRebindableSyntax allows quite some tinkering!
If you want to code along and tinker with the lollipops yourself, I helped the guys at Tweag I/O write a small guide to get started which can be found here.
First I defined the linear monad, because it is the monadic semantics that I need to stricten:
>>= is pretty straight forward: given a monadic value, we unwrap it,
apply it to a linear morphism once, and get a new monadic value. One of my
first hunches here was to use
(>>=) :: m a ⊸ (a -> m b) ⊸ m b which would
make the superclasses a lot less constrained, but unfortunately we need to
take in account that the
a here may also be some monadic value
a ~ Maybe Int, and particularly
a ~ Stream f m r). Allowing this
a -> m b would allow freely duplicating those
>> looks a bit more different than we are used to, and in particular very
restrictive! This is logical though, since the semantics of
>> is to perform
a computation and throw away the result, something not very linear at all.
Therefore it only makes sense to blind something that does not produce
results, namely values of type
pure from a linear
Applicative because I want to keep the
heritage line of subclasses:
Functor > Applicative > Monad (this is why I
ap, which will be clear in a moment). Let’s follow the types
and see where this takes us for the superclasses!
Now we want to define of a linear Applicative, which is already somewhat
constrained from the types of
LMonad. We know from the monad laws that
Monad should relate through these two equations:
…which already hints us with the correct types for
Here we get the types for
ap for free from the above laws,
since they need to be the same as for their
<* we face the same restrictions as for
LMonad: we cannot
throw away values! If we do not respect this, we cannot use
operations on any
LMonad, because they will break the linearity constraints.
Hence, the only reasonable approach is to only allow replacing values of type
Worth noting if you are hacking along is that
preludeone, but a linear counterpart. This is a returning problem at the moment; since the linearity checker does not infer linearity if not explicitly told so, instead it assumes functions to be unrestricted which leads to
hey, this variable should be treated linearly-errors. This is explained further in the readme linked in the introduction.
Now let’s take a look where this leads us for the
It would sure be nice to have
fmap :: (a ⊸ b) -> f a ⊸ f b (note the regular
arrow), letting us transform all values in the functor with a single linear
function. But unfortunately that would not allows us to use
fmap on linear
monads, because it will have an unrestricted (nonlinear) type! The linearity
checker cannot allow this, because it is not sure the values are treated
linearly. So we are confined to:
Here we almost have the good old
fmap, but with a linear transformation
which can only be applied once. For
(<$) the same logic applies as for
LApplicative: we can’t throw away values, so the only values we can replace
are values of type unit.
It sounds crippling, but as it turns out this does not seem to be the end of
the world. For example, the functor that is used for representing the shape of
streamed elements in the
streaming prelude looks like this:
b is the end-of-stream value. …hey, that isn’t half bad:
only applied to a single value, but the functor can hold any type of values in
a! To solve the problems with streaming we want to
constrain the effects of the stream, usually we don’t care about the
linearity of the values. So, since we in this context don’t really care
about linearity in
a, we might as well just make it unrestricted (note the
regular arrow in the constructor):
With this definition of a partly-linear
Of we can even use the same
Functor instance (with the above default implementation of
(<$)) and be
on our way!
I was promised extension hacking!
Ah yes, so how can we use these without having to resort to
less-than-stellar-readability code with qualified infix operators
mixed with crazy lambdas everywhere? Say hi to
little gem of an extension allows you to rebind much of the Haskell syntax
to your own definitions (pretty well explained in further detail
a neat advent calendar with a new GHC extension every day).
So everything we need to do to actually use our new and shiny monad is to hide
return from prelude, activate the extension, import
our monad class and do-notation works magically out of the box:
The example is taken from my linear streaming fork.
This extension is very clever and enables friction-free use of whatever
definition you want to use for
return (other syntactic
Thanks for reading! If you would like to discuss the content, feel free to drop a comment in the Reddit thread.