In a previous question I discovered the existence of Conor McBride's Kleisli arrows of Outrageous Fortune while looking for ways of encoding Idris examples in Haskell. My efforts to understand McBride's code and make it compile in Haskell led to this gist: https://gist.github.com/abailly/02dcc04b23d4c607f33dca20021bcd2f
While searching on Hackage, I discovered several implementations of these concepts, notably by (guess who?) Edward Kmett and Gabriel Gonzalez.
What experience do people have putting such code in production? In particular, do the expected benefits (runtime safety, self-guiding usage) actually occur IRL? How about maintaining this kind of code over time and onboarding newcomers?
EDIT: I changed the title to be more explicit about what I am looking for: Real-world use of indexed monads in the wild. I am interested in using them and I have several use-cases in mind, just wondering if other people have already used them in "production" code.
EDIT 2: Thanks to the great answers provided so far and helpful comments, I edited that question's title and description again to reflect more precisely what kind of answer I expect, e.g. experience report.
I think the below should count as a practical example: statically enforcing "well-stackedness" in a compiler. Boilerplate first:
Then a simple stack language:
and we won't bother with real
Label
s:and
Prog
rams are just type-aligned lists ofOp
s:So in this setting, we can very easily make a compiler which is an indexed writer monad; that is, an indexed monad:
that allows accumulating a(n indexed) monoid:
just like regular
Writer
:So we just apply this machinery to
Prog
rams:and then we can try compiling a simple expression language:
and if we omitted e.g. one of the arguments to
BINOP
, the typechecker will detect this:Another nice example is mutexes with lock-unlock check at compile time. You can find this example on Stephen Diehl website:
http://dev.stephendiehl.com/hask/#indexed-monads
Session types are an attempt to give type-level descriptions to networking protocols. The idea is that if a client sends a value, the server must be ready to receive it, and vice versa.
So here's a type (using
TypeInType
) describing sessions consisting of a sequence of values to send and values to receive.a :! s
means "send a value of typea
, then continue with the protocols
".a :? s
means "receive a value of typea
, then continue with the protocols
".So
Session
represents a (type-level) list of actions. Our monadic computations will work their way along this list, sending and receiving data as the type demands it. More concretely, a computation of typeChan s t a
reduces the remaining work to be done to satisfy the protocol froms
tot
. I'll buildChan
using the indexed free monad that I used in my answer to your other question.Our base actions in the
Chan
monad will simply send and receive values.send
takes the current state of the session froma :! s
tos
, fulfilling the obligation to send ana
. Likewise,recv
transforms a session froma :? s
tos
.Here's the fun part. When one end of the protocol sends a value, the other end must be ready to receive it, and vice versa. This leads to the idea of a session type's dual:
In a total language
Dual (Dual s) = s
would be provable, but alas Haskell is not total.You can connect a pair of channels if their types are dual. (I guess you'd call this an in-memory simulation of connecting a client and a server.)
For example, here's a protocol for a server which tests whether a number is greater than 3. The server waits to receive an
Int
, sends back aBool
, and then ends the computation.And to test it:
Session types are an area of active research. This particular implementation is fine for very simple protocols, but you can't describe protocols where the type of the data being sent over the wire depends on the state of the protocol. For that you need, surprise surprise, dependent types. See this talk by Brady for a quick demo of the state of the art of session types.