Safe Haskell | Safe |
---|---|

Language | Haskell2010 |

This module provides a collection of types and type families.

Specifically it defines the session type data type, capability data type and type families that compute using session types or capabilities as arguments.

- data ST a
- data Cap a = Cap [ST a] (ST a)
- type family GetST s where ...
- type family GetCtx s where ...
- type family Dual s = r | r -> s where ...
- type family DualST (a :: ST c) = (b :: ST c) | b -> a where ...
- type family MapDual xs = ys | ys -> xs where ...
- type family RemoveSend s where ...
- type family RemoveSendST s where ...
- type family MapRemoveSend ctx where ...
- type family RemoveRecv s where ...
- type family RemoveRecvST s where ...
- type family MapRemoveRecv ctx where ...
- type family HasConstraint (c :: Type -> Constraint) s :: Constraint where ...
- type family HasConstraintST (c :: Type -> Constraint) s :: Constraint where ...
- type family MapHasConstraint (c :: Type -> Constraint) ss :: Constraint where ...
- type family HasConstraints (cs :: [Type -> Constraint]) s :: Constraint where ...
- type family IfThenElse (b :: Bool) (l :: k) (r :: k) :: k where ...
- type family Not b :: Bool where ...
- type family Or b1 b2 :: Bool where ...
- data Prod t = (:*:) (Cap t) (Cap t)
- type family Left p where ...
- type family Right p where ...
- data Nat
- data Ref s xs where
- type family TypeEqList xs s where ...
- type family Append xs ys where ...

# Session Types

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.

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

IxMonad (Cap *) (IxC m) Source # | |

IxApplicative (Cap *) (IxC m) Source # | |

IxFunctor (Cap *) (IxC m) Source # | |

Monad m => IxMonadT (Cap a) (STTerm a) m Source # | |

MonadIO m => IxMonadIO (Cap a) (STTerm a m) Source # | |

Monad m => IxMonad (Cap a) (STTerm a m) Source # | |

Monad m => IxApplicative (Cap a) (STTerm a m) Source # | |

IxFunctor (Cap a) (STTerm a m) Source # | |

# Duality

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

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.

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

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

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

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

# Removing

type family RemoveSend s where ... Source #

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

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

type family RemoveSendST s where ... Source #

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

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 ... Source #

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

MapRemoveSend '[] = '[] | |

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

type family RemoveRecv s where ... Source #

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

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

type family RemoveRecvST s where ... Source #

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

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 ... Source #

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

MapRemoveRecv '[] = '[] | |

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

# Applying Constraints

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

Type family for applying a constraint to types of kind `Type`

in a session type. It may be applied to a capability.

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

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

Type family for applying a constraint to types of kind `Type`

in a list of session types.

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 ... Source #

Type family for applying a constraint to types of kind `Type`

in a session type. It may be applied to a session type.

MapHasConstraint c '[] = () | |

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

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

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.

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 ... Source #

Promoted `ifThenElse`

IfThenElse True l r = l | |

IfThenElse False l r = r |

# Product type

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.

# Other

Data type defining natural numbers

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

type family TypeEqList xs s where ... Source #

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

TypeEqList '[s] s = '[True] | |

TypeEqList '[r] s = '[False] | |

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

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