A simple example of dual client/server session types.

channel.idr

module Data.FSM.Channel
import Data.List
%default total

data Protocol : Type
where
  Out    : a -> Protocol -> Protocol
  In     : a -> Protocol -> Protocol
  Accept : Protocol -> Protocol -> Protocol
  Select : Protocol -> Protocol -> Protocol
  Empty  : Protocol

dual : Protocol -> Protocol
dual (Out x p)      = In x $ dual p
dual (In x p)       = Out x $ dual p
dual (Accept p1 p2)  = Select (dual p1) (dual p2)
dual (Select p1 p2) = Accept (dual p1) (dual p2)
dual Empty          = Empty

data Channel : (a:Type) -> Protocol -> (a -> Protocol) -> Type
where
  Send    : a -> Channel () (Out a remaining) (const remaining)
  Receive : Channel a (In a remaining) (const remaining)

  Choose  : (x:Bool) -> Channel () (Select p1 p2) (\r => if x then p1 else p2)
  Offer   : Channel Bool (Accept p1 p2) (\r => if r then p1 else p2)

  Return  : a -> Channel a Empty (const Empty)
  (>>=)   : Channel a p1 next -> ((x:a) -> Channel b (next x) finally) -> Channel b p1 finally

Server : Protocol -> Type -> Type
Server p a = Channel a p (const Empty)

Client : Protocol -> Type -> Type
Client p a = Channel a (dual p) (const Empty)

Addition : Protocol
Addition = In Nat $ In Nat $ Out Nat $ Empty

adder : Server Addition String
adder = do
  x <- Receive
  y <- Receive
  Send (x+y)
  Return $ "Added " ++ show x ++ " and " ++ show y ++ "."

addee : Nat -> Nat -> Client Addition String
addee x y = do
  Send x
  Send y
  sum <- Receive
  Return $ "The sum is " ++ show sum ++ "."

Negation : Protocol
Negation = In Nat $ Out Integer $ Empty

negator : Server Negation String
negator = do
  x <- Receive
  Send $ toIntegerNat x * -1
  Return $ "Negated " ++ show x ++ "."

Calculation : Protocol
Calculation = Accept Addition Negation

calculator : Server Calculation String
calculator = do
  x <- Offer
  case x of
    True  => adder
    False => negator

calculatee : Nat -> Client Calculation String
calculatee x = do
  Choose False
  Send x
  y <- Receive
  Return $ "The negation is " ++ show y ++ "."