Control.SessionTypes

This packages provides a deep embedded domain-specific language for writing session typed program.

A session typed program is a program annotated with session types. A session type describes a communication protocol at the type-level.

The motivation for doing so is that it gives you a static guarantee that a program correctly implements a protocol. It may even guarantee that no deadlocking can occur.

The following constitutes the most important parts of this library for writing session typed programs.

• STTerm: A GADT representing the terms of the DSL. The constructors represent the different session types and are annotated with session types.
• ST: A protomoted data type describing the different session types.
• MonadSession: A type class exposing the interface of the DSL.
• Control.SessionTypes.Indexed: A custom prelude module replacing common type classes with indexed type classes

This package also implements a couple interpreters that evaluate an abstract-syntax tree consisting of STTerm constructors:

• Control.SessionTypes.Debug: Purely evaluation
• Control.SessionTypes.Interactive: Interactive evaluation
• Control.SessionTypes.Normalize: Rewrites STTerm programs to a normal form
• Control.SessionTypes.Visualize: Visualizes a session type

STTerm

data STTerm :: (Type -> Type) -> Cap a -> Cap a -> Type -> Type where

The STTerm GADT

Although we say that a STTerm is annotated with a session type, it is actually annotated with a capability (Cap).

The capability contains a context that is necessary for recursion and the session type.

The constructors can be split in four different categories:

• Communication: Send and Recv for basic communication
• Branching: Sel1, Sel2, OffZ and OffS
• Recursion: Rec, Weaken and Var
• Unsession typed: Ret and Lift

Constructors

Send :: a -> STTerm m (Cap ctx r) r' b -> STTerm m (Cap ctx (a :!> r)) r' b

The constructor for sending messages. It is annotated with the send session type (:!>).

It takes as an argument, the message to send, of type equal to the first argument of :!> and the continuing STTerm that is session typed with the second argument of :!>.

Recv :: (a -> STTerm m (Cap ctx r) r' b) -> STTerm m (Cap ctx (a :?> r)) r' b

The constructor for receiving messages. It is annotated with the receive session type (:?>)

It takes a continuation that promises to deliver a value that may be used in the rest of the program.

Sel1 :: STTerm m (Cap ctx s) r a -> STTerm m (Cap ctx (Sel (s ': xs))) r a

Selects the first branch in a selection session type.

By selecting a branch, that selected session type must then be implemented.

Sel2 :: STTerm m (Cap ctx (Sel (t ': xs))) r a -> STTerm m (Cap ctx (Sel (s ': (t ': xs)))) r a

Skips a branch in a selection session type.

If the first branch in the selection session type is not the one we want to implement then we may use Sel2 to skip this.

OffZ :: STTerm m (Cap ctx s) r a -> STTerm m (Cap ctx (Off '[s])) r a

Dually to selection there is also offering branches.

Unlike selection, where we may only implement one branch, an offering asks you to implement all branches. Which is chosen depends on how an interpreter synchronizes selection with offering.

This constructor denotes the very last branch that may be offered.

OffS :: STTerm m (Cap ctx s) r a -> STTerm m (Cap ctx (Off (t ': xs))) r a -> STTerm m (Cap ctx (Off (s ': (t ': xs)))) r a

offers a branch and promises at least one more branch to be offered.

Rec :: STTerm m (Cap (s ': ctx) s) r a -> STTerm m (Cap ctx (R s)) r a

Constructor for delimiting the scope of recursion

The recursion constructors also modify or at least make use of the context in the capability.

The Rec constructor inserts the session type argument to R into the context of the capability of its STTerm argument.

This is necessary such that we remember the session type of the body of code that we may want to recurse over and thus avoiding infinite type occurrence errors.

Weaken :: STTerm m (Cap ctx t) r a -> STTerm m (Cap (s ': ctx) (Wk t)) r a

Constructor for weakening (expanding) the scope of recusion

This constructor does the opposite of R by popping a session type from the context.

Use this constructor to essentially exit a recursion

Var :: STTerm m (Cap (s ': ctx) s) t a -> STTerm m (Cap (s ': ctx) V) t a

Constructor that denotes the recursion variable

It assumes the context to be non-empty and uses the session type at the top of the context to determine what should be implemented after Var.

Ret :: (a :: Type) -> STTerm m s s a

Constructor that makes STTerm a (indexed) monad

Lift :: m (STTerm m s r a) -> STTerm m s r a

Constructor that makes STTerm a (indexed) monad transformer

Instances

Monad m => IxMonadT (Cap a) (STTerm a) m

Methods

lift :: m a -> m m s s a

MonadIO m => IxMonadIO (Cap a) (STTerm a m)

Methods

liftIO :: IO a -> m s s a

Monad m => IxMonad (Cap a) (STTerm a m)

Methods

(>>=) :: m s t a -> (a -> m t k b) -> m s k b

(>>) :: m s t a -> m t k b -> m s k b

return :: a -> m i i a

fail :: String -> m i i a

Monad m => IxApplicative (Cap a) (STTerm a m)

Methods

pure :: a -> f i i a

(<*>) :: f s r (a -> b) -> f r k a -> f s k b

IxFunctor (Cap a) (STTerm a m)

Methods

fmap :: (a -> b) -> f j k a -> f j k b

Monad m => MonadSession (STTerm * m)

Methods

send :: a -> STTerm * m (Cap * ctx ((* :!> a) r)) (Cap * ctx r) ()

recv :: STTerm * m (Cap * ctx ((* :?> a) r)) (Cap * ctx r) a

sel1 :: STTerm * m (Cap * ctx (Sel * ((ST * ': s) xs))) (Cap * ctx s) ()

sel2 :: STTerm * m (Cap * ctx (Sel * ((ST * ': s) ((ST * ': t) xs)))) (Cap * ctx (Sel * ((ST * ': t) xs))) ()

offZ :: STTerm * m (Cap * ctx s) r a -> STTerm * m (Cap * ctx (Off * ((ST * ': s) [ST *]))) r a

offS :: STTerm * m (Cap * ctx s) r a -> STTerm * m (Cap * ctx (Off * ((ST * ': t) xs))) r a -> STTerm * m (Cap * ctx (Off * ((ST * ': s) ((ST * ': t) xs)))) r a

recurse :: STTerm * m (Cap * ((ST * ': s) ctx) s) r a -> STTerm * m (Cap * ctx (R * s)) r a

weaken :: STTerm * m (Cap * ctx s) r a -> STTerm * m (Cap * ((ST * ': t) ctx) (Wk * s)) r a

var :: STTerm * m (Cap * ((ST * ': s) ctx) s) r a -> STTerm * m (Cap * ((ST * ': s) ctx) (V *)) r a

eps :: a -> STTerm * m (Cap * ctx (Eps *)) (Cap * ctx (Eps *)) a

Monad (STTerm a m s s)

Methods

(>>=) :: STTerm a m s s a -> (a -> STTerm a m s s b) -> STTerm a m s s b

(>>) :: STTerm a m s s a -> STTerm a m s s b -> STTerm a m s s b

return :: a -> STTerm a m s s a

fail :: String -> STTerm a m s s a

Functor (STTerm a m s s)

Methods

fmap :: (a -> b) -> STTerm a m s s a -> STTerm a m s s b

(<$) :: a -> STTerm a m s s b -> STTerm a m s s a

Applicative (STTerm a m s s)

Methods

pure :: a -> STTerm a m s s a

(<*>) :: STTerm a m s s (a -> b) -> STTerm a m s s a -> STTerm a m s s b

(*>) :: STTerm a m s s a -> STTerm a m s s b -> STTerm a m s s b

(<*) :: STTerm a m s s a -> STTerm a m s s b -> STTerm a m s s a

inferIdentity :: STTerm Identity s r a -> STTerm Identity s r a

This function can be used if we do not use lift in a program but we must still disambiguate m.

MonadSession

Primitives

class IxMonad m => MonadSession m where

The MonadSession type class exposes a set of functions that composed together form a session typed program

A type that is an instance of MonadSession must therefore also be an instance of IxMonad.

The functions themselves are generally defined as wrappers over corresponding STTerm constructors.

Minimal complete definition

send, recv, sel1, sel2, offZ, offS, recurse, weaken, var, eps

Methods

send :: a -> m (Cap ctx (a :!> r)) (Cap ctx r) ()

recv :: m (Cap ctx (a :?> r)) (Cap ctx r) a

sel1 :: m (Cap ctx (Sel (s ': xs))) (Cap ctx s) ()

sel2 :: m (Cap ctx (Sel (s ': (t ': xs)))) (Cap ctx (Sel (t ': xs))) ()

offZ :: m (Cap ctx s) r a -> m (Cap ctx (Off '[s])) r a

offS :: m (Cap ctx s) r a -> m (Cap ctx (Off (t ': xs))) r a -> m (Cap ctx (Off (s ': (t ': xs)))) r a

recurse :: m (Cap (s ': ctx) s) r a -> m (Cap ctx (R s)) r a

weaken :: m (Cap ctx s) r a -> m (Cap (t ': ctx) (Wk s)) r a

var :: m (Cap (s ': ctx) s) r a -> m (Cap (s ': ctx) V) r a

eps :: a -> m (Cap ctx Eps) (Cap ctx Eps) a

Instances

Monad m => MonadSession (IxC m)

Methods

send :: a -> IxC m (Cap * ctx ((* :!> a) r)) (Cap * ctx r) ()

recv :: IxC m (Cap * ctx ((* :?> a) r)) (Cap * ctx r) a

sel1 :: IxC m (Cap * ctx (Sel * ((ST * ': s) xs))) (Cap * ctx s) ()

sel2 :: IxC m (Cap * ctx (Sel * ((ST * ': s) ((ST * ': t) xs)))) (Cap * ctx (Sel * ((ST * ': t) xs))) ()

offZ :: IxC m (Cap * ctx s) r a -> IxC m (Cap * ctx (Off * ((ST * ': s) [ST *]))) r a

offS :: IxC m (Cap * ctx s) r a -> IxC m (Cap * ctx (Off * ((ST * ': t) xs))) r a -> IxC m (Cap * ctx (Off * ((ST * ': s) ((ST * ': t) xs)))) r a

recurse :: IxC m (Cap * ((ST * ': s) ctx) s) r a -> IxC m (Cap * ctx (R * s)) r a

weaken :: IxC m (Cap * ctx s) r a -> IxC m (Cap * ((ST * ': t) ctx) (Wk * s)) r a

var :: IxC m (Cap * ((ST * ': s) ctx) s) r a -> IxC m (Cap * ((ST * ': s) ctx) (V *)) r a

eps :: a -> IxC m (Cap * ctx (Eps *)) (Cap * ctx (Eps *)) a

Monad m => MonadSession (STTerm * m)

Methods

send :: a -> STTerm * m (Cap * ctx ((* :!> a) r)) (Cap * ctx r) ()

recv :: STTerm * m (Cap * ctx ((* :?> a) r)) (Cap * ctx r) a

sel1 :: STTerm * m (Cap * ctx (Sel * ((ST * ': s) xs))) (Cap * ctx s) ()

sel2 :: STTerm * m (Cap * ctx (Sel * ((ST * ': s) ((ST * ': t) xs)))) (Cap * ctx (Sel * ((ST * ': t) xs))) ()

offZ :: STTerm * m (Cap * ctx s) r a -> STTerm * m (Cap * ctx (Off * ((ST * ': s) [ST *]))) r a

offS :: STTerm * m (Cap * ctx s) r a -> STTerm * m (Cap * ctx (Off * ((ST * ': t) xs))) r a -> STTerm * m (Cap * ctx (Off * ((ST * ': s) ((ST * ': t) xs)))) r a

recurse :: STTerm * m (Cap * ((ST * ': s) ctx) s) r a -> STTerm * m (Cap * ctx (R * s)) r a

weaken :: STTerm * m (Cap * ctx s) r a -> STTerm * m (Cap * ((ST * ': t) ctx) (Wk * s)) r a

var :: STTerm * m (Cap * ((ST * ': s) ctx) s) r a -> STTerm * m (Cap * ((ST * ': s) ctx) (V *)) r a

eps :: a -> STTerm * m (Cap * ctx (Eps *)) (Cap * ctx (Eps *)) a

Combinators

empty :: MonadSession m => m (Cap '[] s) r a -> m (Cap '[] s) r a

A session typed program that is polymorphic in its context can often not be used by interpreters.

We can apply empty to the session typed program before passing it to an interpreter to instantiate that the context is empty.

empty0 :: MonadSession m => m (Cap '[] r) (Cap '[] r) ()

Monadic composable definition of empty

Prefix a session typed program with (empty >>) to instantiate the context to be empty.

selN :: MonadSession m => Ref s xs -> m (Cap ctx (Sel xs)) (Cap ctx s) ()

Allows indexing of selections.

The given Ref type can be used as an indexed to select a branch. This circumvents the need to sequence a bunch of sel1 and sel2 to select a branch.

prog :: MonadSession m => m ('Cap ctx (Sel '[a,b,c,d])) ('Cap ctx Eps) ()

MonadSession m => m ('Cap ctx b) ('Cap ctx Eps) ()
prog2 = prog >> selN (RefS RefZ)

selN1 :: MonadSession m => m (Cap ctx (Sel (s ': xs))) (Cap ctx s) ()

Select the first branch of a selection.

selN2 :: MonadSession m => m (Cap ctx (Sel (s ': (t ': xs)))) (Cap ctx t) ()

Select the second branch of a selection.

selN3 :: MonadSession m => m (Cap ctx (Sel (s ': (t ': (k ': xs))))) (Cap ctx k) ()

Select the third branch of a selection.

selN4 :: MonadSession m => m (Cap ctx (Sel (s ': (t ': (k ': (r ': xs)))))) (Cap ctx r) ()

Select the fourth branch of a selection.

class Select xs s where

Type class for selecting a branch through injection.

Selects the first branch that matches the given session type.

prog :: MonadSession m => m ('Cap ctx (Sel '[Eps, String :!> Eps, Int :!> Eps])) ('Cap ctx Eps) ()
prog = sel >> send "c" >>= eps

It should be obvious that you cannot select a branch using sel if that branch has the same session type as a previous branch.

Minimal complete definition

sel

Methods

sel :: MonadSession m => m (Cap ctx (Sel xs)) (Cap ctx s) ()

Instances

((~) [Bool] tl (TypeEqList (ST *) xs s), Select' [Bool] xs s tl) => Select xs s

Methods

sel :: MonadSession m => m (Cap * ctx (Sel * xs)) (Cap * ctx s) ()

(<&) :: MonadSession m => m (Cap ctx s) r a -> m (Cap ctx (Off (t ': xs))) r a -> m (Cap ctx (Off (s ': (t ': xs)))) r a infixr 1

Infix synonym for offS

(<&>) :: MonadSession m => m (Cap ctx s) r a -> m (Cap ctx t) r a -> m (Cap ctx (Off '[s, t])) r a infix 2

Infix synonym for offer

Using both <& and <&> we can now construct an offering as follows:

 branch1 
 <& branch2
 <& branch3
 <&> branch4

This will be parsed as

(branch1
 <& (branch2
 <& (branch3
 <&> branch4)))

offer :: MonadSession m => m (Cap ctx s) r a -> m (Cap ctx t) r a -> m (Cap ctx (Off '[s, t])) r a

Takes two session typed programs and constructs an offering consisting of two branches

recurseFix :: MonadSession m => (m (Cap (s ': ctx) V) r a -> m (Cap (s ': ctx) s) r a) -> m (Cap ctx (R s)) r a

A fixpoint combinator for recursion

The argument function must take a recursion variable as an argument that can be used to denote the point of recursion.

For example:

prog = recurseFix \f -> do
 send 5
 f

This program will send the number 5 an infinite amount of times.

recurse0 :: MonadSession m => m (Cap ctx (R s)) (Cap (s ': ctx) s) ()

Monadic composable definition of recurse

weaken0 :: MonadSession m => m (Cap (t ': ctx) (Wk s)) (Cap ctx s) ()

Monadic composable definition of weaken

var0 :: MonadSession m => m (Cap (s ': ctx) V) (Cap (s ': ctx) s) ()

Monadic composable definition of var

eps0 :: MonadSession m => m (Cap ctx Eps) (Cap ctx Eps) ()

Monadic composable definition of eps

Types

Session Types

data ST a

The session type data type

Each constructor denotes a specific session type. Using the DataKinds pragma the constructors are promoted to types and ST is promoted to a kind.

Constructors

(:?>) a (ST a) infixr 6

Send a value

(:!>) a (ST a) infixr 6

Recv a value

Sel [ST a]

Selection of branches

Off [ST a]

Offering of branches

R (ST a)

Delimit the scope of recursion

Wk (ST a)

Weaken the scope of recursion

V

Recursion variable

Eps

End of the session

data Cap a

A capability that stores a context/scope that is a list of session types and a session type

Constructors

Cap [ST a] (ST a)

Instances

IxMonad (Cap *) (IxC m)

Methods

(>>=) :: m s t a -> (a -> m t k b) -> m s k b

(>>) :: m s t a -> m t k b -> m s k b

return :: a -> m i i a

fail :: String -> m i i a

IxApplicative (Cap *) (IxC m)

Methods

pure :: a -> f i i a

(<*>) :: f s r (a -> b) -> f r k a -> f s k b

IxFunctor (Cap *) (IxC m)

Methods

fmap :: (a -> b) -> f j k a -> f j k b

Monad m => IxMonadT (Cap a) (STTerm a) m

Methods

lift :: m a -> m m s s a

MonadIO m => IxMonadIO (Cap a) (STTerm a m)

Methods

liftIO :: IO a -> m s s a

Monad m => IxMonad (Cap a) (STTerm a m)

Methods

(>>=) :: m s t a -> (a -> m t k b) -> m s k b

(>>) :: m s t a -> m t k b -> m s k b

return :: a -> m i i a

fail :: String -> m i i a

Monad m => IxApplicative (Cap a) (STTerm a m)

Methods

pure :: a -> f i i a

(<*>) :: f s r (a -> b) -> f r k a -> f s k b

IxFunctor (Cap a) (STTerm a m)

Methods

fmap :: (a -> b) -> f j k a -> f j k b

type family GetST s where ...

Retrieves the session type from the capability

Equations

GetST (Cap ctx s) = s

type family GetCtx s where ...

Retrieves the context from the capability

Equations

GetCtx (Cap ctx s) = ctx

Duality

type family Dual s = r | r -> s where ...

Type family for calculating the dual of a session type. It may be applied to a capability.

We made Dual injective to support calculating the dual of a selection that contains an ambiguous branch. Of course that does require that the dual of that ambiguous branch must be known.

Equations

Dual (Cap ctx s) = Cap (MapDual ctx) (DualST s)

type family DualST (a :: ST c) = (b :: ST c) | b -> a where ...

Type family for calculating the dual of a session type. It may be applied to the actual session type.

Equations

DualST (s :!> r) = s :?> DualST r

DualST (s :?> r) = s :!> DualST r

DualST (Sel xs) = Off (MapDual xs)

DualST (Off xs) = Sel (MapDual xs)

DualST (R s) = R (DualST s)

DualST (Wk s) = Wk (DualST s)

DualST V = V

DualST Eps = Eps

type family MapDual xs = ys | ys -> xs where ...

Type family for calculating the dual of a list of session types.

Equations

MapDual '[] = '[]

MapDual (s ': xs) = DualST s ': MapDual xs

Removing

type family RemoveSend s where ...

Type family for removing the send session type from the given session type. It may be applied to a capability.

Equations

RemoveSend (Cap ctx s) = Cap (MapRemoveSend ctx) (RemoveSendST s)

type family RemoveSendST s where ...

Type family for removing the send session type from the given session type. It may be applied to a session type.

Equations

RemoveSendST (a :!> r) = RemoveSendST r

RemoveSendST (a :?> r) = a :?> RemoveSendST r

RemoveSendST (Sel xs) = Sel (MapRemoveSend xs)

RemoveSendST (Off xs) = Off (MapRemoveSend xs)

RemoveSendST (R s) = R (RemoveSendST s)

RemoveSendST (Wk s) = Wk (RemoveSendST s)

RemoveSendST s = s

type family MapRemoveSend ctx where ...

Type family for removing the send session type from a list of session types.

Equations

MapRemoveSend '[] = '[]

MapRemoveSend (s ': ctx) = RemoveSendST s ': MapRemoveSend ctx

type family RemoveRecv s where ...

Type family for removing the receive session type from the given session type. It may be applied to a capability.

Equations

RemoveRecv (Cap ctx s) = Cap (MapRemoveRecv ctx) (RemoveRecvST s)

type family RemoveRecvST s where ...

Type family for removing the receive session type from a list of session types.

Equations

RemoveRecvST (a :!> r) = a :!> RemoveRecvST r

RemoveRecvST (a :?> r) = RemoveRecvST r

RemoveRecvST (Sel xs) = Sel (MapRemoveRecv xs)

RemoveRecvST (Off xs) = Off (MapRemoveRecv xs)

RemoveRecvST (R s) = R (RemoveRecvST s)

RemoveRecvST (Wk s) = Wk (RemoveRecvST s)

RemoveRecvST s = s

type family MapRemoveRecv ctx where ...

Type family for removing the receive session type from the given session type. It may be applied to a session type.

Equations

MapRemoveRecv '[] = '[]

MapRemoveRecv (s ': ctx) = RemoveRecvST s ': MapRemoveRecv ctx

Applying Constraints

type family HasConstraint (c :: Type -> Constraint) s :: Constraint where ...

Type family for applying a constraint to types of kind Type in a session type. It may be applied to a capability.

Equations

HasConstraint c (Cap ctx s) = (HasConstraintST c s, MapHasConstraint c ctx)

type family HasConstraintST (c :: Type -> Constraint) s :: Constraint where ...

Type family for applying a constraint to types of kind Type in a list of session types.

Equations

HasConstraintST c (a :!> r) = (c a, HasConstraintST c r)

HasConstraintST c (a :?> r) = (c a, HasConstraintST c r)

HasConstraintST c (Sel '[]) = ()

HasConstraintST c (Sel (s ': xs)) = (HasConstraintST c s, HasConstraintST c (Sel xs))

HasConstraintST c (Off '[]) = ()

HasConstraintST c (Off (s ': xs)) = (HasConstraintST c s, HasConstraintST c (Off xs))

HasConstraintST c (R s) = HasConstraintST c s

HasConstraintST c (Wk s) = HasConstraintST c s

HasConstraintST c V = ()

HasConstraintST c s = ()

type family MapHasConstraint (c :: Type -> Constraint) ss :: Constraint where ...

Type family for applying a constraint to types of kind Type in a session type. It may be applied to a session type.

Equations

MapHasConstraint c '[] = ()

MapHasConstraint c (s ': ss) = (HasConstraintST c s, MapHasConstraint c ss)

type family HasConstraints (cs :: [Type -> Constraint]) s :: Constraint where ...

Type family for applying zero or more constraints to types of kind Type in a list of session types. It may be applied to a capability.

Equations

HasConstraints '[] s = ()

HasConstraints (c ': cs) s = (HasConstraint c s, HasConstraints cs s)

Boolean functions

type family IfThenElse (b :: Bool) (l :: k) (r :: k) :: k where ...

Promoted ifThenElse

Equations

IfThenElse True l r = l

IfThenElse False l r = r

type family Not b :: Bool where ...

Promoted not

Equations

Not True = False

Not False = True

type family Or b1 b2 :: Bool where ...

Promoted ||

Equations

Or True b = True

Or b True = True

Or b1 b2 = False

Product type

data Prod t

Data type that takes a kind as an argument. Its sole constructor takes two capabilities parameterized by the kind argument.

This data type is useful if it is necessary for an indexed monad to be indexed by four parameters.

Constructors

(:*:) (Cap t) (Cap t)

type family Left p where ...

Type family for returning the first argument of a product.

Equations

Left (l :*: r) = l

type family Right p where ...

Type family for returning the second argument of a product.

Equations

Right (l :*: r) = r

Other

data Nat

Data type defining natural numbers

Constructors

Z

S Nat

Instances

Eq Nat

Methods

(==) :: Nat -> Nat -> Bool

(/=) :: Nat -> Nat -> Bool

Ord Nat

Methods

compare :: Nat -> Nat -> Ordering

(<) :: Nat -> Nat -> Bool

(<=) :: Nat -> Nat -> Bool

(>) :: Nat -> Nat -> Bool

(>=) :: Nat -> Nat -> Bool

max :: Nat -> Nat -> Nat

min :: Nat -> Nat -> Nat

Show Nat

Methods

showsPrec :: Int -> Nat -> ShowS

show :: Nat -> String

showList :: [Nat] -> ShowS

data Ref s xs where

Data type that can give us proof of membership of an element in a list of elements.

Constructors

RefZ :: Ref s (s ': xs)

RefS :: Ref s (k ': xs) -> Ref s (t ': (k ': xs))

type family TypeEqList xs s where ...

Type family for computing which types in a list of types are equal to a given type.

Equations

TypeEqList '[s] s = '[True]

TypeEqList '[r] s = '[False]

TypeEqList (s ': xs) s = True ': TypeEqList xs s

TypeEqList (r ': xs) s = False ': TypeEqList xs s

type family Append xs ys where ...

Promoted ++

Equations

Append '[] ys = ys

Append (x ': xs) ys = x ': (xs `Append` ys)