> {-# LANGUAGE RebindableSyntax, TypeOperators, DataKinds, KindSignatures, PolyKinds, TypeFamilies, ConstraintKinds, NoMonomorphismRestriction, MultiParamTypeClasses, FlexibleInstances, FlexibleContexts, DeriveDataTypeable, StandaloneDeriving, ExistentialQuantification, RankNTypes, UndecidableInstances, EmptyDataDecls, ScopedTypeVariables, GADTs, InstanceSigs, ImplicitParams, IncoherentInstances #-}

> module Control.Effect.Sessions.Process where

> import Control.Concurrent ( threadDelay )
> import qualified Control.Concurrent.Chan as C
> import qualified Control.Concurrent as Conc

> import qualified Prelude as P
> import Prelude hiding (Monad(..),print)

> import Control.Effect 
> import GHC.TypeLits
> import Unsafe.Coerce
> import GHC.Prim

> import Data.Type.FiniteMap
> import Data.Type.Set (Sort)

> -- Needed when you are using RebindableSyntax extension [most of the time]
> ifThenElse True e1 e2 = e1
> ifThenElse False e1 e2 = e2
The baseis of the session calculus encoding in Haskell is: * the encoding of session types into an effect system as described in Section 7 * using a Haskell implementation of /graded monads/ to embed effect systems (follows the technique in 'Embedding effect systems in Haskell', Orchard, Petricek, Haskell Symposoium 2014) Processes are captured by the following data type which wraps the IO monad and which is indexed a type-level finite map from names to session types: 
> {-| Process computation type indexed by an environment of the (free) channel
>     names used in the computation, paired with a specification of their behaviour. -}
> data Process (s :: [Map Name Session]) a = Process { getProcess :: IO a }
The type index represents a finite map of channel-session-type pairs as a type-level list. This treated as a finite map when taking 'union' of two maps, where duplicate mappings get merged by sequential session composition. Session types are given by the data type: 
> {-| Session types -}
> data Session = 
>                {-| Send -}
>                forall a . a :! Session 
>                {-| Receive -}
>              | forall a . a :? Session 
>                {-| Output -}
>              | forall a . a :*! Session
>                {-| Alternation (for branch/select) -}
>              | Session :+ Session
>               {-| Marks a session that should 'balance' when composed -}
>              | Bal Session
>               {-| End of session -}
>              | End
>               {-| Denotes an affine fixed point, where Fix a b = a* . b -} 
>              | Fix Session Session     
>               {-| A placeholder for a recursion variable- never generated by
>                  the encoding or produced by any operation, but set as 
>                  the session type for a recursive call in a fixed-point (see `affineFix`).  -}
>              | Star     

> {-| Delegated session -}
> data Delegate = Delg Session           

> {-| Duality function: calculuate the dual of a simple, non-recursive session type -}
> type family Dual s where
>     Dual End       = End
>     Dual (t :! s)  = t :? (Dual s)
>     Dual (t :*! s) = t :? (Dual s) 
>     Dual (t :? s)  = t :! (Dual s)
>     Dual (s :+ t)  = (Dual s) :+ (Dual t)
>     Dual (Bal t)   = Dual t
>     Dual Star      = Star
>     -- Dual (Fix a b) is not computed here, only duality of non-recursive sessions

> {-| Duality relation: extends the duality function to include recursive session types -}
> type family DualP (s :: Session) (t :: Session) :: Constraint where
>             DualP End End             = ()
>             DualP (t :! s) (t' :? s') = (t ~ t', DualP s s')
>             DualP (t :? s) (t' :! s') = (t ~ t', DualP s s')
>             DualP (Bal s) s'          = DualP s s'
>             DualP s (Bal s')          = DualP s s'
>             DualP (s :+ t) (s' :+ t') = (DualP s s', DualP t t')
>             DualP (Fix a b) s         = EqFix a (Fix a b) (Dual s)
>             DualP s (Fix a b)         = EqFix a (Fix a b) (Dual s)

> {-| Compute fixed-point equality of session types by unrolling -}
> type family EqFix (f :: Session) (f' :: Session) (s :: Session) :: Constraint where
>             EqFix a (Fix Star b) b                  = ()
>             EqFix a (Fix Star b) s                  = EqFix a (Fix a b) s
>             EqFix a (Fix (t :! s) b) (t' :! s')     = (t ~ t', EqFix a (Fix s b) s')
>             EqFix a (Fix (t :? s) b) (t' :? s')     = (t ~ t', EqFix a (Fix s b) s')
>             EqFix a (Fix (t1 :+ t2) b) (t1' :+ t2') = (t1 ~ t1', t2 ~ t2')
>             EqFix a (Fix (t :*! s) b) (t' :*! s')   = (t ~ t', EqFix a (Fix s b) s')

> {-| Predicate over environments that channel 'c' has dual endpoints with dual session types -}
> type Duality env c = DualP (env :@ (Ch c)) (env :@ (Op c))
A specialised version of the usual 'Lookup' that replies 'End' if the key doesn't exist in the map. 
> {-| Lookup a channel from an enrivonment, returning 'End' if it is not a member -}
> type family (:@) (m :: [Map Name Session]) (c :: Name) :: Session where
>             '[]              :@ k = End
>             ((k :-> v) ': m) :@ k = v
>             (kvp ': m)       :@ k = m :@ k
The 'Combine' type family is used by the 'Union' function on finite sets when there are two matching keys in each map. It determines the new value in the resulting map, which in this case is defined by sequational composition of session types. 
> type instance Combine s t = SessionSeq s t

> {-| Sequential composition of sessions -}
> type family SessionSeq s t where
>             SessionSeq End s        = s
>             SessionSeq (a :? s) t   = a :? (SessionSeq s t)
>             SessionSeq (a :! s) t   = a :! (SessionSeq s t)
>             SessionSeq (a :*! s) t   = a :*! (SessionSeq s t)
>             SessionSeq (s1 :+ s2) t  = (SessionSeq s1 t) :+ (SessionSeq s2 t)
>             SessionSeq Star Star     = Star

> {-| Channel endpoint names -}
> data Name = Ch Symbol | Op Symbol
> {-| Namec channels, encapsulating Concurrent Haskell channels -}
> data Chan (n :: Name) = forall a . MkChan (C.Chan a)
Channel names can be compared as follows (this is needed for the normalisation procedure in the type-level finite maps library). 
> {-| Compare channel names for normalising type-level finite map representations -}
> type instance Cmp (c :-> a) (d :-> b) = CmpSessionMap (c :-> a) (d :-> b)

> {-| Compare channel names for normalising type-level finite map representations -}
> type family CmpSessionMap (x :: Map Name Session) (y :: Map Name Session)  where
>     CmpSessionMap ((Ch c) :-> a) ((Op d) :-> b) = LT
>     CmpSessionMap ((Op c) :-> a) ((Ch d) :-> b) = GT
>     CmpSessionMap ((Ch c) :-> a) ((Ch d) :-> b) = CmpSymbol c d
>     CmpSessionMap ((Op c) :-> a) ((Op d) :-> b) = CmpSymbol c d
We then define the effect-graded monads (in the style of Katusmata) for sessions, an instance of 'Effect' class from Control.Effect.Monad (see https://hackage.haskell.org/package/effect-mon:ad-0.6.1/docs/Control-Effect.html). 
> type UnionSeq s t = Union s t -- to remind us that the `union' is more like 
>                          -- sequential composition
> instance Effect Process where
>    type Plus Process s t = UnionSeq s t
>    type Unit Process     = '[]
>    type Inv Process s t  = Balanced s t

>    return :: a -> Process (Unit Process) a
>    return a = Process (P.return a)

>    (>>=) :: (Inv Process s t) => Process s a -> (a -> Process t b) -> Process (Plus Process s t) b
>    x >>= k = Process ((P.>>=) (getProcess x) (getProcess . k))

> fail = error "Fail in a process computation"

> {-| Normalises session types using the left-distributivity 
>      rule for effects: i.e. f * (g + h) = (f * g) + (f * h) -}
> type family DistribL g where
>             DistribL (a :! (s :+ t)) = (DistribL (a :! s)) :+ (DistribL (a :! t))
>             DistribL (a :? (s :+ t)) = (DistribL (a :? s)) :+ (DistribL (a :? t))
>             DistribL (a :? s) = DistribInsideSeq ((:?) a) (DistribL s)
>             DistribL (a :! s) = DistribInsideSeq ((:!) a) (DistribL s)
>             DistribL (a :+ b) = (DistribL a) :+ (DistribL b)
>             DistribL Star = Star
>             DistribL End = End

> {-| Part of the normalisation procedure for left-distributivity -}
> type family DistribInsideSeq (k :: Session -> Session) (a :: Session) :: Session where
>             DistribInsideSeq k (s :+ t) = (k s) :+ (k t)
>             DistribInsideSeq k s        = k s

> {-| Map an affine equation on effects to the fixed point solution: 
>    That is '(Seq Star a) :+ b' where 'Star' is the placeholder for a recursion variable
>     then 'ToFix ((Seq Star a) :+ b) = Fix a b' -}
> type ToFix s = ToFixP (DistribL s)

> type family ToFixPP (a :: Session) (a' :: Session) (b :: Session) (b' :: Session) :: Session where
>             ToFixPP a (t :! s) b b' = ToFixPP a s b b'
>             ToFixPP a (t :? s) b b' = ToFixPP a s b b'
>             ToFixPP a End      b b' = ToFixPP b b' a End
>             ToFixPP a Star b b'     = Fix a b
>             ToFixPP a a' b Star     = Fix b a

> type family ToFixP s where
>             ToFixP (a :+ b) = ToFixPP a a b b
>             ToFixP s        = ToFixPP s s End End

> type family ToFixes (env :: [Map Name Session]) :: [Map Name Session] where
>             ToFixes '[] = '[]
>             ToFixes ((c :-> v) ': env) = (c :-> ToFix v) ': env

> {-| Predicate for checking that two environments are balanced 
>      (in context of sequential composition) -}
> type family (Balanced s t) :: Constraint where
>                   Balanced '[] '[] = ()
>                   Balanced env '[] = ()
>                   Balanced '[] env = ()
>                   Balanced ((c :-> s) ': env) env' = (BalancedF (c :-> s) env', Balanced env env')

> {-| Side recursive case of balancing (check each var -> session type map against every other -}
> type family (BalancedF s t) :: Constraint where
>                   BalancedF (c :-> s) '[]                          = ()
>                   BalancedF (Ch c :-> s) ((Op c :-> Bal t) ': env) = (t ~ Dual s)
>                   BalancedF (Op c :-> s) ((Ch c :-> Bal t) ': env) = (t ~ Dual s) 
>                   BalancedF (Ch c :-> Bal s) ((Op c :-> t) ': env) = (t ~ Dual s)
>                   BalancedF (Op c :-> Bal s) ((Ch c :-> t) ': env) = (t ~ Dual s)
>                   BalancedF (c :-> s) ((c :-> t) ': env)           = (NotBal s, NotBal t)
>                   BalancedF (c :-> s) ((d :-> t) ': env)           = BalancedF (c :-> s) env

> {-| Checks that we are not requiring a balanced session -}
> type family (NotBal s) :: Constraint where
>     NotBal (s :! t) = ()
>     NotBal (s :? t) = ()
>     NotBal (s :+ t) = ()
>     NotBal (s :*! t) = ()
>     NotBal Star = ()
>     NotBal End = ()

> {-| Predicate for checking that two environments are balanced 
>       (in the context of parallel composition) -}
> type family (BalancedPar s t) :: Constraint where
>                   BalancedPar '[] '[] = ()
>                   BalancedPar env '[] = ()
>                   BalancedPar '[] env = ()
>                   BalancedPar ((c :-> s) ': env) env' = (BalancedParF (c :-> s) env', BalancedPar env env')

> {-| Side recursive case of balancing for par (check each var -> session type map against every other -}
> type family (BalancedParF s t) :: Constraint where
>                   BalancedParF (c :-> s) '[]                      = ()
>                   BalancedParF (Ch c :-> s) ((Op c :-> t) ': env) = (DualP s t)
>                   BalancedParF (Op c :-> s) ((Ch c :-> t) ': env) = (DualP s t) 
>                   {-| Can be equal if replicated send encoding in each part -}
>                   BalancedParF (c :-> Int :! (s :*! t)) ((c :-> Int :! (s' :*! t')) ': env) 
>                                                                  = (s ~ s', t ~ t')
>                   BalancedParF (c :-> s) ((d :-> t) ': env)       = (BalancedParF (c :-> s) env)