ElixirSessions

ElixirSessions applies Session Types to the Elixir language. It statically checks that the programs use the correct communication structures (e.g. send/receive) when dealing with message passing between actors. It also ensures that the correct types are being used. For example, the session type ?Add(number, number).!Result(number).end expects that two numbers are received (i.e. ?), then a number is sent (i.e. !) and finally the session terminates.

Installation

If available in Hex, the package can be installed by adding elixirsessions to your list of dependencies in mix.exs:

def deps do
  [
    {:elixirsessions, "~> 0.2.0"}
  ]
end

Documentation can be generated with ExDoc and published on HexDocs. Once published, the docs can be found at https://hexdocs.pm/elixirsessions.

Example

To session typecheck files in Elixir, add use STEx and include any assertions using @session (or @dual) attributes preceding any def functions. The following is a simple example:

defmodule Examples.SmallExample do
  use STEx

  @session "server = ?Hello()"
  @spec server(pid) :: atom()
  def server(_pid) do
    receive do
      {:Hello} -> :ok
    end
  end

  @dual "server"
  @spec client(pid) :: {atom()}
  def client(pid) do
    send(pid, {:Hello})
  end
end

ElixirSessions runs automatically at compile time (mix compile) or as a mix task (mix session_check (module)):

$ mix session_check Examples.SmallExample
[info]  Session typechecking for client/1 terminated successfully
[info]  Session typechecking for server/0 terminated successfully

If the client sends a different label (e.g. :Hi) instead of the one specified in the session type (i.e. @session "!Hello()"), ElixirSessions will complain:

$ mix session_check Examples.SmallExample
[error] Session typechecking for client/1 found an error. 
[error] [Line 7] Expected send with label :Hello but found :Hi.

Session Types in Elixir

Session types are used to ensure correct communication between concurrent programs. Some session type definitions: ! refers to a send action, ? refers to a receive action, & refers to a branch (external choice), and + refers to an (internal) choice.

Session types accept the following grammar and types:

S =
    !label(types, ...).S            (send)
  | ?label(types, ...).S            (receive)
  | &{?label(types, ...).S, ...}    (branch)
  | +{!label(types, ...).S, ...}    (choice)
  | rec X.(S)                       (recurse)
  | X                               (recursion var)
  | end                             (terminate)

types =
  atom
  | boolean
  | number
  | pid
  | nil
  | binary
  | {types, types, ...}             (tuple)
  | [types]                         (list)

The following are some session type examples along with the equivalent Elixir code.

send(pid, {:Hello})

receive do
  {:Ping, value} -> value
end

&{ 
  ?Option1().!Hello(number), 
  ?Option2()
 }

receive do
  {:Option1} -> send(pid, {:Hello, 55})
                # ...
  {:Option2} -> # ...
end

def rec() do
  receive do
    {:Stop}  -> # ...
    {:Retry} -> rec()
  end 
end

Using ElixirSessions

To session typecheck a module, insert this line at the top:

use STEx

Insert any checks using the @session attribute followed by a function that should be session type checked, such as:

@session "pinger = !Ping().?Pong()"
def function(), do: ...

The @dual attribute checks the dual of the specified session type.

@dual "pinger"
# Equivalent to: @session "?Ping().!Pong()"

Other examples can be found in the examples folder.

Acknowledgements

Some code related to Elixir expression typing was adapted from typelixir by Cassola (MIT licence).