-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/


-- | values that witness types
--   
--   A witness is a value that <i>witnesses</i> some sort of constraint on
--   some list of type variables. This library provides support for simple
--   witnesses, that constrain a type variable to a single type, and
--   equality witnesses, that constrain two type variables to be the same
--   type. It also provides classes for representatives, which are values
--   that represent types. See the paper <i>Witnesses and Open
--   Witnesses</i> (<a>http://semantic.org/stuff/Open-Witnesses.pdf</a>).
@package witness
@version 0.4

module Control.Category.Tensor
class Tensor cc
tensorUnit :: Tensor cc => cc () ()
tensorPair :: Tensor cc => cc a1 b1 -> cc a2 b2 -> cc (a1, a2) (b1, b2)
instance Control.Category.Tensor.Tensor (->)
instance Control.Category.Tensor.Tensor cc => Control.Category.Tensor.Tensor (Data.Semigroupoid.Dual.Dual cc)

module Data.Nat
data Nat
Zero :: Nat
Succ :: Nat -> Nat
addNat :: Nat -> Nat -> Nat

-- | subtractFromNat a b = b - a
subtractFromNat :: Nat -> Nat -> Maybe Nat
multiplyNat :: Nat -> Nat -> Nat

module Data.Witness.Any

-- | Any value with a witness to it.
data Any (w :: * -> *)
MkAny :: w a -> a -> Any
matchAny :: TestEquality w => w a -> Any w -> Maybe a

-- | Any value with a witness to a parameter of its type.
data AnyF (w :: k -> *) (f :: k -> *)
MkAnyF :: w a -> f a -> AnyF
matchAnyF :: TestEquality w => w a -> AnyF w f -> Maybe (f a)

-- | Any witness.
data AnyWitness (w :: k -> *)
MkAnyWitness :: w a -> AnyWitness
matchAnyWitness :: TestEquality w => w a -> AnyWitness w -> Bool
instance forall k (w :: k -> *). Data.Type.Equality.TestEquality w => GHC.Classes.Eq (Data.Witness.Any.AnyWitness w)

module Data.Witness.Representative
class Eq1 (p :: k -> *)
equals1 :: forall a. Eq1 p => p a -> p a -> Bool
isWitnessRepresentative :: Dict (Is rep a) -> rep a
class Eq1 rep => Representative (rep :: k -> *)

-- | Every value is an instance of <a>Is</a>.
getRepWitness :: forall (a :: k). Representative rep => rep a -> Dict (Is rep a)
withRepresentative :: forall (rep :: k -> *) r. Representative rep => (forall (a :: k). Is rep a => rep a -> r) -> forall (b :: k). rep b -> r

-- | If two representatives have the same type, then they have the same
--   value.
class Representative rep => Is (rep :: k -> *) (a :: k)

-- | The representative value for type <tt>a</tt>.
representative :: Is rep a => rep a
getRepresentative :: Is rep a => a -> rep a
rerepresentative :: Is rep a => p a -> rep a
mkAny :: Is rep a => a -> Any rep
mkAnyF :: Is rep a => f a -> AnyF rep f
instance Data.Witness.Representative.Representative Data.Proxy.Proxy
instance forall k (a :: k). Data.Witness.Representative.Is Data.Proxy.Proxy a
instance Data.Witness.Representative.Eq1 Data.Proxy.Proxy

module Data.Witness.Nat
data NatType (t :: Nat)
[ZeroType] :: NatType  'Zero
[SuccType] :: NatType t -> NatType ( 'Succ t)
instance Data.Type.Equality.TestEquality Data.Witness.Nat.NatType
instance Data.Witness.Representative.Eq1 Data.Witness.Nat.NatType
instance Data.Witness.Representative.Representative Data.Witness.Nat.NatType
instance Data.Witness.Representative.Is Data.Witness.Nat.NatType 'Data.Nat.Zero
instance Data.Witness.Representative.Is Data.Witness.Nat.NatType n => Data.Witness.Representative.Is Data.Witness.Nat.NatType ('Data.Nat.Succ n)

module Data.Witness.ListElement
class HasListElement (n :: Nat) (list :: *) where {
    type family ListElement n list :: *;
}
getListElement :: HasListElement n list => NatType n -> list -> ListElement n list
putListElement :: HasListElement n list => NatType n -> ListElement n list -> list -> list
modifyListElement :: HasListElement n t => NatType n -> (ListElement n t -> ListElement n t) -> t -> t
instance Data.Witness.ListElement.HasListElement 'Data.Nat.Zero (a, r)
instance Data.Witness.ListElement.HasListElement n r => Data.Witness.ListElement.HasListElement ('Data.Nat.Succ n) (a, r)

module Data.Witness.List

-- | a witness type for HList-style lists. The <tt>w</tt> parameter is the
--   witness type of the elements.
data ListType (w :: * -> *) (lt :: *)
[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 :: ListType w lr -> (la -> lb -> lr) -> (lr -> (la, lb)) -> AppendList w la lb
[listAppendWitness] :: AppendList w la lb -> ListType w lr
[listAppend] :: AppendList w la lb -> la -> lb -> lr
[listSplit] :: AppendList w la lb -> lr -> (la, lb)
appendList :: ListType w la -> ListType w lb -> AppendList w la lb
data AddItemList w a l
MkAddItemList :: ListType w lr -> (a -> l -> lr) -> (lr -> (a, l)) -> AddItemList w a l
[listAddItemWitness] :: AddItemList w a l -> ListType w lr
[listAddItem] :: AddItemList w a l -> a -> l -> lr
[listSplitItem] :: AddItemList w a l -> lr -> (a, l)
addListItem :: w a -> ListType w l -> AddItemList w a l
data MergeItemList w a l
MkMergeItemList :: ListType w lr -> ((Maybe a -> a) -> l -> lr) -> (lr -> (a, l)) -> MergeItemList w a l
[listMergeItemWitness] :: MergeItemList w a l -> ListType w lr
[listMergeItem] :: MergeItemList w a l -> (Maybe a -> a) -> l -> lr
[listUnmergeItem] :: MergeItemList w a l -> lr -> (a, l)
mergeListItem :: TestEquality w => ListType w l -> w a -> MergeItemList w a l
data MergeList w la lb
MkMergeList :: ListType w lr -> ((forall t. w t -> t -> t -> t) -> la -> lb -> lr) -> (lr -> (la, lb)) -> MergeList w la lb
[listMergeWitness] :: MergeList w la lb -> ListType w lr
[listMerge] :: MergeList w la lb -> (forall t. w t -> t -> t -> t) -> la -> lb -> lr
[listUnmerge] :: MergeList w la lb -> 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 :: ListType w2 lr -> cc l lr -> MapList cc w2 l
[listMapWitness] :: MapList cc w2 l -> ListType w2 lr
[listMapW] :: MapList cc w2 l -> cc l lr
mapList :: Tensor cc => MapWitness cc w1 w2 -> ListType w1 l -> MapList cc w2 l
data RemoveFromList w a l
MkRemoveFromList :: ListType w lr -> (a -> lr -> l) -> (l -> lr) -> RemoveFromList w a l
[listRemoveWitness] :: RemoveFromList w a l -> ListType w lr
[listInsert] :: RemoveFromList w a l -> a -> lr -> l
[listRemove] :: RemoveFromList w a l -> l -> lr
removeAllMatching :: TestEquality w => w a -> ListType w l -> RemoveFromList w a l
data RemoveManyFromList wit lx l
MkRemoveManyFromList :: ListType wit lr -> (lx -> lr -> l) -> (l -> lr) -> RemoveManyFromList wit lx l
[listRemoveManyWitness] :: RemoveManyFromList wit lx l -> ListType wit lr
[listInsertMany] :: RemoveManyFromList wit lx l -> lx -> lr -> l
[listRemoveMany] :: RemoveManyFromList wit lx l -> 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) -> EitherWitness
data PartitionList wit1 wit2 l
MkPartitionList :: ListType wit1 l1 -> ListType wit2 l2 -> (l1 -> l2 -> l) -> (l -> l1) -> (l -> l2) -> PartitionList wit1 wit2 l
[listPartitionWitness1] :: PartitionList wit1 wit2 l -> ListType wit1 l1
[listPartitionWitness2] :: PartitionList wit1 wit2 l -> ListType wit2 l2
[listFromPartition] :: PartitionList wit1 wit2 l -> l1 -> l2 -> l
[listToPartition1] :: PartitionList wit1 wit2 l -> l -> l1
[listToPartition2] :: PartitionList wit1 wit2 l -> l -> l2
partitionList :: ListType (EitherWitness w1 w2) l -> PartitionList w1 w2 l
instance forall k (w1 :: k -> *) (w2 :: k -> *). (Data.Type.Equality.TestEquality w1, Data.Type.Equality.TestEquality w2) => Data.Type.Equality.TestEquality (Data.Witness.List.EitherWitness w1 w2)
instance Data.Witness.Representative.Eq1 w => Data.Witness.Representative.Eq1 (Data.Witness.List.ListType w)
instance Data.Witness.Representative.Eq1 w => GHC.Classes.Eq (Data.Witness.List.ListType w a)
instance Data.Witness.Representative.Representative w => Data.Witness.Representative.Representative (Data.Witness.List.ListType w)
instance Data.Witness.Representative.Representative w => Data.Witness.Representative.Is (Data.Witness.List.ListType w) ()
instance (Data.Witness.Representative.Is w a, Data.Witness.Representative.Is (Data.Witness.List.ListType w) lt) => Data.Witness.Representative.Is (Data.Witness.List.ListType w) (a, lt)
instance Data.Type.Equality.TestEquality w => Data.Type.Equality.TestEquality (Data.Witness.List.ListType w)

module Data.Witness.WitnessDict

-- | A dictionary that is heterogenous up to its simple witness type
--   <tt>w</tt>. Witnesses are the keys of the dictionary, and the values
--   they witness are the values of the dictionary.
newtype WitnessDict (w :: * -> *)
MkWitnessDict :: [Any w] -> WitnessDict

-- | An empty dictionary.
emptyWitnessDict :: WitnessDict w

-- | Look up the first value in the dictionary that matches the given
--   witness.
witnessDictLookup :: TestEquality w => w a -> WitnessDict w -> Maybe a

-- | Modify the first value in the dictionary that matches a particular
--   witness.
witnessDictModify :: TestEquality w => w a -> (a -> a) -> WitnessDict w -> WitnessDict w

-- | Replace the first value in the dictionary that matches the witness
witnessDictReplace :: TestEquality w => w a -> a -> WitnessDict w -> WitnessDict w

-- | Add a witness and value as the first entry in the dictionary.
witnessDictAdd :: w a -> a -> WitnessDict w -> WitnessDict w

-- | Remove the first entry in the dictionary that matches the given
--   witness.
witnessDictRemove :: TestEquality w => w a -> WitnessDict w -> WitnessDict w

-- | Create a dictionary from a list of witness/value pairs
witnessDictFromList :: [Any w] -> WitnessDict w

module Data.Witness.WitnessFDict

-- | A dictionary that is heterogenous up to its simple witness type
--   <tt>w</tt>. Witnesses are the keys of the dictionary, and the values
--   they witness are the values of the dictionary.
newtype WitnessFDict (w :: k -> *) (f :: k -> *)
MkWitnessFDict :: [AnyF w f] -> WitnessFDict

-- | An empty dictionary.
emptyWitnessFDict :: WitnessFDict w f

-- | Look up the first value in the dictionary that matches the given
--   witness.
witnessFDictLookup :: TestEquality w => w a -> WitnessFDict w f -> Maybe (f a)

-- | Modify the first value in the dictionary that matches a particular
--   witness.
witnessFDictModify :: TestEquality w => w a -> (f a -> f a) -> WitnessFDict w f -> WitnessFDict w f

-- | Replace the first value in the dictionary that matches the witness
witnessFDictReplace :: TestEquality w => w a -> f a -> WitnessFDict w f -> WitnessFDict w f

-- | Add a witness and value as the first entry in the dictionary.
witnessFDictAdd :: w a -> f a -> WitnessFDict w f -> WitnessFDict w f

-- | Remove the first entry in the dictionary that matches the given
--   witness.
witnessFDictRemove :: TestEquality w => w a -> WitnessFDict w f -> WitnessFDict w f

-- | Create a dictionary from a list of witness/value pairs
witnessFDictFromList :: [AnyF w f] -> WitnessFDict w f

module Data.Witness

-- | See whether two represented and witnessed types are the same.
matchIs :: forall w a b. (TestEquality w, Is w a, Is w b) => Proxy w -> Maybe (a :~: b)
