dimensions-2.0.0.0: Safe type-level dimensionality for multidimensional data.

Copyright(c) Artem Chirkin
LicenseBSD3
Safe HaskellNone
LanguageHaskell2010

Numeric.Dimensions

Description

Provides a set of data types to define and traverse through multiple dimensions. The core types are `Dims ds` and `Idxs ds`, which fix dimension sizes at compile time.

Higher indices go first, i.e. assumed enumeration is i = i1*n1*n2*...*n(k-1) + ... + i(k-2)*n1*n2 + i(k-1)*n1 + ik This corresponds to row-first layout of matrices and multidimenional arrays.

Synopsis

Documentation

mapDict :: (a :- b) -> Dict a -> Dict b #

Apply an entailment to a dictionary.

From a category theoretic perspective Dict is a functor that maps from the category of constraints (with arrows in :-) to the category Hask of Haskell data types.

(\\) :: HasDict c e => (c -> r) -> e -> r infixl 1 #

Operator version of withDict, with the arguments flipped

data Dict a where #

Values of type Dict p capture a dictionary for a constraint of type p.

e.g.

Dict :: Dict (Eq Int)

captures a dictionary that proves we have an:

instance Eq 'Int

Pattern matching on the Dict constructor will bring this instance into scope.

Constructors

Dict :: forall a. a => Dict a 
Instances
HasDict a (Dict a) 
Instance details

Defined in Data.Constraint

Methods

evidence :: Dict a -> Dict a #

a :=> (Read (Dict a)) 
Instance details

Defined in Data.Constraint

Methods

ins :: a :- Read (Dict a) #

a :=> (Monoid (Dict a)) 
Instance details

Defined in Data.Constraint

Methods

ins :: a :- Monoid (Dict a) #

a :=> (Enum (Dict a)) 
Instance details

Defined in Data.Constraint

Methods

ins :: a :- Enum (Dict a) #

a :=> (Bounded (Dict a)) 
Instance details

Defined in Data.Constraint

Methods

ins :: a :- Bounded (Dict a) #

() :=> (Eq (Dict a)) 
Instance details

Defined in Data.Constraint

Methods

ins :: () :- Eq (Dict a) #

() :=> (Ord (Dict a)) 
Instance details

Defined in Data.Constraint

Methods

ins :: () :- Ord (Dict a) #

() :=> (Show (Dict a)) 
Instance details

Defined in Data.Constraint

Methods

ins :: () :- Show (Dict a) #

() :=> (Semigroup (Dict a)) 
Instance details

Defined in Data.Constraint

Methods

ins :: () :- Semigroup (Dict a) #

a => Bounded (Dict a) 
Instance details

Defined in Data.Constraint

Methods

minBound :: Dict a #

maxBound :: Dict a #

a => Enum (Dict a) 
Instance details

Defined in Data.Constraint

Methods

succ :: Dict a -> Dict a #

pred :: Dict a -> Dict a #

toEnum :: Int -> Dict a #

fromEnum :: Dict a -> Int #

enumFrom :: Dict a -> [Dict a] #

enumFromThen :: Dict a -> Dict a -> [Dict a] #

enumFromTo :: Dict a -> Dict a -> [Dict a] #

enumFromThenTo :: Dict a -> Dict a -> Dict a -> [Dict a] #

Eq (Dict a) 
Instance details

Defined in Data.Constraint

Methods

(==) :: Dict a -> Dict a -> Bool #

(/=) :: Dict a -> Dict a -> Bool #

(Typeable p, p) => Data (Dict p) 
Instance details

Defined in Data.Constraint

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Dict p -> c (Dict p) #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Dict p) #

toConstr :: Dict p -> Constr #

dataTypeOf :: Dict p -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Dict p)) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Dict p)) #

gmapT :: (forall b. Data b => b -> b) -> Dict p -> Dict p #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Dict p -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Dict p -> r #

gmapQ :: (forall d. Data d => d -> u) -> Dict p -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Dict p -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Dict p -> m (Dict p) #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Dict p -> m (Dict p) #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Dict p -> m (Dict p) #

Ord (Dict a) 
Instance details

Defined in Data.Constraint

Methods

compare :: Dict a -> Dict a -> Ordering #

(<) :: Dict a -> Dict a -> Bool #

(<=) :: Dict a -> Dict a -> Bool #

(>) :: Dict a -> Dict a -> Bool #

(>=) :: Dict a -> Dict a -> Bool #

max :: Dict a -> Dict a -> Dict a #

min :: Dict a -> Dict a -> Dict a #

a => Read (Dict a) 
Instance details

Defined in Data.Constraint

Show (Dict a) 
Instance details

Defined in Data.Constraint

Methods

showsPrec :: Int -> Dict a -> ShowS #

show :: Dict a -> String #

showList :: [Dict a] -> ShowS #

Semigroup (Dict a) 
Instance details

Defined in Data.Constraint

Methods

(<>) :: Dict a -> Dict a -> Dict a #

sconcat :: NonEmpty (Dict a) -> Dict a #

stimes :: Integral b => b -> Dict a -> Dict a #

a => Monoid (Dict a) 
Instance details

Defined in Data.Constraint

Methods

mempty :: Dict a #

mappend :: Dict a -> Dict a -> Dict a #

mconcat :: [Dict a] -> Dict a #

newtype a :- b infixr 9 #

This is the type of entailment.

a :- b is read as a "entails" b.

With this we can actually build a category for Constraint resolution.

e.g.

Because Eq a is a superclass of Ord a, we can show that Ord a entails Eq a.

Because instance Ord a => Ord [a] exists, we can show that Ord a entails Ord [a] as well.

This relationship is captured in the :- entailment type here.

Since p :- p and entailment composes, :- forms the arrows of a Category of constraints. However, Category only became sufficiently general to support this instance in GHC 7.8, so prior to 7.8 this instance is unavailable.

But due to the coherence of instance resolution in Haskell, this Category has some very interesting properties. Notably, in the absence of IncoherentInstances, this category is "thin", which is to say that between any two objects (constraints) there is at most one distinguishable arrow.

This means that for instance, even though there are two ways to derive Ord a :- Eq [a], the answers from these two paths _must_ by construction be equal. This is a property that Haskell offers that is pretty much unique in the space of languages with things they call "type classes".

What are the two ways?

Well, we can go from Ord a :- Eq a via the superclass relationship, and then from Eq a :- Eq [a] via the instance, or we can go from Ord a :- Ord [a] via the instance then from Ord [a] :- Eq [a] through the superclass relationship and this diagram by definition must "commute".

Diagrammatically,

                   Ord a
               ins /     \ cls
                  v       v
            Ord [a]     Eq a
               cls \     / ins
                    v   v
                   Eq [a]

This safety net ensures that pretty much anything you can write with this library is sensible and can't break any assumptions on the behalf of library authors.

Constructors

Sub (a -> Dict b) 
Instances
Category (:-)

Possible since GHC 7.8, when Category was made polykinded.

Instance details

Defined in Data.Constraint

Methods

id :: a :- a #

(.) :: (b :- c) -> (a :- b) -> a :- c #

() :=> (Eq (a :- b)) 
Instance details

Defined in Data.Constraint

Methods

ins :: () :- Eq (a :- b) #

() :=> (Ord (a :- b)) 
Instance details

Defined in Data.Constraint

Methods

ins :: () :- Ord (a :- b) #

() :=> (Show (a :- b)) 
Instance details

Defined in Data.Constraint

Methods

ins :: () :- Show (a :- b) #

a => HasDict b (a :- b) 
Instance details

Defined in Data.Constraint

Methods

evidence :: (a :- b) -> Dict b #

Eq (a :- b)

Assumes IncoherentInstances doesn't exist.

Instance details

Defined in Data.Constraint

Methods

(==) :: (a :- b) -> (a :- b) -> Bool #

(/=) :: (a :- b) -> (a :- b) -> Bool #

(Typeable p, Typeable q, p, q) => Data (p :- q) 
Instance details

Defined in Data.Constraint

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> (p :- q) -> c (p :- q) #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (p :- q) #

toConstr :: (p :- q) -> Constr #

dataTypeOf :: (p :- q) -> DataType #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (p :- q)) #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (p :- q)) #

gmapT :: (forall b. Data b => b -> b) -> (p :- q) -> p :- q #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> (p :- q) -> r #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> (p :- q) -> r #

gmapQ :: (forall d. Data d => d -> u) -> (p :- q) -> [u] #

gmapQi :: Int -> (forall d. Data d => d -> u) -> (p :- q) -> u #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> (p :- q) -> m (p :- q) #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> (p :- q) -> m (p :- q) #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> (p :- q) -> m (p :- q) #

Ord (a :- b)

Assumes IncoherentInstances doesn't exist.

Instance details

Defined in Data.Constraint

Methods

compare :: (a :- b) -> (a :- b) -> Ordering #

(<) :: (a :- b) -> (a :- b) -> Bool #

(<=) :: (a :- b) -> (a :- b) -> Bool #

(>) :: (a :- b) -> (a :- b) -> Bool #

(>=) :: (a :- b) -> (a :- b) -> Bool #

max :: (a :- b) -> (a :- b) -> a :- b #

min :: (a :- b) -> (a :- b) -> a :- b #

Show (a :- b) 
Instance details

Defined in Data.Constraint

Methods

showsPrec :: Int -> (a :- b) -> ShowS #

show :: (a :- b) -> String #

showList :: [a :- b] -> ShowS #