Data.Witness.List

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)

Methods

testEquality :: f a -> f b -> Maybe ((ListType w :~: a) b)

Representative * w => Representative * (ListType w)

Methods

getRepWitness :: rep a -> Dict (Is (ListType w) rep a)

Eq1 * w => Eq1 * (ListType w)

Methods

equals1 :: p a -> p a -> Bool

Representative * w => Is * (ListType w) ()

Methods

representative :: () a

(Is * w a, Is * (ListType w) lt) => Is * (ListType w) (a, lt)

Methods

representative :: (a, lt) a

Eq1 * w => Eq (ListType w a)

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 w2 a

Constructors

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

Instances

(TestEquality k w1, TestEquality k w2) => TestEquality k (EitherWitness k w1 w2)

Methods

testEquality :: f a -> f b -> Maybe ((EitherWitness k w1 w2 :~: 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