ElixirST.ST (ElixirST v0.6.3) View Source

Manipulate Session Type (ST) data.

Session type definitions:

! = send
? = receive
& = branch (or external choice)
+ = (interal) choice

Session types accept the following grammar:

S =
    !label(types, ...).S
  | ?label(types, ...).S
  | &{?label(types, ...).S, ...}
  | +{!label(types, ...).S, ...}
  | rec X.(S)
  | X
  | end

Note: The session type end is optional, therefore !Hello() and !Hello().end are equivalent. X refers to to a variable which can be called later in a recursion operation. rec X.(S) refers to recursion, or looping - when X is called, it is replaced with the whole session type rec X.(S).

Some session types examples:

!Hello()                           # Sends {:Hello}

?Ping(number)                      # Receives {:Ping, value}, where values has to be a number

&{?Option1().!Hello(), ?Option2()} # Receive either {:Option1} or {:Option2}. If it
                                   # receives the former, then it sends {:Hello}. If it
                                   # receives {:Option2}, then it terminates.

rec X.(&{?Stop().end, ?Retry().X}) # The actor is able to receive multiple {:Retry},
                                   # and terminates when it receives {:Stop}.

Internal representation of session types take the form of the following structs:

  • %Send{label, types, next}
  • %Recv{label, types, next}
  • %Choice{choices}
  • %Branch{branches}
  • %Recurse{label, body}
  • %Call_Recurse{label}
  • %Terminate{}

The labels and types are of type label/0 and types/0, respectively. next, choices, branches and body have the type session_type/0.

Parser

Parses an input string to session types (as Elixir data).

Simple example

iex> s = "!Hello(Number)"
...> ElixirST.ST.string_to_st(s)
%ElixirST.ST.Send{label: :Hello, next: %ElixirST.ST.Terminate{}, types: [:number]}

Another example

iex> s = "rec X.(&{?Ping().!Pong().X, ?Quit().end})"
...> ElixirST.ST.string_to_st(s)
%ElixirST.ST.Recurse{
  label: :X,
  body: %ElixirST.ST.Branch{
    branches: %{
      Ping: %ElixirST.ST.Recv{
        label: :Ping,
        next: %ElixirST.ST.Send{label: :Pong, next: %ElixirST.ST.Call_Recurse{label: :X}, types: []},
        types: []
      },
      Quit: %ElixirST.ST.Recv{label: :Quit, next: %ElixirST.ST.Terminate{}, types: []}
    }
  }
}

Link to this section Summary

Types

Abstract Syntax Tree (AST)

Label for sending/receiving statements. Should be of the form of an atom.

Type for name and arity keys.

A session type list of session operations.

Session types when stored as tuples. Useful for when converting from Erlang records.

Native types accepted in the send/receive statements. E.g. !Ping(integer)

Functions

Returns the dual of the given session type.

Converts s session type to a string. To do the opposite, use string_to_st/1.

Converts the current session type to a string. E.g. ?Hello().!hi() would return ?Hello() only.

Converts a string to a session type. To do the opposite, use st_to_string/1.

Takes a session type (starting with a recursion, e.g. rec X.(...)) and outputs a single unfold of X.

Link to this section Types

Specs

ast() :: Macro.t()

Abstract Syntax Tree (AST)

Specs

label() :: atom()

Label for sending/receiving statements. Should be of the form of an atom.

Specs

name_arity() :: {label(), non_neg_integer()}

Type for name and arity keys.

Specs

session_type() ::
  %ElixirST.ST.Send{label: label(), next: session_type(), types: types()}
  | %ElixirST.ST.Recv{label: label(), next: session_type(), types: types()}
  | %ElixirST.ST.Choice{choices: %{required(label()) => session_type()}}
  | %ElixirST.ST.Branch{branches: %{required(label()) => session_type()}}
  | %ElixirST.ST.Recurse{
      body: session_type(),
      label: label(),
      outer_recurse: term()
    }
  | %ElixirST.ST.Call_Recurse{label: label()}
  | %ElixirST.ST.Terminate{}

A session type list of session operations.

Specs

session_type_tuple() ::
  {:send, atom(), [atom()], session_type_tuple()}
  | {:recv, atom(), [atom()], session_type_tuple()}
  | {:choice, [session_type_tuple()]}
  | {:branch, [session_type_tuple()]}
  | {:call, atom()}
  | {:recurse, atom(), session_type_tuple()}
  | {:terminate}

Session types when stored as tuples. Useful for when converting from Erlang records.

Specs

types() :: [
  :atom
  | :binary
  | :bitstring
  | :boolean
  | :exception
  | :float
  | :function
  | :integer
  | :list
  | :map
  | nil
  | :number
  | :pid
  | :port
  | :reference
  | :struct
  | :tuple
  | :string
]

Native types accepted in the send/receive statements. E.g. !Ping(integer)

Link to this section Functions

Specs

dual(session_type()) :: session_type()

Returns the dual of the given session type.

Changes that are made:

  • Receive <-> Send
  • Branch <-> Choice

Examples

iex> st_string = "!Ping(Number).?Pong(String)"
...> st = ElixirST.Parser.parse(st_string)
...> st_dual = ElixirST.ST.dual(st)
...> ElixirST.ST.st_to_string(st_dual)
"?Ping(number).!Pong(string)"
Link to this function

dual?(session_type1, session_type2)

View Source

Specs

dual?(session_type(), session_type()) :: boolean()
Link to this function

equal?(session_type1, session_type2)

View Source

Specs

equal?(session_type(), session_type()) :: boolean()
Link to this function

st_to_string(session_type)

View Source

Specs

st_to_string(session_type()) :: String.t()

Converts s session type to a string. To do the opposite, use string_to_st/1.

Examples

iex> s = "rec x.(&{?Hello(number), ?Retry().X})"
...> st = ElixirST.ST.string_to_st(s)
...> ElixirST.ST.st_to_string(st)
"rec x.(&{?Hello(number), ?Retry().X})"
Link to this function

st_to_string_current(session_type)

View Source

Specs

st_to_string_current(session_type()) :: String.t()

Converts the current session type to a string. E.g. ?Hello().!hi() would return ?Hello() only.

Examples

iex> s = "?Hello(number).?Retry()"
...> st = ElixirST.ST.string_to_st(s)
...> ElixirST.ST.st_to_string_current(st)
"?Hello(number)"

Specs

string_to_st(String.t()) :: session_type()

Converts a string to a session type. To do the opposite, use st_to_string/1.

Examples

iex> s = "?Ping().!Pong()"
...> ElixirST.ST.string_to_st(s)
%ElixirST.ST.Recv{
  label: :Ping,
  next: %ElixirST.ST.Send{label: :Pong, next: %ElixirST.ST.Terminate{}, types: []},
  types: []
}

Specs

unfold(session_type()) :: session_type()

Takes a session type (starting with a recursion, e.g. rec X.(...)) and outputs a single unfold of X.

Examples

    iex> st = "rec X.(!A().X)"
    ...> session_type = ElixirST.ST.string_to_st(st)
    ...> unfolded = ElixirST.ST.unfold(session_type)
    ...> ElixirST.ST.st_to_string(unfolded)
    "!A().rec X.(!A().X)"