System.Concurrency.Session(source)

Definitions

data Session : Type

  A session type describes the interactions one thread may have with
  another over a shared bidirectional channel: it may send or receive
  values of arbitrary types, or be done communicating.

Totality: total
Visibility: public export
Constructors:

Send : Type -> Session -> Session

Recv : Type -> Session -> Session

End : Session

Dual : Session -> Session

  Dual describes how the other party to the communication sees the
  interactions: our sends become their receives and vice-versa.

Totality: total
Visibility: public export

dualInvolutive : (s : Session) -> Dual (Dual s) = s

  Duality is involutive: the dual of my dual is me

Totality: total
Visibility: export

data Seen : Nat -> Nat -> (Session -> Session) -> Type

  The inductive family (Seen m n f) states that the function `f`
  was obtained by composing an interleaving of `m` receiving
  steps and `n` sending ones.

Totality: total
Visibility: public export
Constructors:

None : Seen 0 0 id

Recv : (ty : Type) -> Seen m n f -> Seen (S m) n (f . Recv ty)

Send : (ty : Type) -> Seen m n f -> Seen m (S n) (f . Send ty)

record Channel : Session -> Type

  A (bidirectional) channel is parametrised by a session it must respect.
  
  It is implemented in terms of two low-level channels: one for sending
  and one for receiving. This ensures that we never are in a situation
  where a thread with session (Send Nat (Recv String ...)) sends a natural
  number and subsequently performs a receive before the other party
  to the communication had time to grab the Nat thus receiving it
  instead of a String.
  
  The low-level channels can only carry values of a single type. And so
  they are given respective union types corresponding to the types that
  can be sent on the one hand and the ones that can be received on the
  other.
  These union types are tagged unions where if `ty` is at index `k` in
  the list of types `tys` then `(k, v)` is a value of `Union tys` provided
  that `v` has type `ty`.
  
  `sendStep`, `recvStep`, `seePrefix`, and `seen` encode the fact that
  we have already performed some of the protocol and so the low-level
  channels' respective types necessarily mention types that we won't
  see anymore.

Totality: total
Visibility: export
Constructor: 

MkChannel : (0 _ : Seen recvStep sendStep seenPrefix) -> Channel (Union (SendTypes (seenPrefix s))) -> Channel (Union (RecvTypes (seenPrefix s))) -> Channel s

Projections:

.recvChan : ({rec:0} : Channel s) -> Channel (Union (RecvTypes (seenPrefix {rec:0} s)))

.recvStep : Channel s -> Nat

0 .seen : ({rec:0} : Channel s) -> Seen (recvStep {rec:0}) (sendStep {rec:0}) (seenPrefix {rec:0})

0 .seenPrefix : Channel s -> Session -> Session

.sendChan : ({rec:0} : Channel s) -> Channel (Union (SendTypes (seenPrefix {rec:0} s)))

.sendStep : Channel s -> Nat

recv : LinearIO io => Channel (Recv ty s) -@ L1 io (Res ty (const (Channel s)))

  Consume a linear channel with a `Recv ty` step at the head of the
  session type in order to obtain a value of type `ty` together with
  a linear channel for the rest of the session.

Totality: total
Visibility: export

send : LinearIO io => (1 _ : Channel (Send ty s)) -> ty -> L1 io (Channel s)

  Consume a linear channel with a `Send ty` step at the head of the
  session type in order to send a value of type `ty` and obtain a
  linear channel for the rest of the session.

Totality: total
Visibility: export

end : LinearIO io => Channel End -@ L io ()

  Discard the channel provided that the session has reached its `End`.

Totality: total
Visibility: export

makeChannel : LinearIO io => (0 s : Session) -> L1 io (LPair (Channel s) (Channel (Dual s)))

  Given a session, create a bidirectional communication channel and
  return its two endpoints

Totality: total
Visibility: export

fork : (0 s : Session) -> (Channel s -@ L IO a) -@ ((Channel (Dual s) -@ L IO b) -@ L IO (a, b))

  Given a session and two functions communicating according to that
  session, we can run the two programs concurrently and collect their
  final results.

Totality: total
Visibility: export