Safe Haskell	None
Language	Haskell98

Data.Witness.List

Synopsis

Documentation

data ListType w lt where Source

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) Source
Representative * w => Representative * (ListType w) Source
Eq1 * w => Eq1 * (ListType w) Source
Representative * w => Is * (ListType w) () Source
(Is * w a, Is * (ListType w) lt) => Is * (ListType w) (a, lt) Source
Eq1 * w => Eq (ListType w a) Source

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

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

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

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

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

listIdentity :: ListType Identity lt -> lt Source

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

data AppendList w la lb Source

Constructors

forall lr . 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 Source

data AddItemList w a l Source

Constructors

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

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

data MergeItemList w a l Source

Constructors

forall lr . 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 Source

data MergeList w la lb Source

Constructors

forall lr . 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 Source

class Tensor cc where Source

Methods

tensorUnit :: cc () () Source

tensorPair :: cc a1 b1 -> cc a2 b2 -> cc (a1, a2) (b1, b2) Source

Instances

Tensor (->) Source
Tensor cc => Tensor (Dual cc) Source

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

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

data MapList cc w2 l Source

Constructors

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

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

data RemoveFromList w a l Source

Constructors

forall lr . 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 Source

data RemoveManyFromList wit lx l Source

Constructors

forall lr . 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 Source

newtype EitherWitness w1 w2 a Source

Constructors

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

Instances

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

data PartitionList wit1 wit2 l Source

Constructors

forall l1 l2 . 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 Source