Copyright	(c) Artem Chirkin
License	BSD3
Safe Haskell	None
Language	Haskell2010

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

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
- Dict :: forall a. a => Dict a
newtype a :- b = Sub (a -> Dict b)

Documentation

module Numeric.Dimensions.Dim

module Numeric.Dimensions.Idx

module Data.Type.List

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 Methods readsPrec :: Int -> ReadS (Dict a) # readList :: ReadS [Dict a] # readPrec :: ReadPrec (Dict a) # readListPrec :: ReadPrec [Dict a] #
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 #