The Session monad. ss and tt denotes the usage of channels.

• ss denotes pre-type, which denotes the type-level list of session types required to run the session.
• tt denotes post-type, which denotes the type-level lists of session types produced by the session.

t denotes a type-tag, which prevents abuse of use of channels. For detail, see runS.

Pickup ss n s denotes that the n-th element of the list ss is s. This type class plays an important role in session-type inference.

Formally, Pickup ss n s if s = pickup ss n where pickup is:

   pickup ss n = pickupR ss (len ss - (n+1))
     where pickupR (ss:>s) Z     = s
           pickupR (ss:>s) (S n) = pickupR ss n
           len Nil     = 0
           len (ss:>s) = (len ss) + 1

In other words, Pickup (End :> Bot :> Send Int End) Z End) is an instance of Pickup.

Note that the list counts from left to right. For example, The 0-th element of the list (End :> Bot) :> Send Int End is End.

Usually the list is accessed from the right end. The context

     SList ss (S n), Pickup (ss:>Bot:>Recv Char End) n s

is expanded into

     SList ss (S n), PickupR (ss:>Bot:>Recv Char End) (SubT (S n) (S n)) s, Sub (S n) (S n)

since SubT (S n) (S n) ~ Z, it will be reduced to

     PickupR (ss:>Bot:>Recv Char End) Z s

and then s is unified with Recv Char End.

Update ss n t ss' denotes that ss' is same as ss except that its n-th element is t. Formally, Update ss n t ss' if ss' = update ss n t where update is:

   update ss n t = updateR ss (len ss - (n+1)) t
     where updateR (ss:>_) Z     t = ss :> t
           updateR (ss:>s) (S n) t = updateR ss n t :> s
           len Nil     = 0
           len (ss:>s) = (len ss) + 1

In other words, Update (End :> Bot :> Send Int End) Z End (End :> Bot :> End)) is an instance of Update.

Note that the list counts from left to right, as in the case of Pickup.