| Safe Haskell | None |
|---|---|
| Language | GHC2021 |
Data.Type.Witness.Specific.List.List
Synopsis
- data ListType (w :: k -> Type) (lt :: [k]) where
- NilListType :: forall {k} (w :: k -> Type). ListType w ('[] :: [k])
- ConsListType :: forall {k} (w :: k -> Type) (a :: k) (lt1 :: [k]). w a -> ListType w lt1 -> ListType w (a ': lt1)
- assembleListType :: forall {k} (w :: k -> Type). [Some w] -> Some (ListType w)
- mapMListType :: forall {k} m wita witb (t :: [k]). Applicative m => (forall (t' :: k). wita t' -> m (witb t')) -> ListType wita t -> m (ListType witb t)
- joinMListType :: forall {k} m wita witb witc (t :: [k]). Applicative m => (forall (t' :: k). wita t' -> witb t' -> m (witc t')) -> ListType wita t -> ListType witb t -> m (ListType witc t)
- mapListType :: forall {k} wita witb (t :: [k]). (forall (t' :: k). wita t' -> witb t') -> ListType wita t -> ListType witb t
- joinListType :: forall {k} wita witb witc (t :: [k]). (forall (t' :: k). wita t' -> witb t' -> witc t') -> ListType wita t -> ListType witb t -> ListType witc t
- pairListType :: forall {k} (wita :: k -> Type) (t :: [k]) (witb :: k -> Type). ListType wita t -> ListType witb t -> ListType (PairType wita witb) t
- listTypeLength :: forall {k} (w :: k -> Type) (lt :: [k]). ListType w lt -> Int
- listTypeToList :: forall {k} w r (t :: [k]). (forall (a :: k). w a -> r) -> ListType w t -> [r]
- listTypeToListM :: forall {k} m w r (t :: [k]). Applicative m => (forall (a :: k). w a -> m r) -> ListType w t -> m [r]
- listTypeFor :: forall {k} m w1 (t :: [k]) w2. Applicative m => ListType w1 t -> (forall (a :: k). w1 a -> m (w2 a)) -> m (ListType w2 t)
- listTypeForList :: forall {k} m w (t :: [k]) r. Applicative m => ListType w t -> (forall (a :: k). w a -> m r) -> m [r]
- listTypeFor_ :: forall {k} m w (t :: [k]). Applicative m => ListType w t -> (forall (a :: k). w a -> m ()) -> m ()
- listTypeLengthType :: forall {k} (w :: k -> Type) (lt :: [k]). ListType w lt -> PeanoNatType (ListLength lt)
- listTypeToFixedList :: forall {k} w r (t :: [k]). (forall (a :: k). w a -> r) -> ListType w t -> FixedList (ListLength t) r
- listTypeFromFixedList :: forall {k} (n :: PeanoNat) (w :: k -> Type) r. FixedList n (Some w) -> (forall (t :: [k]). n ~ ListLength t => ListType w t -> r) -> r
- listTypeFind :: forall {k} w r (tt :: [k]). (forall (a :: k). w a -> Maybe r) -> ListType w tt -> Maybe r
- sequenceComposeListType :: forall {k} f (w :: k -> Type) (lt :: [k]). Applicative f => ListType (Compose f w) lt -> f (ListType w lt)
Documentation
data ListType (w :: k -> Type) (lt :: [k]) where Source #
a witness type for lists of types
The w parameter is the witness type of the elements.
Constructors
| NilListType :: forall {k} (w :: k -> Type). ListType w ('[] :: [k]) | |
| ConsListType :: forall {k} (w :: k -> Type) (a :: k) (lt1 :: [k]). w a -> ListType w lt1 -> ListType w (a ': lt1) |
Instances
| TestEquality w => TestEquality (ListType w :: [k] -> Type) Source # | |
Defined in Data.Type.Witness.Specific.List.List | |
| Representative w => Representative (ListType w :: [k] -> Type) Source # | |
Defined in Data.Type.Witness.Specific.List.List Methods getRepWitness :: Subrepresentative (ListType w) (ListType w) Source # | |
| Representative w => Is (ListType w :: [k] -> Type) ('[] :: [k]) Source # | |
Defined in Data.Type.Witness.Specific.List.List Methods representative :: ListType w ('[] :: [k]) Source # | |
| (Is w a2, Is (ListType w) lt) => Is (ListType w :: [a1] -> Type) (a2 ': lt :: [a1]) Source # | |
Defined in Data.Type.Witness.Specific.List.List Methods representative :: ListType w (a2 ': lt) Source # | |
| (forall (a :: k). Show (w a)) => Show (ListType w lt) Source # | |
mapMListType :: forall {k} m wita witb (t :: [k]). Applicative m => (forall (t' :: k). wita t' -> m (witb t')) -> ListType wita t -> m (ListType witb t) Source #
joinMListType :: forall {k} m wita witb witc (t :: [k]). Applicative m => (forall (t' :: k). wita t' -> witb t' -> m (witc t')) -> ListType wita t -> ListType witb t -> m (ListType witc t) Source #
mapListType :: forall {k} wita witb (t :: [k]). (forall (t' :: k). wita t' -> witb t') -> ListType wita t -> ListType witb t Source #
joinListType :: forall {k} wita witb witc (t :: [k]). (forall (t' :: k). wita t' -> witb t' -> witc t') -> ListType wita t -> ListType witb t -> ListType witc t Source #
pairListType :: forall {k} (wita :: k -> Type) (t :: [k]) (witb :: k -> Type). ListType wita t -> ListType witb t -> ListType (PairType wita witb) t Source #
listTypeToList :: forall {k} w r (t :: [k]). (forall (a :: k). w a -> r) -> ListType w t -> [r] Source #
listTypeToListM :: forall {k} m w r (t :: [k]). Applicative m => (forall (a :: k). w a -> m r) -> ListType w t -> m [r] Source #
listTypeFor :: forall {k} m w1 (t :: [k]) w2. Applicative m => ListType w1 t -> (forall (a :: k). w1 a -> m (w2 a)) -> m (ListType w2 t) Source #
listTypeForList :: forall {k} m w (t :: [k]) r. Applicative m => ListType w t -> (forall (a :: k). w a -> m r) -> m [r] Source #
listTypeFor_ :: forall {k} m w (t :: [k]). Applicative m => ListType w t -> (forall (a :: k). w a -> m ()) -> m () Source #
listTypeLengthType :: forall {k} (w :: k -> Type) (lt :: [k]). ListType w lt -> PeanoNatType (ListLength lt) Source #
listTypeToFixedList :: forall {k} w r (t :: [k]). (forall (a :: k). w a -> r) -> ListType w t -> FixedList (ListLength t) r Source #
listTypeFromFixedList :: forall {k} (n :: PeanoNat) (w :: k -> Type) r. FixedList n (Some w) -> (forall (t :: [k]). n ~ ListLength t => ListType w t -> r) -> r Source #
listTypeFind :: forall {k} w r (tt :: [k]). (forall (a :: k). w a -> Maybe r) -> ListType w tt -> Maybe r Source #
sequenceComposeListType :: forall {k} f (w :: k -> Type) (lt :: [k]). Applicative f => ListType (Compose f w) lt -> f (ListType w lt) Source #