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