Safe Haskell	Safe
Language	GHC2021

LambdaUC.Types

Synopsis

module Data.HList
data Void
type Type = TYPE LiftedRep
type Constraint = CONSTRAINT LiftedRep
data (a :: k) :~: (b :: k) where
- Refl :: forall {k} (a :: k). a :~: a
type Continuation x = forall a. (x -> a) -> a
type Not (a :: Type) = a -> Void
data SBool (a :: Bool) where
- STrue :: SBool True
- SFalse :: SBool False
data SIndex (a :: Index) where
- SNextSend :: SIndex NextSend
- SNextRecv :: SIndex NextRecv
type family Or x y where ...
type family BoolNeg x where ...
class Empty x
type family IfThenElse c t f where ...
class KnownBool (b :: Bool) where
- getSBool :: SBool b
lemmaBoolNegInv :: forall b. KnownBool b => BoolNeg (BoolNeg b) :~: b
class KnownIndex (b :: Index) where
- getSIndex :: SIndex b
data KnownLenD :: forall a. [a] -> Type where
- KnownLenZ :: KnownLenD '[]
- KnownLenS :: forall a (x :: a) (l :: [a]). KnownLenD l -> KnownLenD (x : l)
class KnownLen l where
- getKnownLenPrf :: KnownLenD l
data SameLenD :: forall a b. [a] -> [b] -> Type where
- SameLenNil :: SameLenD '[] '[]
- SameLenCons :: SameLenD l l' -> SameLenD (x : l) (x' : l')
class SameLen l l' where
- proveSameLength :: SameLenD l l'
data Index
- = NextSend
- | NextRecv

Documentation

module Data.HList

data Void #

Uninhabited data type

Since: base-4.8.0.0

Instances

Instances details

Semigroup Void	Since: base-4.9.0.0
Instance details Defined in GHC.Base Methods (<>) :: Void -> Void -> Void # sconcat :: NonEmpty Void -> Void # stimes :: Integral b => b -> Void -> Void #
Generic Void
Instance details Defined in GHC.Generics Associated Types type Rep Void :: Type -> Type # Methods from :: Void -> Rep Void x # to :: Rep Void x -> Void #
Read Void	Reading a `Void` value is always a parse error, considering `Void` as a data type with no constructors. Since: base-4.8.0.0
Instance details Defined in GHC.Read Methods readsPrec :: Int -> ReadS Void # readList :: ReadS [Void] # readPrec :: ReadPrec Void # readListPrec :: ReadPrec [Void] #
Show Void	Since: base-4.8.0.0
Instance details Defined in GHC.Show Methods showsPrec :: Int -> Void -> ShowS # show :: Void -> String # showList :: [Void] -> ShowS #
Eq Void	Since: base-4.8.0.0
Instance details Defined in GHC.Base Methods (==) :: Void -> Void -> Bool # (/=) :: Void -> Void -> Bool #
Ord Void	Since: base-4.8.0.0
Instance details Defined in GHC.Base Methods compare :: Void -> Void -> Ordering # (<) :: Void -> Void -> Bool # (<=) :: Void -> Void -> Bool # (>) :: Void -> Void -> Bool # (>=) :: Void -> Void -> Bool # max :: Void -> Void -> Void # min :: Void -> Void -> Void #
Hashable Void
Instance details Defined in Data.Hashable.Class Methods hashWithSalt :: Int -> Void -> Int # hash :: Void -> Int #
MayOnlyReturnAfterRecv 'NextRecv Void #
Instance details Defined in LambdaUC.Syntax.Async.Eval.Internal Methods getMayOnlyReturnAfterRecvPrf :: MayOnlyReturnAfterRecvD 'NextRecv Void #
type Rep Void	Since: base-4.8.0.0
Instance details Defined in GHC.Generics type Rep Void = D1 ('MetaData "Void" "GHC.Base" "base" 'False) (V1 :: Type -> Type)

type Type = TYPE LiftedRep #

The kind of types with lifted values. For example Int :: Type.

type Constraint = CONSTRAINT LiftedRep #

The kind of lifted constraints

data (a :: k) :~: (b :: k) where infix 4 #

Propositional equality. If a :~: b is inhabited by some terminating value, then the type a is the same as the type b. To use this equality in practice, pattern-match on the a :~: b to get out the Refl constructor; in the body of the pattern-match, the compiler knows that a ~ b.

Since: base-4.7.0.0

Constructors

Refl :: forall {k} (a :: k). a :~: a

Instances

Instances details

Category ((:~:) :: k -> k -> Type)	Since: base-4.7.0.0
Instance details Defined in Control.Category Methods id :: forall (a :: k0). a :~: a # (.) :: forall (b :: k0) (c :: k0) (a :: k0). (b :~: c) -> (a :~: b) -> a :~: c #
TestEquality ((:~:) a :: k -> Type)	Since: base-4.7.0.0
Instance details Defined in Data.Type.Equality Methods testEquality :: forall (a0 :: k0) (b :: k0). (a :~: a0) -> (a :~: b) -> Maybe (a0 :~: b) #
a ~ b => Bounded (a :~: b)	Since: base-4.7.0.0
Instance details Defined in Data.Type.Equality Methods minBound :: a :~: b # maxBound :: a :~: b #
a ~ b => Enum (a :~: b)	Since: base-4.7.0.0
Instance details Defined in Data.Type.Equality Methods succ :: (a :~: b) -> a :~: b # pred :: (a :~: b) -> a :~: b # toEnum :: Int -> a :~: b # fromEnum :: (a :~: b) -> Int # enumFrom :: (a :~: b) -> [a :~: b] # enumFromThen :: (a :~: b) -> (a :~: b) -> [a :~: b] # enumFromTo :: (a :~: b) -> (a :~: b) -> [a :~: b] # enumFromThenTo :: (a :~: b) -> (a :~: b) -> (a :~: b) -> [a :~: b] #
a ~ b => Read (a :~: b)	Since: base-4.7.0.0
Instance details Defined in Data.Type.Equality Methods readsPrec :: Int -> ReadS (a :~: b) # readList :: ReadS [a :~: b] # readPrec :: ReadPrec (a :~: b) # readListPrec :: ReadPrec [a :~: b] #
Show (a :~: b)	Since: base-4.7.0.0
Instance details Defined in Data.Type.Equality Methods showsPrec :: Int -> (a :~: b) -> ShowS # show :: (a :~: b) -> String # showList :: [a :~: b] -> ShowS #
Eq (a :~: b)	Since: base-4.7.0.0
Instance details Defined in Data.Type.Equality Methods (==) :: (a :~: b) -> (a :~: b) -> Bool # (/=) :: (a :~: b) -> (a :~: b) -> Bool #
Ord (a :~: b)	Since: base-4.7.0.0
Instance details Defined in Data.Type.Equality Methods compare :: (a :~: b) -> (a :~: b) -> Ordering # (<) :: (a :~: b) -> (a :~: b) -> Bool # (<=) :: (a :~: b) -> (a :~: b) -> Bool # (>) :: (a :~: b) -> (a :~: b) -> Bool # (>=) :: (a :~: b) -> (a :~: b) -> Bool # max :: (a :~: b) -> (a :~: b) -> a :~: b # min :: (a :~: b) -> (a :~: b) -> a :~: b #

type Continuation x = forall a. (x -> a) -> a #

type Not (a :: Type) = a -> Void #

data SBool (a :: Bool) where #

Constructors

STrue :: SBool True
SFalse :: SBool False

data SIndex (a :: Index) where #

Singleton Bool used to store the dependent value of Write Token

Constructors

SNextSend :: SIndex NextSend
SNextRecv :: SIndex NextRecv

type family Or x y where ... #

Equations

Or True _ = True
Or _ True = True
Or _ _ = False

type family BoolNeg x where ... #

Equations

BoolNeg True = False
BoolNeg False = True

class Empty x #

Empty constraint

Instances

Instances details

Empty (x :: k) #
Instance details Defined in LambdaUC.Types

type family IfThenElse c t f where ... #

Type-level if-then-else, we use it to choose constraints conditionally

Equations

IfThenElse True t _ = t
IfThenElse False _ f = f

class KnownBool (b :: Bool) where #

Known boolean value. Implemented by constants, but not by `forall (b :: Bool). b`. Adding this to the context of a function polymorphic over b is the same as adding an explicit parameter `SBool b` to it. I.e. `SBool b ->` is the same as `KnownBool b =>`.

Methods

getSBool :: SBool b #

Instances

Instances details

KnownBool 'False #
Instance details Defined in LambdaUC.Types Methods getSBool :: SBool 'False #
KnownBool 'True #
Instance details Defined in LambdaUC.Types Methods getSBool :: SBool 'True #

lemmaBoolNegInv :: forall b. KnownBool b => BoolNeg (BoolNeg b) :~: b #

¬¬x = x

class KnownIndex (b :: Index) where #

Methods

getSIndex :: SIndex b #

Instances

Instances details

KnownIndex 'NextRecv #
Instance details Defined in LambdaUC.Types Methods getSIndex :: SIndex 'NextRecv #
KnownIndex 'NextSend #
Instance details Defined in LambdaUC.Types Methods getSIndex :: SIndex 'NextSend #

data KnownLenD :: forall a. [a] -> Type where #

Signleton type to express the list structure (length) but not the contents.

Constructors

KnownLenZ :: KnownLenD '[]
KnownLenS :: forall a (x :: a) (l :: [a]). KnownLenD l -> KnownLenD (x : l)

class KnownLen l where #

Class of list values for which their length is known at compile time.

Methods

getKnownLenPrf :: KnownLenD l #

Instances

Instances details

KnownLen ('[] :: [a]) #
Instance details Defined in Data.HList Methods getKnownLenPrf :: KnownLenD '[] #
KnownLen xs => KnownLen (x ': xs :: [a]) #
Instance details Defined in Data.HList Methods getKnownLenPrf :: KnownLenD (x ': xs) #

data SameLenD :: forall a b. [a] -> [b] -> Type where #

Constructors

SameLenNil :: SameLenD '[] '[]
SameLenCons :: SameLenD l l' -> SameLenD (x : l) (x' : l')

class SameLen l l' where #

Methods

proveSameLength :: SameLenD l l' #

Instances

Instances details

SameLen ('[] :: [a]) ('[] :: [b]) #
Instance details Defined in Data.HList Methods proveSameLength :: SameLenD '[] '[] #
SameLen l l' => SameLen (x ': l :: [a]) (x' ': l' :: [b]) #
Instance details Defined in Data.HList Methods proveSameLength :: SameLenD (x ': l) (x' ': l') #

data Index #

Next operation of the asyncronous algorithm

Constructors

NextSend	Our turn to `send`
NextRecv	Our turn to `recvAny`

Instances

Instances details

XApplicative (AsyncExT ex ports :: Index -> Index -> Type -> Type) #
Instance details Defined in LambdaUC.Syntax.Async Methods xpure :: forall a (p :: k). a -> AsyncExT ex ports p p a # (<>:) :: forall (p :: k) (q :: k) a b (r :: k). AsyncExT ex ports p q (a -> b) -> AsyncExT ex ports q r a -> AsyncExT ex ports p r b # xliftA2 :: forall a b c (p :: k) (q :: k) (r :: k). (a -> b -> c) -> AsyncExT ex ports p q a -> AsyncExT ex ports q r b -> AsyncExT ex ports p r c # (>:) :: forall (p :: k) (q :: k) a (r :: k) b. AsyncExT ex ports p q a -> AsyncExT ex ports q r b -> AsyncExT ex ports p r b # (<*:) :: forall (p :: k) (q :: k) a (r :: k) b. AsyncExT ex ports p q a -> AsyncExT ex ports q r b -> AsyncExT ex ports p r a #
XMonad (AsyncExT ex ports :: Index -> Index -> Type -> Type) #
Instance details Defined in LambdaUC.Syntax.Async Methods (>>=:) :: forall a b (p :: k) (q :: k) (r :: k). AsyncExT ex ports p q a -> (a -> AsyncExT ex ports q r b) -> AsyncExT ex ports p r b # (>>:) :: forall a b (p :: k) (q :: k) (r :: k). AsyncExT ex ports p q a -> AsyncExT ex ports q r b -> AsyncExT ex ports p r b # xreturn :: forall a (p :: k). a -> AsyncExT ex ports p p a #