dimensions-2.1.1.0: Safe type-level dimensionality for multidimensional data.
Copyright(c) Artem Chirkin
LicenseBSD3
Safe HaskellNone
LanguageHaskell2010

Numeric.TypedList

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

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

(All Read xs, RepresentableList xs) => Read (Tuple xs) Source # 
Instance details

Defined in Numeric.Tuple.Lazy

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

BoundedDims xs => Read (Idxs xs) Source # 
Instance details

Defined in Numeric.Dimensions.Idx

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

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.