Data.Type.Witness.Specific.List.List

Documentation

data ListType w lt where

a witness type for lists of types 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 :: [k] -> Type)

Defined in Data.Type.Witness.Specific.List.List

Methods

testEquality :: forall (a :: k0) (b :: k0). ListType w a -> ListType w b -> Maybe (a :~: b)

Representative w => Representative (ListType w :: [k] -> Type)

Defined in Data.Type.Witness.Specific.List.List

Methods

getRepWitness :: Subrepresentative (ListType w) (ListType w)

Representative w => Is (ListType w :: [k] -> Type) ('[] :: [k])

Defined in Data.Type.Witness.Specific.List.List

Methods

representative :: ListType w '[]

(Is w a2, Is (ListType w) lt) => Is (ListType w :: [a1] -> Type) (a2 ': lt :: [a1])

Defined in Data.Type.Witness.Specific.List.List

Methods

representative :: ListType w (a2 ': lt)

(forall (a :: k). Show (w a)) => Show (ListType w lt)

Defined in Data.Type.Witness.Specific.List.List

Methods

showsPrec :: Int -> ListType w lt -> ShowS

show :: ListType w lt -> String

showList :: [ListType w lt] -> ShowS

assembleListType :: [Some w] -> Some (ListType w)

mapMListType :: Applicative m => (forall t'. wita t' -> m (witb t')) -> ListType wita t -> m (ListType witb t)

joinMListType :: Applicative m => (forall t'. wita t' -> witb t' -> m (witc t')) -> ListType wita t -> ListType witb t -> m (ListType witc t)

mapListType :: (forall t'. wita t' -> witb t') -> ListType wita t -> ListType witb t

joinListType :: (forall t'. wita t' -> witb t' -> witc t') -> ListType wita t -> ListType witb t -> ListType witc t

pairListType :: ListType wita t -> ListType witb t -> ListType (PairType wita witb) t

listTypeLength :: ListType w lt -> Int

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

listTypeFor :: Applicative m => ListType w t -> (forall a. w a -> m r) -> m [r]

listTypeFor_ :: Applicative m => ListType w t -> (forall a. w a -> m ()) -> m ()

listTypeLengthType :: ListType w lt -> PeanoNatType (ListLength lt)

listTypeToFixedList :: (forall a. w a -> r) -> ListType w t -> FixedList (ListLength t) r

listTypeFromFixedList :: FixedList n (Some w) -> (forall t. n ~ ListLength t => ListType w t -> r) -> r