Type level zero.

Type level successor. S n denotes (n+1).

Type level predecessor (only for internal use). P n denotes (n-1).

The class which covers type-level natural numbers.

Type level True.

Type level False.

Send v u denotes a protocol to emit a value of type v followed by a behavior of type u. Use of send on a channel changes its session type from Send v u into u.

Recv v u denotes a protocol of receiving a value of type v followed by a behavior of type u. Use of recv on a channel changes its session type from Recv v u into u.

Throw u1 u2 denotes a behavior to output of a channel with session type u1 followed by a behavior of type u2. Use of sendS on a channel changes its session type from Throw u1 u2 into u2.

Catch u1 u2 is the input of a channel with session type u1 followed by a behavior of type u2. Use of recvS on a channel changes its session type from Catch u1 u2 into u2.

Select u1 u2 denotes to be either behavior of type u1 or type u2 after emitting a corresponding label 1 or 2. Use of sel1 or sel2 on a channel changes its session type from Select u1 u2 into u1 or u2, respectively.

Offer u1 u2 denotes a behavior like either u1 or u2 according to the incoming label.

End denotes a terminated session. Further communication along a channel with type End cannot take place.

Bot is the type for a channel whose both endpoints are already engaged by two processes, so that no further processes can own that channel. For example, in forkIO (send k e) >>> recv k, k has type Bot.

Rec m r denotes recursive session, where m represents the binder of recursion variable. a type-level natural numer (like S Z). nesting level of Rec, and r is the body of the recursion which may contain Var m.

Recursion variable.

Close denotes a session that can do nothing but closing it.

Type-level snoc (reversed version of cons (:)). ss :> s denotes a list ss with s on its end. (FIXME:English)

Type-level empty list ([]).

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.

Bind (a.k.a >>=) operation for Session monad.

Unit (a.k.a return) operation for Session monad.

runS runs the Session. The pretype (see Session) must be Nil. The posttype must be Ended, i.e. all channels must be End.

Forall'd type variable t prevents abuse of use of channels inside different run. For example, new >>>= c -> io_ (runS ( ... send c ...) ) is rejected by the Haskell typechecker with error Inferred type is less polymorphic than expected.

The channel type. The type-level number n points to the session-type in type environments. For example, in the type Session t (Nil:>Send Int End) (Nil:>End) (), the usage of the channel c :: Channel t Z is Send Int End in pretype and End in posttype.

output a label `1'

output a label `2'

output a label `1'

start a new thread

Equality on type-level natural numbers. b ~ T if x == y. Otherwise b ~ F.

Computes subtraction of n by n' (FIXME:OK?)

Computes subtraction of n by n'

type-level &&

The class which covers session-type environments. The second parameter of the class denotes the length of the list.

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

For example, Pickup (End :> Bot :> Send Int End) Z t) is an instance of Pickup, and t is unified with Bot.

Note that the list counts from left to right. For example, The 0-th element of the list ((Nil :> 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.

The reversed version of Pickup which accesses lists in reversed order (counts from right to left). I.e., PickupR (End :> Bot :> Send Int End) Z (Send Int End) is an instance of PickupR.

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.

The reversed version of Update.

Ended n ss denotes that the session-type environment ss (the length of it is n) is Ended. The all elements in an Ended type environments are End.

IsEnded ss b denotes that b ~ T if ss is Ended, otherwise b ~ F. In other words, b ~ T if the all elements of ss are End

duality

sesion type algebra

pointwise extension of Comp -- FIXME: method

the specialized case for ended ss -- FIXME