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

License | BSD3 |

Safe Haskell | None |

Language | Haskell2010 |

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

- module Numeric.Dimensions.Dim
- module Numeric.Dimensions.Idx
- module Data.Type.List
- mapDict :: (a :- b) -> Dict a -> Dict b
- (\\) :: HasDict c e => (c => r) -> e -> r
- data Dict a where
- newtype a :- b = Sub (a => Dict b)

# Documentation

module Numeric.Dimensions.Dim

module Numeric.Dimensions.Idx

module Data.Type.List

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

Operator version of `withDict`

, with the arguments flipped

Values of type

capture a dictionary for a constraint of type `Dict`

p`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.

#### Instances

HasDict a (Dict a) | |

Defined in Data.Constraint | |

a :=> (Read (Dict a)) | |

a :=> (Monoid (Dict a)) | |

a :=> (Enum (Dict a)) | |

a :=> (Bounded (Dict a)) | |

() :=> (Eq (Dict a)) | |

() :=> (Ord (Dict a)) | |

() :=> (Show (Dict a)) | |

() :=> (Semigroup (Dict a)) | |

a => Bounded (Dict a) | |

a => Enum (Dict a) | |

Defined in Data.Constraint | |

Eq (Dict a) | |

(Typeable p, p) => Data (Dict p) | |

Defined in Data.Constraint 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 :: forall r r'. (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) | |

a => Read (Dict a) | |

Show (Dict a) | |

Semigroup (Dict a) | |

a => Monoid (Dict a) | |

This is the type of entailment.

`a `

is read as `:-`

b`a`

"entails" `b`

.

With this we can actually build a category for `Constraint`

resolution.

e.g.

Because

is a superclass of `Eq`

a

, we can show that `Ord`

a

entails `Ord`

a

.`Eq`

a

Because `instance `

exists, we can show that `Ord`

a => `Ord`

[a]

entails `Ord`

a

as well.`Ord`

[a]

This relationship is captured in the `:-`

entailment type here.

Since `p `

and entailment composes, `:-`

p`:-`

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

, 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".`Ord`

a `:-`

`Eq`

[a]

What are the two ways?

Well, we can go from

via the
superclass relationship, and then from `Ord`

a `:-`

`Eq`

a

via the
instance, or we can go from `Eq`

a `:-`

`Eq`

[a]

via the instance
then from `Ord`

a `:-`

`Ord`

[a]

through the superclass relationship
and this diagram by definition must "commute".`Ord`

[a] `:-`

`Eq`

[a]

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.

#### Instances

Category (:-) | Possible since GHC 7.8, when |

() :=> (Eq (a :- b)) | |

() :=> (Ord (a :- b)) | |

() :=> (Show (a :- b)) | |

a => HasDict b (a :- b) | |

Defined in Data.Constraint | |

Eq (a :- b) | Assumes |

(Typeable p, Typeable q, p, q) => Data (p :- q) | |

Defined in Data.Constraint 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 :: forall r r'. (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 |

Defined in Data.Constraint | |

Show (a :- b) | |