Copyright  (c) Artem Chirkin 

License  BSD3 
Safe Haskell  None 
Language  Haskell2010 
Provide a typeindexed 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 typelevel functionality is implemented using GADTlike pattern synonyms. Import this module qualified to use listlike 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
 data Dict1 :: (k > Constraint) > k > Type where
 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 #
Typeindexed list
pattern U :: forall (k :: Type) (f :: k > Type) (xs :: [k]). () => xs ~ '[] => TypedList f xs  Zerolength type list 
pattern (:*) :: forall f xs. () => forall y ys. xs ~ (y ': ys) => f y > TypedList f ys > TypedList f xs infixr 5  Constructing a typeindexed list 
pattern Empty :: forall (k :: Type) (f :: k > Type) (xs :: [k]). () => xs ~ '[] => TypedList f xs  Zerolength type list; synonym to 
pattern TypeList :: forall xs. () => RepresentableList xs => TypeList xs  Pattern matching against this causes 
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 typeindexed 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 typeindexed 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
(RepresentableList xs, All Bounded xs) => Bounded (Tuple xs) Source #  
(RepresentableList xs, All Bounded xs) => Bounded (Tuple xs) Source #  
All Eq xs => Eq (Tuple xs) Source #  
All Eq xs => Eq (Tuple xs) Source #  
(All Eq xs, All Ord xs) => Ord (Tuple xs) Source #  Lexicorgaphic ordering; same as normal Haskell lists. 
Defined in Numeric.Tuple.Strict  
(All Eq xs, All Ord xs) => Ord (Tuple xs) Source #  Lexicorgaphic ordering; same as normal Haskell lists. 
Defined in Numeric.Tuple.Lazy  
(All Read xs, RepresentableList xs) => Read (Tuple xs) Source #  
(All Read xs, RepresentableList xs) => Read (Tuple xs) Source #  
All Show xs => Show (Tuple xs) Source #  
All Show xs => Show (Tuple xs) Source #  
All Semigroup xs => Semigroup (Tuple xs) Source #  
All Semigroup xs => Semigroup (Tuple xs) Source #  
(RepresentableList xs, All Semigroup xs, All Monoid xs) => Monoid (Tuple xs) Source #  
(RepresentableList xs, All Semigroup xs, All Monoid xs) => Monoid (Tuple xs) Source #  
BoundedDims ds => Bounded (Idxs ds) Source #  
Dimensions ds => Enum (Idxs ds) Source # 

Eq (Dims ds) Source #  
Eq (Dims ds) Source #  
Eq (Idxs xs) Source #  
Ord (Dims ds) Source #  
Ord (Dims ds) Source #  
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 sort == sortOn fromEnum 
BoundedDims xs => Read (Dims xs) Source #  
BoundedDims xs => Read (Idxs xs) Source #  
Show (Dims xs) Source #  
Show (Idxs xs) Source #  
(Typeable k, Typeable f, Typeable xs, All Data (Map f xs)) => Data (TypedList f xs) Source #  Termlevel structure of a 
Defined in Numeric.TypedList 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 #  
type Rep (TypedList f xs) Source #  
Defined in Numeric.TypedList 
class RepresentableList xs where Source #
Representable type lists. Allows getting type information about list structure at runtime.
Instances
RepresentableList ('[] :: [k]) Source #  
Defined in Numeric.TypedList  
RepresentableList xs => RepresentableList (x ': xs :: [k]) Source #  
Defined in Numeric.TypedList 
data Dict1 :: (k > Constraint) > k > Type where Source #
Same as Dict
, but allows to separate constraint function from
the type it is applied to.
Instances
Eq (Dict1 p a) Source #  
(Typeable k, Typeable p, Typeable a, p a) => Data (Dict1 p a) Source #  
Defined in Numeric.TypedList 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 #  
Defined in Numeric.TypedList  
Show (Dict1 p a) Source #  
type DictList (c :: k > Constraint) = TypedList (Dict1 c) :: [k] > Type Source #
A list of dicts for the same constraint over several types.
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 nonempty.
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 nonempty.
last :: forall f xs. TypedList f xs > f (Last xs) Source #
O(n) Extract the last element of a TypedList
, which must be nonempty.
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 nonempty).
splitAt :: forall (n :: Nat) f xs. Dim n > TypedList f xs > (TypedList f (Take n xs), TypedList f (Drop n xs)) Source #
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 typelevel evidence that one typelevel 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 #
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, valuelevel equality).
concat :: forall f xs ys. TypedList f xs > TypedList f ys > TypedList f (xs ++ ys) Source #
Concat two TypedList
s.
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
:: 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
.
:: 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
.
:: 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.