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

License | BSD3 |

Maintainer | chirkin@arch.ethz.ch |

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 (f :: k -> Type) (xs :: [k]). () => xs ~ '[] => TypedList f xs
- pattern (:*) :: forall (f :: k -> Type) (xs :: [k]). () => forall (y :: k) (ys :: [k]). xs ~ (y ': ys) => f y -> TypedList f ys -> TypedList f xs
- pattern Empty :: forall (f :: k -> Type) (xs :: [k]). () => xs ~ '[] => TypedList f xs
- pattern TypeList :: forall (xs :: [k]). () => RepresentableList xs => TypeList xs
- pattern EvList :: forall (c :: k -> Constraint) (xs :: [k]). () => (All c xs, RepresentableList xs) => EvidenceList c xs
- pattern Cons :: forall (f :: k -> Type) (xs :: [k]). () => forall (y :: k) (ys :: [k]). xs ~ (y ': ys) => f y -> TypedList f ys -> TypedList f xs
- pattern Snoc :: forall (f :: k -> Type) (xs :: [k]). () => forall (sy :: [k]) (y :: k). xs ~ (sy +: y) => TypedList f sy -> f y -> TypedList f xs
- pattern Reverse :: forall (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
- type TypeList (xs :: [k]) = TypedList Proxy xs
- types :: TypedList f xs -> TypeList xs
- order :: TypedList f xs -> Dim (Length xs)
- order' :: forall xs. RepresentableList xs => Dim (Length xs)
- cons :: f x -> TypedList f xs -> TypedList f (x :+ xs)
- snoc :: TypedList f xs -> f x -> TypedList f (xs +: x)
- reverse :: TypedList f xs -> TypedList f (Reverse xs)
- take :: Dim n -> TypedList f xs -> TypedList f (Take n xs)
- drop :: Dim n -> TypedList f xs -> TypedList f (Drop n xs)
- head :: TypedList f xs -> f (Head xs)
- tail :: TypedList f xs -> TypedList f (Tail xs)
- last :: TypedList f xs -> f (Last xs)
- init :: TypedList f xs -> TypedList f (Init xs)
- splitAt :: Dim n -> TypedList f xs -> (TypedList f (Take n xs), TypedList f (Drop n xs))
- concat :: TypedList f xs -> TypedList f ys -> TypedList f (xs ++ ys)
- length :: TypedList f xs -> Dim (Length xs)
- map :: (forall a. f a -> g a) -> TypedList f xs -> TypedList g xs
- module Numeric.Type.List

# Documentation

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

Type-indexed list

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

pattern (:*) :: forall (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 (f :: k -> Type) (xs :: [k]). () => xs ~ '[] => TypedList f xs | Zero-length type list; synonym to |

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

pattern EvList :: forall (c :: k -> Constraint) (xs :: [k]). () => (All c xs, RepresentableList xs) => EvidenceList 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 :: 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 (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 (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) # | |

(RepresentableList xs, All Bounded xs) => Bounded (Tuple xs) # | |

All Eq xs => Eq (Tuple xs) # | |

All Eq xs => Eq (Tuple xs) # | |

(All Eq xs, All Ord xs) => Ord (Tuple xs) # | Ord instance of the Tuple implements inverse lexicorgaphic ordering. That is, the last element in the tuple is the most significant one. Note, this will never work on infinite-dimensional tuples! |

Defined in Numeric.Tuple.Strict | |

(All Eq xs, All Ord xs) => Ord (Tuple xs) # | Ord instance of the Tuple implements inverse lexicorgaphic ordering. That is, the last element in the tuple is the most significant one. Note, this will never work on infinite-dimensional tuples! |

Defined in Numeric.Tuple.Lazy | |

(RepresentableList xs, All Read xs) => Read (Tuple xs) # | |

(RepresentableList xs, All Read xs) => Read (Tuple xs) # | |

All Show xs => Show (Tuple xs) # | |

All Show xs => Show (Tuple xs) # | |

All Semigroup xs => Semigroup (Tuple xs) # | |

All Semigroup xs => Semigroup (Tuple xs) # | |

(Semigroup (Tuple xs), RepresentableList xs, All Monoid xs) => Monoid (Tuple xs) # | |

(Semigroup (Tuple xs), RepresentableList xs, All Monoid xs) => Monoid (Tuple xs) # | |

Dimensions ds => Bounded (Dims ds) # | |

Dimensions ds => Bounded (Idxs ds) # | |

Dimensions ds => Enum (Idxs ds) # | |

Eq (Dims ds) # | |

Eq (Dims ds) # | |

Eq (Idxs xs) # | |

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

Defined in Numeric.Dimensions.Idxs (+) :: 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) # | |

Ord (Dims ds) # | |

Ord (Idxs xs) # | Compare indices by their importance in lexicorgaphic order
from the last dimension to the first dimension
(the last dimension is the most significant one) Literally, compare a b = compare (reverse $ listIdxs a) (reverse $ listIdxs b) This is the same sort == sortOn fromEnum |

Show (Dims xs) # | |

Show (Idxs xs) # | |

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 |

types :: 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 -> ...

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

Map a function over contents of a typed list

module Numeric.Type.List