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

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

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
 Possible since GHC 7.8, when Category was made polykinded. Instance detailsDefined in Data.Constraint Methodsid :: a :- a #(.) :: (b :- c) -> (a :- b) -> a :- c # () :=> (Eq (a :- b)) Instance detailsDefined in Data.Constraint Methodsins :: () :- Eq (a :- b) # () :=> (Ord (a :- b)) Instance detailsDefined in Data.Constraint Methodsins :: () :- Ord (a :- b) # () :=> (Show (a :- b)) Instance detailsDefined in Data.Constraint Methodsins :: () :- Show (a :- b) # a => HasDict b (a :- b) Instance detailsDefined in Data.Constraint Methodsevidence :: (a :- b) -> Dict b # Eq (a :- b) Assumes IncoherentInstances doesn't exist. Instance detailsDefined in Data.Constraint Methods(==) :: (a :- b) -> (a :- b) -> Bool #(/=) :: (a :- b) -> (a :- b) -> Bool # (Typeable p, Typeable q, p, q) => Data (p :- q) Instance detailsDefined in Data.Constraint Methodsgfoldl :: (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 detailsDefined in Data.Constraint Methodscompare :: (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 detailsDefined in Data.Constraint MethodsshowsPrec :: Int -> (a :- b) -> ShowS #show :: (a :- b) -> String #showList :: [a :- b] -> ShowS #