Safe Haskell	None
Language	Haskell98

Data.Witness.List

Synopsis

data ListType (w :: * -> *) (lt :: *) where
- NilListType :: ListType w ()
- ConsListType :: w a -> ListType w lt -> ListType w (a, lt)
listFill :: ListType w t -> (forall a. w a -> a) -> t
listMap :: ListType w t -> (forall a. w a -> a -> a) -> t -> t
listLift2 :: ListType w t -> (forall a. w a -> a -> a -> a) -> t -> t -> t
listTypeToList :: (forall a. w a -> r) -> ListType w t -> [r]
listTypeMap :: (forall a. w1 a -> w2 a) -> ListType w1 t -> ListType w2 t
listIdentity :: ListType Identity lt -> lt
listSequence :: Applicative f => ListType f lt -> f lt
data AppendList w la lb = MkAppendList {
- listAppendWitness :: ListType w lr
- listAppend :: la -> lb -> lr
- listSplit :: lr -> (la, lb)
}
appendList :: ListType w la -> ListType w lb -> AppendList w la lb
data AddItemList w a l = MkAddItemList {
- listAddItemWitness :: ListType w lr
- listAddItem :: a -> l -> lr
- listSplitItem :: lr -> (a, l)
}
addListItem :: w a -> ListType w l -> AddItemList w a l
data MergeItemList w a l = MkMergeItemList {
- listMergeItemWitness :: ListType w lr
- listMergeItem :: (Maybe a -> a) -> l -> lr
- listUnmergeItem :: lr -> (a, l)
}
mergeListItem :: TestEquality w => ListType w l -> w a -> MergeItemList w a l
data MergeList w la lb = MkMergeList {
- listMergeWitness :: ListType w lr
- listMerge :: (forall t. w t -> t -> t -> t) -> la -> lb -> lr
- listUnmerge :: lr -> (la, lb)
}
mergeList :: TestEquality w => ListType w la -> ListType w lb -> MergeList w la lb
type MapWitness cc w1 w2 = forall r v1. w1 v1 -> (forall v2. w2 v2 -> cc v1 v2 -> r) -> r
sameMapWitness :: (forall v. w v -> cc v v) -> MapWitness cc w w
data MapList cc w2 l = MkMapList {
- listMapWitness :: ListType w2 lr
- listMapW :: cc l lr
}
mapList :: Tensor cc => MapWitness cc w1 w2 -> ListType w1 l -> MapList cc w2 l
data RemoveFromList w a l = MkRemoveFromList {
- listRemoveWitness :: ListType w lr
- listInsert :: a -> lr -> l
- listRemove :: l -> lr
}
removeAllMatching :: TestEquality w => w a -> ListType w l -> RemoveFromList w a l
data RemoveManyFromList wit lx l = MkRemoveManyFromList {
- listRemoveManyWitness :: ListType wit lr
- listInsertMany :: lx -> lr -> l
- listRemoveMany :: l -> lr
}
removeAllMatchingMany :: TestEquality wit => ListType wit lx -> ListType wit l -> RemoveManyFromList wit lx l
newtype EitherWitness (w1 :: k -> *) (w2 :: k -> *) (a :: k) = MkEitherWitness (Either (w1 a) (w2 a))
data PartitionList wit1 wit2 l = MkPartitionList {
- listPartitionWitness1 :: ListType wit1 l1
- listPartitionWitness2 :: ListType wit2 l2
- listFromPartition :: l1 -> l2 -> l
- listToPartition1 :: l -> l1
- listToPartition2 :: l -> l2
}
partitionList :: ListType (EitherWitness w1 w2) l -> PartitionList w1 w2 l

Documentation

data ListType (w :: * -> *) (lt :: *) where #

a witness type for HList-style lists. The w parameter is the witness type of the elements.

Constructors

NilListType :: ListType w ()
ConsListType :: w a -> ListType w lt -> ListType w (a, lt)

Instances

TestEquality w => TestEquality (ListType w :: * -> *) #
Instance details Defined in Data.Witness.List Methods testEquality :: ListType w a -> ListType w b -> Maybe (a :~: b) #
Representative w => Representative (ListType w :: * -> *) #
Instance details Defined in Data.Witness.List Methods getRepWitness :: ListType w a -> Dict (Is (ListType w) a) #
Eq1 w => Eq1 (ListType w :: * -> *) #
Instance details Defined in Data.Witness.List Methods equals1 :: ListType w a -> ListType w a -> Bool #
Representative w => Is (ListType w :: * -> *) () #
Instance details Defined in Data.Witness.List Methods representative :: ListType w () #
(Is w a, Is (ListType w) lt) => Is (ListType w :: * -> ) ((a, lt) :: ) #
Instance details Defined in Data.Witness.List Methods representative :: ListType w (a, lt) #
Eq1 w => Eq (ListType w a) #
Instance details Defined in Data.Witness.List Methods (==) :: ListType w a -> ListType w a -> Bool # (/=) :: ListType w a -> ListType w a -> Bool #

listFill :: ListType w t -> (forall a. w a -> a) -> t #

listMap :: ListType w t -> (forall a. w a -> a -> a) -> t -> t #

listLift2 :: ListType w t -> (forall a. w a -> a -> a -> a) -> t -> t -> t #

listTypeToList :: (forall a. w a -> r) -> ListType w t -> [r] #

listTypeMap :: (forall a. w1 a -> w2 a) -> ListType w1 t -> ListType w2 t #

listIdentity :: ListType Identity lt -> lt #

listSequence :: Applicative f => ListType f lt -> f lt #

data AppendList w la lb #

Constructors

MkAppendList
Fields listAppendWitness :: ListType w lr listAppend :: la -> lb -> lr listSplit :: lr -> (la, lb)

appendList :: ListType w la -> ListType w lb -> AppendList w la lb #

data AddItemList w a l #

Constructors

MkAddItemList
Fields listAddItemWitness :: ListType w lr listAddItem :: a -> l -> lr listSplitItem :: lr -> (a, l)

addListItem :: w a -> ListType w l -> AddItemList w a l #

data MergeItemList w a l #

Constructors

MkMergeItemList
Fields listMergeItemWitness :: ListType w lr listMergeItem :: (Maybe a -> a) -> l -> lr listUnmergeItem :: lr -> (a, l)

mergeListItem :: TestEquality w => ListType w l -> w a -> MergeItemList w a l #

data MergeList w la lb #

Constructors

MkMergeList
Fields listMergeWitness :: ListType w lr listMerge :: (forall t. w t -> t -> t -> t) -> la -> lb -> lr listUnmerge :: lr -> (la, lb)

mergeList :: TestEquality w => ListType w la -> ListType w lb -> MergeList w la lb #

type MapWitness cc w1 w2 = forall r v1. w1 v1 -> (forall v2. w2 v2 -> cc v1 v2 -> r) -> r #

sameMapWitness :: (forall v. w v -> cc v v) -> MapWitness cc w w #

data MapList cc w2 l #

Constructors

MkMapList
Fields listMapWitness :: ListType w2 lr listMapW :: cc l lr

mapList :: Tensor cc => MapWitness cc w1 w2 -> ListType w1 l -> MapList cc w2 l #

data RemoveFromList w a l #

Constructors

MkRemoveFromList
Fields listRemoveWitness :: ListType w lr listInsert :: a -> lr -> l listRemove :: l -> lr

removeAllMatching :: TestEquality w => w a -> ListType w l -> RemoveFromList w a l #

data RemoveManyFromList wit lx l #

Constructors

MkRemoveManyFromList
Fields listRemoveManyWitness :: ListType wit lr listInsertMany :: lx -> lr -> l listRemoveMany :: l -> lr

removeAllMatchingMany :: TestEquality wit => ListType wit lx -> ListType wit l -> RemoveManyFromList wit lx l #

newtype EitherWitness (w1 :: k -> *) (w2 :: k -> *) (a :: k) #

Constructors

MkEitherWitness (Either (w1 a) (w2 a))

Instances

(TestEquality w1, TestEquality w2) => TestEquality (EitherWitness w1 w2 :: k -> *) #
Instance details Defined in Data.Witness.List Methods testEquality :: EitherWitness w1 w2 a -> EitherWitness w1 w2 b -> Maybe (a :~: b) #

data PartitionList wit1 wit2 l #

Constructors

MkPartitionList
Fields listPartitionWitness1 :: ListType wit1 l1 listPartitionWitness2 :: ListType wit2 l2 listFromPartition :: l1 -> l2 -> l listToPartition1 :: l -> l1 listToPartition2 :: l -> l2

partitionList :: ListType (EitherWitness w1 w2) l -> PartitionList w1 w2 l #