Adaptation of the streaming library for increased safety through linear types. Summer of Haskell 2017 project in collaboration with Tweag I/O. My name is Edvard Hübinette, and I study computer science @ Chalmers University of Technology in Gothenburg, Sweden.
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 do-notation to plug-and-play, 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.
When adapting the streaming library for better type safety by leveraging
linearity, one particular set of functions has been, and still is, a major
issue: take, zip and everything based on them.
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
bind (>>=) to consume its first argument (disallowing multiple uses of
earlier stream references), effectively making the
previously shown
runtime errors impossible.
Linear types is closely related to linear logic, where the idea of value consumption is introduced, meaning a value is only valid for one use. In the 90’s, this was found a neat way to represent finite resources which is very interesting for programming languages; this viewpoint is well explained here.
. . .The streaming streams are simply an effectful sequence of values, followed by a result. Think list, but with the possiblility to run monadic actions to produce the values. From the generality of monads, this could be reading input
from keyboard, waiting for a server reply, asking some state, reading a mind,
et cetera.
My name is Edvard Hübinette, and I have gotten the opportunity to work with open-source Haskell during the upcoming months thanks to Summer of Haskell, an awesome initiative that funds a handful of students to work with Haskell over the summer. My project will focus on adapting the streaming library to use with a prototype version of GHC that supports linear types, in order to make it safer.
. . .