Numeric.TypedList

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.

Documentation

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

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 (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 U.

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

Defined in Numeric.Tuple.Strict

Methods

minBound :: Tuple xs

maxBound :: Tuple xs

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

Defined in Numeric.Tuple.Lazy

Methods

minBound :: Tuple xs

maxBound :: Tuple xs

All Eq xs => Eq (Tuple xs)

Defined in Numeric.Tuple.Strict

Methods

(==) :: Tuple xs -> Tuple xs -> Bool

(/=) :: Tuple xs -> Tuple xs -> Bool

All Eq xs => Eq (Tuple xs)

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)

Lexicorgaphic ordering; same as normal Haskell lists.

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)

Lexicorgaphic ordering; same as normal Haskell lists.

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)

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)

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)

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)

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)

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)

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)

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)

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)

Defined in Numeric.Dimensions.Idx

Methods

minBound :: Idxs ds

maxBound :: Idxs ds

Dimensions ds => Enum (Idxs ds)

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)

Defined in Numeric.Dimensions.Dim

Methods

(==) :: Dims ds -> Dims ds -> Bool

(/=) :: Dims ds -> Dims ds -> Bool

Eq (Dims ds)

Defined in Numeric.Dimensions.Dim

Methods

(==) :: Dims ds -> Dims ds -> Bool

(/=) :: Dims ds -> Dims ds -> Bool

Eq (Idxs xs)

Defined in Numeric.Dimensions.Idx

Methods

(==) :: Idxs xs -> Idxs xs -> Bool

(/=) :: Idxs xs -> Idxs xs -> Bool

BoundedDim 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.Idx

Methods

(+) :: 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)

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)

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)

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

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)

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)

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)

Defined in Numeric.Dimensions.Dim

Methods

showsPrec :: Int -> Dims xs -> ShowS

show :: Dims xs -> String

showList :: [Dims xs] -> ShowS

Show (Idxs xs)

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)

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.

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 :: (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)

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)

Defined in Numeric.TypedList

type Rep (TypedList f xs)

class RepresentableList (xs :: [k]) where

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

Methods

tList :: TypeList xs

Get type-level constructed list

Instances

RepresentableList ([] :: [k])

Defined in Numeric.TypedList

Methods

tList :: TypeList []

RepresentableList xs => RepresentableList (x ': xs :: [k])

Defined in Numeric.TypedList

Methods

tList :: TypeList (x ': xs)

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

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

Constructors

Dict1 :: c a => Dict1 c a

Instances

Eq (Dict1 p a)

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)

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 :: (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)

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)

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

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

type TypeList (xs :: [k]) = TypedList Proxy xs

A list of type proxies

types :: forall (k :: Type) (f :: k -> Type) (xs :: [k]). TypedList f xs -> TypeList xs

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

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)

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)

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)

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)

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

Map a function over contents of a typed list

module Data.Type.List

Deriving Show and Read

typedListShowsPrecC

Arguments

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

typedListShowsPrec

Arguments

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

typedListReadPrec

Arguments

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

Arguments

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