Copyright	(c) Artem Chirkin
License	BSD3
Safe Haskell	None
Language	Haskell2010

Numeric.TypedList

Contents

Deriving Show and Read

Description

Provide a type-indexed heterogeneous list type TypedList. Behind the facade, TypedList is just a plain list of haskell pointers. It is used to represent dimension lists, indices, and just flexible tuples.

Most of type-level functionality is implemented using GADT-like pattern synonyms. Import this module qualified to use list-like functionality.

Synopsis

data TypedList (f :: k -> Type) (xs :: [k]) where
- pattern U :: forall (k :: Type) (f :: k -> Type) (xs :: [k]). () => xs ~ '[] => TypedList f xs
- pattern (:*) :: forall f xs. () => forall y ys. xs ~ (y ': ys) => f y -> TypedList f ys -> TypedList f xs
- pattern Empty :: forall (k :: Type) (f :: k -> Type) (xs :: [k]). () => xs ~ '[] => TypedList f xs
- pattern TypeList :: forall xs. () => RepresentableList xs => TypeList xs
- pattern EvList :: forall c xs. () => (All c xs, RepresentableList xs) => DictList c xs
- pattern Cons :: forall f xs. () => forall y ys. xs ~ (y ': ys) => f y -> TypedList f ys -> TypedList f xs
- pattern Snoc :: forall f xs. () => forall sy y. SnocList sy y xs => TypedList f sy -> f y -> TypedList f xs
- pattern Reverse :: forall f xs. () => forall sx. ReverseList xs sx => TypedList f sx -> TypedList f xs
class RepresentableList xs where
- tList :: TypeList xs
data Dict1 :: (k -> Constraint) -> k -> Type where
- Dict1 :: c a => Dict1 c a
type DictList (c :: k -> Constraint) = TypedList (Dict1 c) :: [k] -> Type
type TypeList = TypedList Proxy :: [k] -> Type
types :: forall f xs. TypedList f xs -> TypeList xs
typeables :: forall xs. Typeable xs => TypeList xs
inferTypeableList :: forall f xs. (Typeable (KindOfEl xs), All Typeable xs) => TypedList f xs -> Dict (Typeable xs)
order :: forall f xs. TypedList f xs -> Dim (Length xs)
order' :: forall xs. RepresentableList xs => Dim (Length xs)
cons :: forall f x xs. f x -> TypedList f xs -> TypedList f (x :+ xs)
snoc :: forall f xs x. TypedList f xs -> f x -> TypedList f (xs +: x)
reverse :: forall f xs. TypedList f xs -> TypedList f (Reverse xs)
take :: forall (n :: Nat) f xs. Dim n -> TypedList f xs -> TypedList f (Take n xs)
drop :: forall (n :: Nat) f xs. Dim n -> TypedList f xs -> TypedList f (Drop n xs)
head :: forall f xs. TypedList f xs -> f (Head xs)
tail :: forall f xs. TypedList f xs -> TypedList f (Tail xs)
last :: forall f xs. TypedList f xs -> f (Last xs)
init :: forall f xs. TypedList f xs -> TypedList f (Init xs)
splitAt :: forall (n :: Nat) f xs. Dim n -> TypedList f xs -> (TypedList f (Take n xs), TypedList f (Drop n xs))
stripPrefix :: forall f xs ys. (All Typeable xs, All Typeable ys, All Eq (Map f xs)) => TypedList f xs -> TypedList f ys -> Maybe (TypedList f (StripPrefix xs ys))
stripSuffix :: forall f xs ys. (All Typeable xs, All Typeable ys, All Eq (Map f xs)) => TypedList f xs -> TypedList f ys -> Maybe (TypedList f (StripSuffix xs ys))
sameList :: forall f xs ys. (All Typeable xs, All Typeable ys, All Eq (Map f xs)) => TypedList f xs -> TypedList f ys -> Maybe (xs :~: ys, Bool)
concat :: forall f xs ys. TypedList f xs -> TypedList f ys -> TypedList f (xs ++ ys)
length :: forall f xs. TypedList f xs -> Dim (Length xs)
map :: forall f g xs. (forall a. f a -> g a) -> TypedList f xs -> TypedList g xs
module Data.Type.List
typedListShowsPrecC :: forall c f xs. All c xs => String -> (forall x. c x => Int -> f x -> ShowS) -> Int -> TypedList f xs -> ShowS
typedListShowsPrec :: forall f xs. (forall x. Int -> f x -> ShowS) -> Int -> TypedList f xs -> ShowS
typedListReadPrec :: forall c f xs g. All c xs => String -> (forall x. c x => ReadPrec (f x)) -> TypedList g xs -> ReadPrec (TypedList f xs)
withTypedListReadPrec :: forall f (r :: Type). (forall (z :: Type). (forall x. f x -> z) -> ReadPrec z) -> (forall xs. TypedList f xs -> r) -> ReadPrec r

Documentation

data TypedList (f :: k -> Type) (xs :: [k]) where Source #

Type-indexed list

Bundled Patterns

pattern U :: forall (k :: Type) (f :: k -> Type) (xs :: [k]). () => xs ~ '[] => TypedList f xs	Zero-length type list
pattern (:*) :: forall f xs. () => forall y ys. xs ~ (y ': ys) => f y -> TypedList f ys -> TypedList f xs infixr 5	Constructing a type-indexed list
pattern Empty :: forall (k :: Type) (f :: k -> Type) (xs :: [k]). () => xs ~ '[] => TypedList f xs	Zero-length type list; synonym to `U`.
pattern TypeList :: forall xs. () => RepresentableList xs => TypeList xs	Pattern matching against this causes `RepresentableList` instance come into scope. Also it allows constructing a term-level list out of a constraint.
pattern EvList :: forall c xs. () => (All c xs, RepresentableList xs) => DictList c xs	Pattern matching against this allows manipulating lists of constraints. Useful when creating functions that change the shape of dimensions.
pattern Cons :: forall f xs. () => forall y ys. xs ~ (y ': ys) => f y -> TypedList f ys -> TypedList f xs	Constructing a type-indexed list in the canonical way
pattern Snoc :: forall f xs. () => forall sy y. SnocList sy y xs => TypedList f sy -> f y -> TypedList f xs	Constructing a type-indexed list from the other end
pattern Reverse :: forall f xs. () => forall sx. ReverseList xs sx => TypedList f sx -> TypedList f xs	Reverse a typed list

Instances

Instances details

(RepresentableList xs, All Bounded xs) => Bounded (Tuple xs) Source #
Instance details Defined in Numeric.Tuple.Strict Methods minBound :: Tuple xs # maxBound :: Tuple xs #
(RepresentableList xs, All Bounded xs) => Bounded (Tuple xs) Source #
Instance details Defined in Numeric.Tuple.Lazy Methods minBound :: Tuple xs # maxBound :: Tuple xs #
All Eq xs => Eq (Tuple xs) Source #
Instance details Defined in Numeric.Tuple.Strict Methods (==) :: Tuple xs -> Tuple xs -> Bool # (/=) :: Tuple xs -> Tuple xs -> Bool #
All Eq xs => Eq (Tuple xs) Source #
Instance details Defined in Numeric.Tuple.Lazy Methods (==) :: Tuple xs -> Tuple xs -> Bool # (/=) :: Tuple xs -> Tuple xs -> Bool #
(All Eq xs, All Ord xs) => Ord (Tuple xs) Source #	Lexicorgaphic ordering; same as normal Haskell lists.
Instance details Defined in Numeric.Tuple.Strict Methods compare :: Tuple xs -> Tuple xs -> Ordering # (<) :: Tuple xs -> Tuple xs -> Bool # (<=) :: Tuple xs -> Tuple xs -> Bool # (>) :: Tuple xs -> Tuple xs -> Bool # (>=) :: Tuple xs -> Tuple xs -> Bool # max :: Tuple xs -> Tuple xs -> Tuple xs # min :: Tuple xs -> Tuple xs -> Tuple xs #
(All Eq xs, All Ord xs) => Ord (Tuple xs) Source #	Lexicorgaphic ordering; same as normal Haskell lists.
Instance details Defined in Numeric.Tuple.Lazy Methods compare :: Tuple xs -> Tuple xs -> Ordering # (<) :: Tuple xs -> Tuple xs -> Bool # (<=) :: Tuple xs -> Tuple xs -> Bool # (>) :: Tuple xs -> Tuple xs -> Bool # (>=) :: Tuple xs -> Tuple xs -> Bool # max :: Tuple xs -> Tuple xs -> Tuple xs # min :: Tuple xs -> Tuple xs -> Tuple xs #
(All Read xs, RepresentableList xs) => Read (Tuple xs) Source #
Instance details Defined in Numeric.Tuple.Strict Methods readsPrec :: Int -> ReadS (Tuple xs) # readList :: ReadS [Tuple xs] # readPrec :: ReadPrec (Tuple xs) # readListPrec :: ReadPrec [Tuple xs] #
(All Read xs, RepresentableList xs) => Read (Tuple xs) Source #
Instance details Defined in Numeric.Tuple.Lazy Methods readsPrec :: Int -> ReadS (Tuple xs) # readList :: ReadS [Tuple xs] # readPrec :: ReadPrec (Tuple xs) # readListPrec :: ReadPrec [Tuple xs] #
All Show xs => Show (Tuple xs) Source #
Instance details Defined in Numeric.Tuple.Strict Methods showsPrec :: Int -> Tuple xs -> ShowS # show :: Tuple xs -> String # showList :: [Tuple xs] -> ShowS #
All Show xs => Show (Tuple xs) Source #
Instance details Defined in Numeric.Tuple.Lazy Methods showsPrec :: Int -> Tuple xs -> ShowS # show :: Tuple xs -> String # showList :: [Tuple xs] -> ShowS #
All Semigroup xs => Semigroup (Tuple xs) Source #
Instance details Defined in Numeric.Tuple.Strict Methods (<>) :: Tuple xs -> Tuple xs -> Tuple xs # sconcat :: NonEmpty (Tuple xs) -> Tuple xs # stimes :: Integral b => b -> Tuple xs -> Tuple xs #
All Semigroup xs => Semigroup (Tuple xs) Source #
Instance details Defined in Numeric.Tuple.Lazy Methods (<>) :: Tuple xs -> Tuple xs -> Tuple xs # sconcat :: NonEmpty (Tuple xs) -> Tuple xs # stimes :: Integral b => b -> Tuple xs -> Tuple xs #
(RepresentableList xs, All Semigroup xs, All Monoid xs) => Monoid (Tuple xs) Source #
Instance details Defined in Numeric.Tuple.Strict Methods mempty :: Tuple xs # mappend :: Tuple xs -> Tuple xs -> Tuple xs # mconcat :: [Tuple xs] -> Tuple xs #
(RepresentableList xs, All Semigroup xs, All Monoid xs) => Monoid (Tuple xs) Source #
Instance details Defined in Numeric.Tuple.Lazy Methods mempty :: Tuple xs # mappend :: Tuple xs -> Tuple xs -> Tuple xs # mconcat :: [Tuple xs] -> Tuple xs #
BoundedDims ds => Bounded (Idxs ds) Source #
Instance details Defined in Numeric.Dimensions.Idx Methods minBound :: Idxs ds # maxBound :: Idxs ds #
Dimensions ds => Enum (Idxs ds) Source #	`ds` must be fixed (either `[Nat]` or all (N n)) to know exact bounds in each dimension.
Instance details Defined in Numeric.Dimensions.Idx Methods succ :: Idxs ds -> Idxs ds # pred :: Idxs ds -> Idxs ds # toEnum :: Int -> Idxs ds # fromEnum :: Idxs ds -> Int # enumFrom :: Idxs ds -> [Idxs ds] # enumFromThen :: Idxs ds -> Idxs ds -> [Idxs ds] # enumFromTo :: Idxs ds -> Idxs ds -> [Idxs ds] # enumFromThenTo :: Idxs ds -> Idxs ds -> Idxs ds -> [Idxs ds] #
Eq (Dims ds) Source #
Instance details Defined in Numeric.Dimensions.Dim Methods (==) :: Dims ds -> Dims ds -> Bool # (/=) :: Dims ds -> Dims ds -> Bool #
Eq (Dims ds) Source #
Instance details Defined in Numeric.Dimensions.Dim Methods (==) :: Dims ds -> Dims ds -> Bool # (/=) :: Dims ds -> Dims ds -> Bool #
Eq (Idxs xs) Source #
Instance details Defined in Numeric.Dimensions.Idx Methods (==) :: Idxs xs -> Idxs xs -> Bool # (/=) :: Idxs xs -> Idxs xs -> Bool #
Ord (Dims ds) Source #
Instance details Defined in Numeric.Dimensions.Dim Methods compare :: Dims ds -> Dims ds -> Ordering # (<) :: Dims ds -> Dims ds -> Bool # (<=) :: Dims ds -> Dims ds -> Bool # (>) :: Dims ds -> Dims ds -> Bool # (>=) :: Dims ds -> Dims ds -> Bool # max :: Dims ds -> Dims ds -> Dims ds # min :: Dims ds -> Dims ds -> Dims ds #
Ord (Dims ds) Source #
Instance details Defined in Numeric.Dimensions.Dim Methods compare :: Dims ds -> Dims ds -> Ordering # (<) :: Dims ds -> Dims ds -> Bool # (<=) :: Dims ds -> Dims ds -> Bool # (>) :: Dims ds -> Dims ds -> Bool # (>=) :: Dims ds -> Dims ds -> Bool # max :: Dims ds -> Dims ds -> Dims ds # min :: Dims ds -> Dims ds -> Dims ds #
Ord (Idxs xs) Source #	Compare indices by their importance in lexicorgaphic order from the first dimension to the last dimension (the first dimension is the most significant one). Literally, compare a b = compare (listIdxs a) (listIdxs b) This is the same `compare` rule, as for `Dims`. This is also consistent with offsets: sort == sortOn fromEnum
Instance details Defined in Numeric.Dimensions.Idx Methods compare :: Idxs xs -> Idxs xs -> Ordering # (<) :: Idxs xs -> Idxs xs -> Bool # (<=) :: Idxs xs -> Idxs xs -> Bool # (>) :: Idxs xs -> Idxs xs -> Bool # (>=) :: Idxs xs -> Idxs xs -> Bool # max :: Idxs xs -> Idxs xs -> Idxs xs # min :: Idxs xs -> Idxs xs -> Idxs xs #
BoundedDims xs => Read (Dims xs) Source #
Instance details Defined in Numeric.Dimensions.Dim Methods readsPrec :: Int -> ReadS (Dims xs) # readList :: ReadS [Dims xs] # readPrec :: ReadPrec (Dims xs) # readListPrec :: ReadPrec [Dims xs] #
BoundedDims xs => Read (Idxs xs) Source #
Instance details Defined in Numeric.Dimensions.Idx Methods readsPrec :: Int -> ReadS (Idxs xs) # readList :: ReadS [Idxs xs] # readPrec :: ReadPrec (Idxs xs) # readListPrec :: ReadPrec [Idxs xs] #
Show (Dims xs) Source #
Instance details Defined in Numeric.Dimensions.Dim Methods showsPrec :: Int -> Dims xs -> ShowS # show :: Dims xs -> String # showList :: [Dims xs] -> ShowS #
Show (Idxs xs) Source #
Instance details Defined in Numeric.Dimensions.Idx Methods showsPrec :: Int -> Idxs xs -> ShowS # show :: Idxs xs -> String # showList :: [Idxs xs] -> ShowS #
(Typeable k, Typeable f, Typeable xs, All Data (Map f xs)) => Data (TypedList f xs) Source #	Term-level structure of a `TypedList f xs` is fully determined by its type `Typeable xs`. Thus, `gunfold` does not use its last argument (`Constr`) at all, relying on the structure of the type parameter.
Instance details Defined in Numeric.TypedList Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> TypedList f xs -> c (TypedList f xs) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (TypedList f xs) # toConstr :: TypedList f xs -> Constr # dataTypeOf :: TypedList f xs -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (TypedList f xs)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (TypedList f xs)) # gmapT :: (forall b. Data b => b -> b) -> TypedList f xs -> TypedList f xs # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> TypedList f xs -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> TypedList f xs -> r # gmapQ :: (forall d. Data d => d -> u) -> TypedList f xs -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> TypedList f xs -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> TypedList f xs -> m (TypedList f xs) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> TypedList f xs -> m (TypedList f xs) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> TypedList f xs -> m (TypedList f xs) #
Generic (TypedList f xs) Source #
Instance details Defined in Numeric.TypedList Associated Types type Rep (TypedList f xs) :: Type -> Type # Methods from :: TypedList f xs -> Rep (TypedList f xs) x # to :: Rep (TypedList f xs) x -> TypedList f xs #
type Rep (TypedList f xs) Source #
Instance details Defined in Numeric.TypedList type Rep (TypedList f xs)

class RepresentableList xs where Source #

Representable type lists. Allows getting type information about list structure at runtime.

Methods

tList :: TypeList xs Source #

Get type-level constructed list

Instances

Instances details

RepresentableList ('[] :: [k]) Source #
Instance details Defined in Numeric.TypedList Methods tList :: TypeList '[] Source #
RepresentableList xs => RepresentableList (x ': xs :: [k]) Source #
Instance details Defined in Numeric.TypedList Methods tList :: TypeList (x ': xs) Source #

data Dict1 :: (k -> Constraint) -> k -> Type where Source #

Same as Dict, but allows to separate constraint function from the type it is applied to.

Constructors

Dict1 :: c a => Dict1 c a

Instances

Instances details

Eq (Dict1 p a) Source #
Instance details Defined in Numeric.TypedList Methods (==) :: Dict1 p a -> Dict1 p a -> Bool # (/=) :: Dict1 p a -> Dict1 p a -> Bool #
(Typeable k, Typeable p, Typeable a, p a) => Data (Dict1 p a) Source #
Instance details Defined in Numeric.TypedList Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Dict1 p a -> c (Dict1 p a) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Dict1 p a) # toConstr :: Dict1 p a -> Constr # dataTypeOf :: Dict1 p a -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Dict1 p a)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Dict1 p a)) # gmapT :: (forall b. Data b => b -> b) -> Dict1 p a -> Dict1 p a # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Dict1 p a -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Dict1 p a -> r # gmapQ :: (forall d. Data d => d -> u) -> Dict1 p a -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> Dict1 p a -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> Dict1 p a -> m (Dict1 p a) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Dict1 p a -> m (Dict1 p a) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Dict1 p a -> m (Dict1 p a) #
Ord (Dict1 p a) Source #
Instance details Defined in Numeric.TypedList Methods compare :: Dict1 p a -> Dict1 p a -> Ordering # (<) :: Dict1 p a -> Dict1 p a -> Bool # (<=) :: Dict1 p a -> Dict1 p a -> Bool # (>) :: Dict1 p a -> Dict1 p a -> Bool # (>=) :: Dict1 p a -> Dict1 p a -> Bool # max :: Dict1 p a -> Dict1 p a -> Dict1 p a # min :: Dict1 p a -> Dict1 p a -> Dict1 p a #
Show (Dict1 p a) Source #
Instance details Defined in Numeric.TypedList Methods showsPrec :: Int -> Dict1 p a -> ShowS # show :: Dict1 p a -> String # showList :: [Dict1 p a] -> ShowS #

type DictList (c :: k -> Constraint) = TypedList (Dict1 c) :: [k] -> Type Source #

A list of dicts for the same constraint over several types.

type TypeList = TypedList Proxy :: [k] -> Type Source #

A list of type proxies

types :: forall f xs. TypedList f xs -> TypeList xs Source #

Get a constructible TypeList from any other TypedList; Pattern matching agains the result brings RepresentableList constraint into the scope:

case types ts of TypeList -> ...

typeables :: forall xs. Typeable xs => TypeList xs Source #

Construct a TypeList xs if there is an instance of Typeable xs around.

This way, you can always bring RepresentableList instance into the scope if you have a Typeable instance.

inferTypeableList :: forall f xs. (Typeable (KindOfEl xs), All Typeable xs) => TypedList f xs -> Dict (Typeable xs) Source #

If all elements of a TypedList are Typeable, then the list of these elements is also Typeable.

order :: forall f xs. TypedList f xs -> Dim (Length xs) Source #

Return the number of elements in a TypedList (same as length).

order' :: forall xs. RepresentableList xs => Dim (Length xs) Source #

Return the number of elements in a type list xs bound by a constraint RepresentableList xs (same as order, but takes no value arguments).

cons :: forall f x xs. f x -> TypedList f xs -> TypedList f (x :+ xs) Source #

O(1) append an element in front of a TypedList (same as (:) for lists).

snoc :: forall f xs x. TypedList f xs -> f x -> TypedList f (xs +: x) Source #

O(n) append an element to the end of a TypedList.

reverse :: forall f xs. TypedList f xs -> TypedList f (Reverse xs) Source #

O(n) return elements of a TypedList in reverse order.

take :: forall (n :: Nat) f xs. Dim n -> TypedList f xs -> TypedList f (Take n xs) Source #

O(min(n,k)) take k xs returns a prefix of xs of length min(length xs, k). It calls take under the hood, so expect the same behavior.

drop :: forall (n :: Nat) f xs. Dim n -> TypedList f xs -> TypedList f (Drop n xs) Source #

O(min(n,k)) drop k xs returns a suffix of xs of length max(0, length xs - k). It calls drop under the hood, so expect the same behavior.

head :: forall f xs. TypedList f xs -> f (Head xs) Source #

O(1) Extract the first element of a TypedList, which must be non-empty.

tail :: forall f xs. TypedList f xs -> TypedList f (Tail xs) Source #

O(1) Extract the elements after the head of a TypedList, which must be non-empty.

last :: forall f xs. TypedList f xs -> f (Last xs) Source #

O(n) Extract the last element of a TypedList, which must be non-empty.

init :: forall f xs. TypedList f xs -> TypedList f (Init xs) Source #

O(n) Return all the elements of a TypedList except the last one (the list must be non-empty).

splitAt :: forall (n :: Nat) f xs. Dim n -> TypedList f xs -> (TypedList f (Take n xs), TypedList f (Drop n xs)) Source #

O(min(n,k)) splitAt k xs has the same effect as (take k xs, drop k xs). It calls splitAt under the hood, so expect the same behavior.

stripPrefix :: forall f xs ys. (All Typeable xs, All Typeable ys, All Eq (Map f xs)) => TypedList f xs -> TypedList f ys -> Maybe (TypedList f (StripPrefix xs ys)) Source #

Drops the given prefix from a TypedList. It returns Nothing if the TypedList does not start with the prefix given, or Just the TypedList after the prefix, if it does. It calls stripPrefix under the hood, so expect the same behavior.

This function can be used to find the type-level evidence that one type-level list is indeed a prefix of another.

stripSuffix :: forall f xs ys. (All Typeable xs, All Typeable ys, All Eq (Map f xs)) => TypedList f xs -> TypedList f ys -> Maybe (TypedList f (StripSuffix xs ys)) Source #

Drops the given suffix from a TypedList. It returns Nothing if the TypedList does not end with the suffix given, or Just the TypedList before the suffix, if it does.

This function can be used to find the type-level evidence that one type-level list is indeed a suffix of another.

sameList :: forall f xs ys. (All Typeable xs, All Typeable ys, All Eq (Map f xs)) => TypedList f xs -> TypedList f ys -> Maybe (xs :~: ys, Bool) Source #

Returns two things at once: (Evidence that types of lists match, value-level equality).

concat :: forall f xs ys. TypedList f xs -> TypedList f ys -> TypedList f (xs ++ ys) Source #

Concat two TypedLists. It calls `Prelude.(++)` under the hood, so expect the same behavior.

length :: forall f xs. TypedList f xs -> Dim (Length xs) Source #

Return the number of elements in a TypedList (same as order).

map :: forall f g xs. (forall a. f a -> g a) -> TypedList f xs -> TypedList g xs Source #

Map a function over contents of a typed list

module Data.Type.List

Deriving Show and Read

typedListShowsPrecC Source #

Arguments

:: forall c f xs. All c xs
=> String	Override cons symbol
-> (forall x. c x => Int -> f x -> ShowS)	How to show a single element
-> Int
-> TypedList f xs
-> ShowS

Generic show function for a TypedList.

typedListShowsPrec Source #

Arguments

:: forall f xs. (forall x. Int -> f x -> ShowS)	How to show a single element
-> Int
-> TypedList f xs
-> ShowS

Generic show function for a TypedList.

typedListReadPrec Source #

Arguments

:: forall c f xs g. All c xs
=> String	Override cons symbol
-> (forall x. c x => ReadPrec (f x))	How to read a single element
-> TypedList g xs	Enforce the type structure of the result
-> ReadPrec (TypedList f xs)

Generic read function for a TypedList. Requires a "template" to enforce the structure of the type list.

withTypedListReadPrec Source #

Arguments

:: forall f (r :: Type). (forall (z :: Type). (forall x. f x -> z) -> ReadPrec z)	How to read a single element
-> (forall xs. TypedList f xs -> r)	Consume the result
-> ReadPrec r

Generic read function for a TypedList of unknown length.