Session Types are cool

I just read a tutorial on Session Types. Session Types are a means for statically verifying a protocol between two (or with the new release, more) parties. It is what Erlang’s type system would be if Erlang had a type system.

The tutorial is very good, so I won’t belabor the point by reintroducing them here, but here’s a little teaser. Let’s say you have two processes, implemented like so:

process1 = do
    x <- recv
    y <- recv
    send (x + y)
process2 = do
    send 42
    x <- recv
    send (x + 1)

The session types library can verify at compile time that these two processes cannot talk to each other, since process1 is expecting to receive two integers but process2 only sends one before expecting to receive something.

Therefore, I conclude that Haskell is better than Erlang. Please ignore the fact that Haskell is missing the important things about Erlang (fault tolerance, hot swapping, total serialization). :-)

A quick glance at the automatically generated documentation for the session types library will cause you to go blind1. It is this kind of brilliant hackery which makes me really want a good dependently-typed language, since this kind of thing shouldn’t have to be brilliant hackery. It should be standard, everyday stuff.

1Oh, did you already click on it? I’m sorry, but I can deduce that you have since regained it.


8 thoughts on “Session Types are cool

  1. Well that’s fantastic… I skimmed through the tutorial and the examples don’t look like yours. Is it possible to use the “do” syntax like you did instead of ~>>= / ~>> as is done for “normal” monads?

  2. No, that was just for expository purposes. The ~>>= thing ain’t too bad though; they’re just like fat semicolons:

    process1 =
        recv ~>>= \x ->
        recv ~>>= \y ->
        send (x + y)

    The main thing I don’t like about that contortion is that the variables are on the right of their actions. But then again, I believe some variations of BASIC even did that, so it must be possible to get used to it.

    You might be able to hack the do notation to work using GHC’s -fno-implicit-prelude, but it would be a pain.

  3. So I’m guessing it’s not possible to implement this as monads, right? (I didn’t look at the implementation so this is probably a stupid question… but I guess if it was possible, it would be done, so that one would be able to make use of the “do” notation).

  4. Well, it is implemented as a monad, just not as the Prelude’s Monad. It is easy to see that it cannot be either.

    The example in the post, desugared, is: send 42 >> fmap succ recv, which is not well-typed wrt process1 (meaning run would fail to type when given both of them). However, send 1 >> send 2 >> fmap succ recv would be well-typed. But the type of send 42 is the same as the type of send 1 >> send 2, by the definition of (>>), so there’s no way one would be well-typed and the other one not.

    As with women, you must look beyond appearance to see beauty in session types.

  5. LOL! I guess I’ll have to go and read the tutorials now :)

    Maybe template haskell could be of help here? Beauty on the inside *and* on the outside is even better :P

  6. Just curious, but what part do you think should be the everyday stuff: the way that Session Types were done, or the ST’s themselves? Or both? :)

  7. Kind of both. More like in between.

    I see code as a (multi-layered) interplay between form and content. At the bottom, the language you are using is the form, and the code you are writing is the content. Your code can fail to compile, and that’s because you made a mistake that the compiler was capable of catching.

    But I’ve always tried to take it further. I’ve mostly failed, but to keep my ego I blame it on poor language support. Session types are one example of taking it further: here the form is session types, and the content is particular session functions. But particular session functions can fail to compile, because they failed to comply to the form, because they were incorrect according to your form.

    Software is full of these interplays, but very seldom are they made, er, formal. Object-oriented programming does this to some extent, with base classes or interfaces providing the form. But OO is a weak form specification tool, and dependent type research shows that very strong ones do exist. What I want to do is to meet somewhere in the middle. I don’t know what that looks like, I just know that it needs to be stronger than OO, and dependent types aren’t the right answer in their state of the art (I can’t put my finger on why that is… my best answer is “they’re too hard”).

    Be careful what you ask for, you might get a long-winded reply.

Leave a Reply

Fill in your details below or click an icon to log in: Logo

You are commenting using your account. Log Out /  Change )

Google+ photo

You are commenting using your Google+ account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )


Connecting to %s