Copyright | (c) Artem Chirkin |
---|---|

License | BSD3 |

Safe Haskell | None |

Language | Haskell2010 |

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 (k :: Type) (f :: k -> Type) (xs :: [k]). () => forall (y :: k) (ys :: [k]). 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 (k :: Type) (xs :: [k]). () => RepresentableList xs => TypeList xs
- pattern EvList :: forall (k :: Type) (c :: k -> Constraint) (xs :: [k]). () => (All c xs, RepresentableList xs) => DictList c xs
- pattern Cons :: forall (k :: Type) (f :: k -> Type) (xs :: [k]). () => forall (y :: k) (ys :: [k]). xs ~ (y ': ys) => f y -> TypedList f ys -> TypedList f xs
- pattern Snoc :: forall (k :: Type) (f :: k -> Type) (xs :: [k]). () => forall (sy :: [k]) (y :: k). xs ~ (sy +: y) => TypedList f sy -> f y -> TypedList f xs
- pattern Reverse :: forall (k :: Type) (f :: k -> Type) (xs :: [k]). () => forall (sx :: [k]). (xs ~ Reverse sx, sx ~ Reverse xs) => TypedList f sx -> TypedList f xs

- class RepresentableList (xs :: [k]) where
- data Dict1 :: (k -> Constraint) -> k -> Type where
- type DictList (c :: k -> Constraint) (xs :: [k]) = TypedList (Dict1 c) xs
- type TypeList (xs :: [k]) = TypedList Proxy xs
- types :: forall (k :: Type) (f :: k -> Type) (xs :: [k]). TypedList f xs -> TypeList xs
- typeables :: forall (k :: Type) (xs :: [k]). Typeable xs => TypeList xs
- inferTypeableList :: forall (k :: Type) (f :: k -> Type) (xs :: [k]). (Typeable k, All Typeable xs) => TypedList f xs -> Dict (Typeable xs)
- order :: forall (k :: Type) (f :: k -> Type) (xs :: [k]). TypedList f xs -> Dim (Length xs)
- order' :: forall (k :: Type) (xs :: [k]). RepresentableList xs => Dim (Length xs)
- cons :: forall (k :: Type) (f :: k -> Type) (x :: k) (xs :: [k]). f x -> TypedList f xs -> TypedList f (x :+ xs)
- snoc :: forall (k :: Type) (f :: k -> Type) (xs :: [k]) (x :: k). TypedList f xs -> f x -> TypedList f (xs +: x)
- reverse :: forall (k :: Type) (f :: k -> Type) (xs :: [k]). TypedList f xs -> TypedList f (Reverse xs)
- take :: forall (k :: Type) (n :: Nat) (f :: k -> Type) (xs :: [k]). Dim n -> TypedList f xs -> TypedList f (Take n xs)
- drop :: forall (k :: Type) (n :: Nat) (f :: k -> Type) (xs :: [k]). Dim n -> TypedList f xs -> TypedList f (Drop n xs)
- head :: forall (k :: Type) (f :: k -> Type) (xs :: [k]). TypedList f xs -> f (Head xs)
- tail :: forall (k :: Type) (f :: k -> Type) (xs :: [k]). TypedList f xs -> TypedList f (Tail xs)
- last :: forall (k :: Type) (f :: k -> Type) (xs :: [k]). TypedList f xs -> f (Last xs)
- init :: forall (k :: Type) (f :: k -> Type) (xs :: [k]). TypedList f xs -> TypedList f (Init xs)
- splitAt :: forall (k :: Type) (n :: Nat) (f :: k -> Type) (xs :: [k]). Dim n -> TypedList f xs -> (TypedList f (Take n xs), TypedList f (Drop n xs))
- stripPrefix :: forall (k :: Type) (f :: k -> Type) (xs :: [k]) (ys :: [k]). (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 (k :: Type) (f :: k -> Type) (xs :: [k]) (ys :: [k]). (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 (k :: Type) (f :: k -> Type) (xs :: [k]) (ys :: [k]). (All Typeable xs, All Typeable ys, All Eq (Map f xs)) => TypedList f xs -> TypedList f ys -> Maybe (xs :~: ys, Bool)
- concat :: forall (k :: Type) (f :: k -> Type) (xs :: [k]) (ys :: [k]). TypedList f xs -> TypedList f ys -> TypedList f (xs ++ ys)
- length :: forall (k :: Type) (f :: k -> Type) (xs :: [k]). TypedList f xs -> Dim (Length xs)
- map :: forall (k :: Type) (f :: k -> Type) (g :: k -> Type) (xs :: [k]). (forall (a :: k). f a -> g a) -> TypedList f xs -> TypedList g xs
- module Data.Type.List
- typedListShowsPrecC :: forall (k :: Type) (c :: k -> Constraint) (f :: k -> Type) (xs :: [k]). All c xs => String -> (forall (x :: k). c x => Int -> f x -> ShowS) -> Int -> TypedList f xs -> ShowS
- typedListShowsPrec :: forall (k :: Type) (f :: k -> Type) (xs :: [k]). (forall (x :: k). Int -> f x -> ShowS) -> Int -> TypedList f xs -> ShowS
- typedListReadPrec :: forall (k :: Type) (c :: k -> Constraint) (f :: k -> Type) (xs :: [k]) (g :: k -> Type). All c xs => String -> (forall (x :: k). c x => ReadPrec (f x)) -> TypedList g xs -> ReadPrec (TypedList f xs)
- withTypedListReadPrec :: forall (k :: Type) (f :: k -> Type) (r :: Type). (forall (z :: Type). (forall (x :: k). f x -> z) -> ReadPrec z) -> (forall (xs :: [k]). TypedList f xs -> r) -> ReadPrec r

# Documentation

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

Type-indexed list

pattern U :: forall (k :: Type) (f :: k -> Type) (xs :: [k]). () => xs ~ '[] => TypedList f xs | Zero-length type list |

pattern (:*) :: forall (k :: Type) (f :: k -> Type) (xs :: [k]). () => forall (y :: k) (ys :: [k]). 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 |

pattern TypeList :: forall (k :: Type) (xs :: [k]). () => RepresentableList xs => TypeList xs | Pattern matching against this causes |

pattern EvList :: forall (k :: Type) (c :: k -> Constraint) (xs :: [k]). () => (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 (k :: Type) (f :: k -> Type) (xs :: [k]). () => forall (y :: k) (ys :: [k]). xs ~ (y ': ys) => f y -> TypedList f ys -> TypedList f xs | Constructing a type-indexed list in the canonical way |

pattern Snoc :: forall (k :: Type) (f :: k -> Type) (xs :: [k]). () => forall (sy :: [k]) (y :: k). xs ~ (sy +: y) => TypedList f sy -> f y -> TypedList f xs | Constructing a type-indexed list from the other end |

pattern Reverse :: forall (k :: Type) (f :: k -> Type) (xs :: [k]). () => forall (sx :: [k]). (xs ~ Reverse sx, sx ~ Reverse xs) => 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 # | |

BoundedDim n => Num (Idxs (n ': ([] :: [k]))) Source # | With this instance we can slightly reduce indexing expressions, e.g. x ! (1 :* 2 :* 4) == x ! (1 :* 2 :* 4 :* U) |

Defined in Numeric.Dimensions.Idx (+) :: Idxs (n ': []) -> Idxs (n ': []) -> Idxs (n ': []) # (-) :: Idxs (n ': []) -> Idxs (n ': []) -> Idxs (n ': []) # (*) :: Idxs (n ': []) -> Idxs (n ': []) -> Idxs (n ': []) # negate :: Idxs (n ': []) -> Idxs (n ': []) # abs :: Idxs (n ': []) -> Idxs (n ': []) # signum :: Idxs (n ': []) -> Idxs (n ': []) # fromInteger :: Integer -> Idxs (n ': []) # | |

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 # | Term-level 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 :: (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 :: [k]) 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 :: (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) (xs :: [k]) = TypedList (Dict1 c) xs Source #

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

types :: forall (k :: Type) (f :: k -> Type) (xs :: [k]). 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 (k :: Type) (xs :: [k]). 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 (k :: Type) (f :: k -> Type) (xs :: [k]). (Typeable k, 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 (k :: Type) (f :: k -> Type) (xs :: [k]). TypedList f xs -> Dim (Length xs) Source #

cons :: forall (k :: Type) (f :: k -> Type) (x :: k) (xs :: [k]). f x -> TypedList f xs -> TypedList f (x :+ xs) Source #

snoc :: forall (k :: Type) (f :: k -> Type) (xs :: [k]) (x :: k). TypedList f xs -> f x -> TypedList f (xs +: x) Source #

reverse :: forall (k :: Type) (f :: k -> Type) (xs :: [k]). TypedList f xs -> TypedList f (Reverse xs) Source #

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

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

tail :: forall (k :: Type) (f :: k -> Type) (xs :: [k]). TypedList f xs -> TypedList f (Tail xs) Source #

init :: forall (k :: Type) (f :: k -> Type) (xs :: [k]). TypedList f xs -> TypedList f (Init xs) Source #

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

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

stripSuffix :: forall (k :: Type) (f :: k -> Type) (xs :: [k]) (ys :: [k]). (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 (k :: Type) (f :: k -> Type) (xs :: [k]) (ys :: [k]). (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 (k :: Type) (f :: k -> Type) (xs :: [k]) (ys :: [k]). TypedList f xs -> TypedList f ys -> TypedList f (xs ++ ys) Source #

length :: forall (k :: Type) (f :: k -> Type) (xs :: [k]). TypedList f xs -> Dim (Length xs) Source #

map :: forall (k :: Type) (f :: k -> Type) (g :: k -> Type) (xs :: [k]). (forall (a :: k). 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 (k :: Type) (c :: k -> Constraint) (f :: k -> Type) (xs :: [k]). All c xs | |

=> String | Override cons symbol |

-> (forall (x :: k). c x => Int -> f x -> ShowS) | How to show a single element |

-> Int | |

-> TypedList f xs | |

-> ShowS |

Generic show function for a `TypedList`

.

:: forall (k :: Type) (f :: k -> Type) (xs :: [k]). (forall (x :: k). Int -> f x -> ShowS) | How to show a single element |

-> Int | |

-> TypedList f xs | |

-> ShowS |

Generic show function for a `TypedList`

.

:: forall (k :: Type) (c :: k -> Constraint) (f :: k -> Type) (xs :: [k]) (g :: k -> Type). All c xs | |

=> String | Override cons symbol |

-> (forall (x :: k). 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 #

:: forall (k :: Type) (f :: k -> Type) (r :: Type). (forall (z :: Type). (forall (x :: k). f x -> z) -> ReadPrec z) | How to read a single element |

-> (forall (xs :: [k]). TypedList f xs -> r) | Consume the result |

-> ReadPrec r |

Generic read function for a `TypedList`

of unknown length.