Safe Haskell	Safe
Language	GHC2021

Data.HList

Contents

Dependent pointer into a list
Port Lists
Heterogenous Lists

Synopsis

data InList xs x where
- Here :: InList (x : xs) x
- There :: InList xs x -> InList (y : xs) x
pattern There2 :: InList xs x -> InList (y0 : (y1 : xs)) x
pattern There3 :: InList xs x -> InList (y0 : (y1 : (y2 : xs))) x
pattern There4 :: InList xs x -> InList (y0 : (y1 : (y2 : (y3 : xs)))) x
pattern There5 :: InList xs x -> InList (y0 : (y1 : (y2 : (y3 : (y4 : xs))))) x
pattern There6 :: InList xs x -> InList (y0 : (y1 : (y2 : (y3 : (y4 : (y5 : xs)))))) x
pattern InList0 :: InList (x : xs) x
pattern InList1 :: InList (y0 : (x : xs)) x
pattern InList2 :: InList (y0 : (y1 : (x : xs))) x
pattern InList3 :: InList (y0 : (y1 : (y2 : (x : xs)))) x
pattern InList4 :: InList (y0 : (y1 : (y2 : (y3 : (x : xs))))) x
pattern InList5 :: InList (y0 : (y1 : (y2 : (y3 : (y4 : (x : xs)))))) x
pattern InList6 :: InList (y0 : (y1 : (y2 : (y3 : (y4 : (y5 : (x : xs))))))) x
data SomeIndex xs where
- SomeIndex :: InList xs x -> SomeIndex xs
data SomeValue xs where
- SomeValue :: InList xs x -> x -> SomeValue xs
padMessageIndex :: SomeValue ts -> SomeValue (t : ts)
data Port = Type :> Type
type family PortTxType p where ...
type family PortRxType p where ...
type family PortDual p where ...
type PortInList x y xs = InList xs (x :> y)
type family Fst p where ...
type family MapFst l where ...
type family Snd p where ...
type family Zip l l' where ...
data SomeRxMess xs where
- SomeRxMess :: InList xs p -> PortRxType p -> SomeRxMess xs
data SomeTxMess xs where
- SomeTxMess :: InList xs p -> PortTxType p -> SomeTxMess xs
data HList f (types :: [a]) where
- HNil :: HList f '[]
- HCons :: f t -> HList f ts -> HList f (t : ts)
data KnownHPPortsD ports where
- KnownHPPortsZ :: KnownHPPortsD '[]
- KnownHPPortsS :: KnownHPPortsD ports -> KnownHPPortsD ((HListPair xl xr :> HListPair yl yr) : ports)
type HListPair l r = (HList Identity l, HList Identity r)
type family Concat2 l r p where ...
type family MapConcat2 l r ports where ...
(++) :: HList f l -> HList f r -> HList f (Concat l r)
(+++) :: HListPair l r -> HListPair l' r' -> HListPair (Concat l l') (Concat r r')
class KnownHPPorts ports where
- getKnownHPPorts :: KnownHPPortsD ports
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'
type family Concat xs ys where ...
concatAssocPrf :: forall p p' s' l s. ListSplitD l p s -> Concat p (Concat p' s') :~: Concat (Concat p p') s'
concatInjPrf :: forall xs ys ys'. (Concat xs ys :~: Concat xs ys') -> KnownLenD xs -> ys :~: ys'
data ListSplitD :: forall a. [a] -> [a] -> [a] -> Type where
- SplitHere :: ListSplitD l '[] l
- SplitThere :: ListSplitD l p s -> ListSplitD (x : l) (x : p) s
type ListSplitConcat p s = ListSplitD (Concat p s) p s
class ListSplit l p s where
- getListSplit :: ListSplitD l p s
getListSplit' :: KnownLenD p -> ListSplitD (Concat p s) p s
listSplitConcat :: ListSplitD l p s -> Concat p s :~: l
listSplitAdd :: ListSplitD l p s -> ListSplitD s p' s' -> ListSplitD l (Concat p p') s'
listConcatSplit :: ListSplitD l p s -> ListSplitD (Concat p s') p s'
listSplitPopSuffix :: ListSplitD (Concat p (x : s)) p (x : s) -> ListSplitD (Concat p s) p s
listSplitSubst :: ListSplitD l' p' (s : rest) -> ListSplitConcat p' (f : rest)
listSplitSwap :: ListSplitD l p (f : l') -> ListSplitD l' p' (s : rest) -> (ListSplitConcat p (s : Concat p' (f : rest)), ListSplitConcat p' (f : rest))
listSplitSuff2 :: ListSplitD l p (f : l') -> ListSplitD l' p' (s : rest) -> (ListSplitConcat p (Concat p' rest), ListSplitConcat p' rest)
pattern Split0 :: ListSplitD l '[] l
pattern Split1 :: ListSplitD (x0 : l) '[x0] l
pattern Split2 :: ListSplitD (x0 : (x1 : l)) (x0 : '[x1]) l
pattern Split3 :: ListSplitD (x0 : (x1 : (x2 : l))) (x0 : (x1 : '[x2])) l
pattern Split4 :: ListSplitD (x0 : (x1 : (x2 : (x3 : l)))) (x0 : (x1 : (x2 : '[x3]))) l
pattern Split5 :: ListSplitD (x0 : (x1 : (x2 : (x3 : (x4 : l))))) (x0 : (x1 : (x2 : (x3 : '[x4])))) l
hlistDrop :: ListSplitD l p s -> HList f l -> HList f s
hlistTakeHead :: HList f (x : xs) -> HList f '[x]
pattern HListMatch0 :: HList f '[]
pattern HListMatch1 :: f a -> HList f '[a]
pattern HListMatch2 :: f a -> f a' -> HList f '[a, a']
pattern HListMatch3 :: f a -> f a' -> f a'' -> HList f '[a, a', a'']
data HList2 f (x :: [a]) (y :: [b]) where
- HNil2 :: HList2 f '[] '[]
- HCons2 :: f x y -> HList2 f xs ys -> HList2 f (x : xs) (y : ys)
pattern HList2Match0 :: HList2 f '[] '[]
pattern HList2Match1 :: f a b -> HList2 f '[a] '[b]
pattern HList2Match2 :: f a b -> f a' b' -> HList2 f '[a, a'] '[b, b']
pattern HList2Match3 :: f a b -> f a' b' -> f a'' b'' -> HList2 f '[a, a', a''] '[b, b', b'']
(!!) :: HList f types -> InList types x -> f x
forIthFst :: Monad m => InList xs x -> HList2 f xs ys -> (forall y. f x y -> m (f x y, z)) -> m (HList2 f xs ys, z)
forIth :: Monad m => InList types x -> HList f types -> (f x -> m (f x, z)) -> m (HList f types, z)
hMap :: (forall a. InList types a -> f a -> g a) -> HList f types -> HList g types
homogenize :: forall t (types :: [t]) (f :: t -> Type) a. (forall x. InList types x -> f x -> a) -> HList f types -> [a]
knownLenToSplit :: KnownLenD p -> ListSplitD (Concat p s) p s
splitHList :: ListSplitD l p s -> HList f l -> (HList f p, HList f s)
someRxMessThere :: SomeRxMess ports' -> SomeRxMess (x : ports')
data ConstrAllD (c :: Type -> Constraint) (l :: [Type]) where
- ConstrAllNil :: ConstrAllD c '[]
- ConstrAllCons :: c t => ConstrAllD c l -> ConstrAllD c (t : l)
knownLenfromConstrAllD :: ConstrAllD c l -> KnownLenD l
class ConstrAll c l where
- getConstrAllD :: ConstrAllD c l
data HListShow l where
- HListShow :: ConstrAllD Ord l -> HList Identity l -> HListShow l

Dependent pointer into a list

data InList xs x where #

Dependent index of an element of type (x, y) in list xs

We use lists of pairs to encode the ports an algorithm has access to, as well heterogenous lists HList that occur during interpretation of our algorithms. And this type serves as a pointer into one of such ports in the list.

Constructors

Here :: InList (x : xs) x
There :: InList xs x -> InList (y : xs) x

Instances

Instances details

TestEquality (InList xs :: k -> Type) #	Compare two indices for equality
Instance details Defined in Data.HList Methods testEquality :: forall (a :: k0) (b :: k0). InList xs a -> InList xs b -> Maybe (a :~: b) #

pattern There2 :: InList xs x -> InList (y0 : (y1 : xs)) x #

pattern There3 :: InList xs x -> InList (y0 : (y1 : (y2 : xs))) x #

pattern There4 :: InList xs x -> InList (y0 : (y1 : (y2 : (y3 : xs)))) x #

pattern There5 :: InList xs x -> InList (y0 : (y1 : (y2 : (y3 : (y4 : xs))))) x #

pattern There6 :: InList xs x -> InList (y0 : (y1 : (y2 : (y3 : (y4 : (y5 : xs)))))) x #

pattern InList0 :: InList (x : xs) x #

pattern InList1 :: InList (y0 : (x : xs)) x #

pattern InList2 :: InList (y0 : (y1 : (x : xs))) x #

pattern InList3 :: InList (y0 : (y1 : (y2 : (x : xs)))) x #

pattern InList4 :: InList (y0 : (y1 : (y2 : (y3 : (x : xs))))) x #

pattern InList5 :: InList (y0 : (y1 : (y2 : (y3 : (y4 : (x : xs)))))) x #

pattern InList6 :: InList (y0 : (y1 : (y2 : (y3 : (y4 : (y5 : (x : xs))))))) x #

data SomeIndex xs where #

Constructors

SomeIndex :: InList xs x -> SomeIndex xs

data SomeValue xs where #

Constructors

SomeValue :: InList xs x -> x -> SomeValue xs

padMessageIndex :: SomeValue ts -> SomeValue (t : ts) #

Pad the index to make it valid after applying (::) to the list.

Port Lists

data Port #

A port is defined by a pair of types.

A :> B allows asyncronously sending values of type A and receiving B.
A :|> B allows to do the same syncronously,
A :>| B allows serving syncronous requests.

Constructors

Type :> Type

Instances

Instances details

KnownHPPorts ('[] :: [Port]) #
Instance details Defined in Data.HList Methods getKnownHPPorts :: KnownHPPortsD '[] #
(KnownHPPorts ports, p ~ (HListPair xl xr ':> HListPair yl yr)) => KnownHPPorts (p ': ports) #
Instance details Defined in Data.HList Methods getKnownHPPorts :: KnownHPPortsD (p ': ports) #

type family PortTxType p where ... #

Equations

PortTxType (x :> _) = x

type family PortRxType p where ... #

Equations

PortRxType (_ :> x) = x

type family PortDual p where ... #

Equations

PortDual (x :> y) = y :> x

type PortInList x y xs = InList xs (x :> y) #

A pointer into the list of ports xs.

The PortInList x y xs is a proof of x :> y being in xs.

type family Fst p where ... #

Equations

Fst '(x, _) = x

type family MapFst l where ... #

Equations

MapFst '[] = '[]
MapFst ('(x, y) : l) = x : MapFst l

type family Snd p where ... #

Equations

Snd '(_, y) = y

type family Zip l l' where ... #

Equations

Zip '[] '[] = '[]
Zip (x : xs) (y : ys) = '(x, y) : Zip xs ys

data SomeRxMess xs where #

Constructors

SomeRxMess :: InList xs p -> PortRxType p -> SomeRxMess xs

data SomeTxMess xs where #

Constructors

SomeTxMess :: InList xs p -> PortTxType p -> SomeTxMess xs

Heterogenous Lists

data HList f (types :: [a]) where #

Heterogenous List

Constructors

HNil :: HList f '[]
HCons :: f t -> HList f ts -> HList f (t : ts)

Instances

Instances details

Flattenable (HListPair '[sid] '[Pid]) #
Instance details Defined in LambdaUC.UC.Flatten Methods getFlattenableD :: FlattenableD (HListPair '[sid] '[Pid]) #
Flattenable (HListPair '[sid] ('[] :: [Type])) #
Instance details Defined in LambdaUC.UC.Flatten Methods getFlattenableD :: FlattenableD (HListPair '[sid] '[]) #
Flattenable (HListPair ('[] :: [Type]) '[Pid, m]) #
Instance details Defined in LambdaUC.UC.Flatten Methods getFlattenableD :: FlattenableD (HListPair '[] '[Pid, m]) #
Flattenable (HListPair ('[] :: [Type]) '[m]) #
Instance details Defined in LambdaUC.UC.Flatten Methods getFlattenableD :: FlattenableD (HListPair '[] '[m]) #

data KnownHPPortsD ports where #

Constructors

KnownHPPortsZ :: KnownHPPortsD '[]
KnownHPPortsS :: KnownHPPortsD ports -> KnownHPPortsD ((HListPair xl xr :> HListPair yl yr) : ports)

type HListPair l r = (HList Identity l, HList Identity r) #

type family Concat2 l r p where ... #

Equations

Concat2 l r (HListPair lx rx :> HListPair ly ry) = HListPair (Concat l lx) (Concat r rx) :> HListPair (Concat l ly) (Concat r ry)

type family MapConcat2 l r ports where ... #

Equations

MapConcat2 _ _ '[] = '[]
MapConcat2 l r (p : ports) = Concat2 l r p : MapConcat2 l r ports

(++) :: HList f l -> HList f r -> HList f (Concat l r) #

(+++) :: HListPair l r -> HListPair l' r' -> HListPair (Concat l l') (Concat r r') #

class KnownHPPorts ports where #

Methods

getKnownHPPorts :: KnownHPPortsD ports #

Instances

Instances details

KnownHPPorts ('[] :: [Port]) #
Instance details Defined in Data.HList Methods getKnownHPPorts :: KnownHPPortsD '[] #
(KnownHPPorts ports, p ~ (HListPair xl xr ':> HListPair yl yr)) => KnownHPPorts (p ': ports) #
Instance details Defined in Data.HList Methods getKnownHPPorts :: KnownHPPortsD (p ': ports) #

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') #

type family Concat xs ys where ... #

Equations

Concat '[] ys = ys
Concat (x : xs) ys = x : Concat xs ys

concatAssocPrf :: forall p p' s' l s. ListSplitD l p s -> Concat p (Concat p' s') :~: Concat (Concat p p') s' #

Proof of `p ++ (p' ++ s') == (p ++ p') ++ s'`.

concatInjPrf :: forall xs ys ys'. (Concat xs ys :~: Concat xs ys') -> KnownLenD xs -> ys :~: ys' #

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

Statement ListSplitD l p s says that l = p ++ s, i.e. that l can be cut into prefix p and suffix s.

Structure-wise, this is just a pointer, like InList, but it carries different information on type-level.

Constructors

SplitHere :: ListSplitD l '[] l
SplitThere :: ListSplitD l p s -> ListSplitD (x : l) (x : p) s

type ListSplitConcat p s = ListSplitD (Concat p s) p s #

class ListSplit l p s where #

Methods

getListSplit :: ListSplitD l p s #

Instances

Instances details

(KnownLen p, l ~ Concat p s) => ListSplit (l :: [a]) (p :: [a]) (s :: [a]) #
Instance details Defined in Data.HList Methods getListSplit :: ListSplitD l p s #

getListSplit' :: KnownLenD p -> ListSplitD (Concat p s) p s #

listSplitConcat :: ListSplitD l p s -> Concat p s :~: l #

listSplitAdd :: ListSplitD l p s -> ListSplitD s p' s' -> ListSplitD l (Concat p p') s' #

listConcatSplit :: ListSplitD l p s -> ListSplitD (Concat p s') p s' #

listSplitPopSuffix :: ListSplitD (Concat p (x : s)) p (x : s) -> ListSplitD (Concat p s) p s #

listSplitSubst :: ListSplitD l' p' (s : rest) -> ListSplitConcat p' (f : rest) #

listSplitSwap :: ListSplitD l p (f : l') -> ListSplitD l' p' (s : rest) -> (ListSplitConcat p (s : Concat p' (f : rest)), ListSplitConcat p' (f : rest)) #

listSplitSuff2 :: ListSplitD l p (f : l') -> ListSplitD l' p' (s : rest) -> (ListSplitConcat p (Concat p' rest), ListSplitConcat p' rest) #

pattern Split0 :: ListSplitD l '[] l #

pattern Split1 :: ListSplitD (x0 : l) '[x0] l #

pattern Split2 :: ListSplitD (x0 : (x1 : l)) (x0 : '[x1]) l #

pattern Split3 :: ListSplitD (x0 : (x1 : (x2 : l))) (x0 : (x1 : '[x2])) l #

pattern Split4 :: ListSplitD (x0 : (x1 : (x2 : (x3 : l)))) (x0 : (x1 : (x2 : '[x3]))) l #

pattern Split5 :: ListSplitD (x0 : (x1 : (x2 : (x3 : (x4 : l))))) (x0 : (x1 : (x2 : (x3 : '[x4])))) l #

hlistDrop :: ListSplitD l p s -> HList f l -> HList f s #

hlistTakeHead :: HList f (x : xs) -> HList f '[x] #

pattern HListMatch0 :: HList f '[] #

pattern HListMatch1 :: f a -> HList f '[a] #

pattern HListMatch2 :: f a -> f a' -> HList f '[a, a'] #

pattern HListMatch3 :: f a -> f a' -> f a'' -> HList f '[a, a', a''] #

data HList2 f (x :: [a]) (y :: [b]) where #

Heterigenous zip of two lists

Constructors

HNil2 :: HList2 f '[] '[]
HCons2 :: f x y -> HList2 f xs ys -> HList2 f (x : xs) (y : ys)

pattern HList2Match0 :: HList2 f '[] '[] #

pattern HList2Match1 :: f a b -> HList2 f '[a] '[b] #

pattern HList2Match2 :: f a b -> f a' b' -> HList2 f '[a, a'] '[b, b'] #

pattern HList2Match3 :: f a b -> f a' b' -> f a'' b'' -> HList2 f '[a, a', a''] '[b, b', b''] #

(!!) :: HList f types -> InList types x -> f x #

Fetch the value under given index. Statically checked version of Prelude.(!!).

forIthFst #

Arguments

:: Monad m
=> InList xs x	Element index
-> HList2 f xs ys	List
-> (forall y. f x y -> m (f x y, z))	Action
-> m (HList2 f xs ys, z)

Applies given mutating action to one of the elements in the list

forIth #

Arguments

:: Monad m
=> InList types x	Action
-> HList f types	Element index
-> (f x -> m (f x, z))	List
-> m (HList f types, z)

Applies given mutating action to one of the elements in the list

hMap :: (forall a. InList types a -> f a -> g a) -> HList f types -> HList g types #

Like map, but for HList.

homogenize :: forall t (types :: [t]) (f :: t -> Type) a. (forall x. InList types x -> f x -> a) -> HList f types -> [a] #

Convert HList to a regular list.

knownLenToSplit :: KnownLenD p -> ListSplitD (Concat p s) p s #

splitHList :: ListSplitD l p s -> HList f l -> (HList f p, HList f s) #

someRxMessThere :: SomeRxMess ports' -> SomeRxMess (x : ports') #

data ConstrAllD (c :: Type -> Constraint) (l :: [Type]) where #

Constructors

ConstrAllNil :: ConstrAllD c '[]
ConstrAllCons :: c t => ConstrAllD c l -> ConstrAllD c (t : l)

knownLenfromConstrAllD :: ConstrAllD c l -> KnownLenD l #

class ConstrAll c l where #

Methods

getConstrAllD :: ConstrAllD c l #

Instances

Instances details

ConstrAll c ('[] :: [Type]) #
Instance details Defined in Data.HList Methods getConstrAllD :: ConstrAllD c '[] #
(c t, ConstrAll c l) => ConstrAll c (t ': l) #
Instance details Defined in Data.HList Methods getConstrAllD :: ConstrAllD c (t ': l) #

data HListShow l where #

Constructors

HListShow :: ConstrAllD Ord l -> HList Identity l -> HListShow l

Instances

Instances details

Eq (HListShow l) #
Instance details Defined in Data.HList Methods (==) :: HListShow l -> HListShow l -> Bool # (/=) :: HListShow l -> HListShow l -> Bool #
Ord (HListShow l) #
Instance details Defined in Data.HList Methods compare :: HListShow l -> HListShow l -> Ordering # (<) :: HListShow l -> HListShow l -> Bool # (<=) :: HListShow l -> HListShow l -> Bool # (>) :: HListShow l -> HListShow l -> Bool # (>=) :: HListShow l -> HListShow l -> Bool # max :: HListShow l -> HListShow l -> HListShow l # min :: HListShow l -> HListShow l -> HListShow l #