-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/
-- | Safe type-level dimensionality for multidimensional data.
--
-- Safe type-level dimensionality for multidimensional data. Please see
-- the README on GitHub at
-- https://github.com/achirkin/easytensor#readme
@package dimensions
@version 2.1.0.0
-- | A Mixture of TypeLits and TypeNats with Nats
-- represented as Natural at runtime, plus some helper functions
-- of our own.
module Data.Type.Lits
-- | (Kind) This is the kind of type-level natural numbers.
data Nat
-- | (Kind) This is the kind of type-level symbols. Declared here because
-- class IP needs it
data Symbol
-- | Get the kind of a given type. Useful when we don't want to introduce
-- another type parameter into a type signature (because the kind is
-- determined by the type), but need to have some constraints on the
-- type's kind.
type KindOf (t :: k) = k
-- | Get the kind of a given list type. Useful when we don't want to
-- introduce another type parameter into a type signature (because the
-- kind is determined by the type), but need to have some constraints on
-- the type's kind.
type KindOfEl (ts :: [k]) = k
-- | This class gives the integer associated with a type-level natural.
-- There are instances of the class for every concrete literal: 0, 1, 2,
-- etc.
class KnownNat (n :: Nat)
natVal :: KnownNat n => proxy n -> Natural
natVal' :: KnownNat n => Proxy# n -> Natural
-- | This class gives the string associated with a type-level symbol. There
-- are instances of the class for every concrete literal: "hello", etc.
class KnownSymbol (n :: Symbol)
symbolVal :: KnownSymbol n => proxy n -> String
symbolVal' :: KnownSymbol n => Proxy# n -> String
-- | This type represents unknown type-level natural numbers.
data SomeNat
[SomeNat] :: forall (n :: Nat). KnownNat n => Proxy n -> SomeNat
-- | This type represents unknown type-level symbols.
data SomeSymbol
[SomeSymbol] :: forall (n :: Symbol). KnownSymbol n => Proxy n -> SomeSymbol
-- | Convert an integer into an unknown type-level natural.
someNatVal :: Natural -> SomeNat
-- | Convert a string into an unknown type-level symbol.
someSymbolVal :: String -> SomeSymbol
-- | We either get evidence that this function was instantiated with the
-- same type-level numbers, or Nothing.
sameNat :: (KnownNat a, KnownNat b) => Proxy a -> Proxy b -> Maybe (a :~: b)
-- | We either get evidence that this function was instantiated with the
-- same type-level symbols, or Nothing.
sameSymbol :: (KnownSymbol a, KnownSymbol b) => Proxy a -> Proxy b -> Maybe (a :~: b)
-- | Addition of type-level naturals.
type family (+) (a :: Nat) (b :: Nat) :: Nat
infixl 6 +
-- | Multiplication of type-level naturals.
type family (*) (a :: Nat) (b :: Nat) :: Nat
infixl 7 *
-- | Exponentiation of type-level naturals.
type family (^) (a :: Nat) (b :: Nat) :: Nat
infixr 8 ^
-- | Subtraction of type-level naturals.
type family (-) (a :: Nat) (b :: Nat) :: Nat
infixl 6 -
-- | Division (round down) of natural numbers. Div x 0 is
-- undefined (i.e., it cannot be reduced).
type family Div (a :: Nat) (b :: Nat) :: Nat
infixl 7 `Div`
-- | Modulus of natural numbers. Mod x 0 is undefined (i.e., it
-- cannot be reduced).
type family Mod (a :: Nat) (b :: Nat) :: Nat
infixl 7 `Mod`
-- | Log base 2 (round down) of natural numbers. Log 0 is
-- undefined (i.e., it cannot be reduced).
type family Log2 (a :: Nat) :: Nat
-- | Miminum among two type-level naturals.
type Min (a :: Nat) (b :: Nat) = Min' a b (CmpNat a b)
-- | Maximum among two type-level naturals.
type Max (a :: Nat) (b :: Nat) = Min' a b (CmpNat a b)
-- | Concatenation of type-level symbols.
type family AppendSymbol (a :: Symbol) (b :: Symbol) :: Symbol
-- | Convert a type-level Nat into a type-level Symbol.
type family ShowNat (n :: Nat) :: Symbol
-- | Comparison of type-level naturals, as a function.
type family CmpNat (a :: Nat) (b :: Nat) :: Ordering
-- | Comparison of type-level symbols, as a function.
type family CmpSymbol (a :: Symbol) (b :: Symbol) :: Ordering
-- | Comparison of type-level naturals, as a constraint.
type (<=) (a :: Nat) (b :: Nat) = LE a b (CmpNat a b)
-- | Singleton-style version of Ordering. Pattern-match againts its
-- constructor to witness the result of type-level comparison.
data SOrdering :: Ordering -> Type
[SLT] :: SOrdering 'LT
[SEQ] :: SOrdering 'EQ
[SGT] :: SOrdering 'GT
-- | Pattern-match against the result of this function to get the evidence
-- of comparing type-level Nats.
cmpNat :: forall (a :: Nat) (b :: Nat) (proxy :: Nat -> Type). (KnownNat a, KnownNat b) => proxy a -> proxy b -> SOrdering (CmpNat a b)
-- | Pattern-match against the result of this function to get the evidence
-- of comparing type-level Symbols.
cmpSymbol :: forall (a :: Symbol) (b :: Symbol) (proxy :: Symbol -> Type). (KnownSymbol a, KnownSymbol b) => proxy a -> proxy b -> SOrdering (CmpSymbol a b)
-- | The type-level equivalent of error.
--
-- The polymorphic kind of this type allows it to be used in several
-- settings. For instance, it can be used as a constraint, e.g. to
-- provide a better error message for a non-existent instance,
--
--
-- -- in a context
-- instance TypeError (Text "Cannot Show functions." :$$:
-- Text "Perhaps there is a missing argument?")
-- => Show (a -> b) where
-- showsPrec = error "unreachable"
--
--
-- It can also be placed on the right-hand side of a type-level function
-- to provide an error for an invalid case,
--
--
-- type family ByteSize x where
-- ByteSize Word16 = 2
-- ByteSize Word8 = 1
-- ByteSize a = TypeError (Text "The type " :<>: ShowType a :<>:
-- Text " is not exportable.")
--
type family TypeError (a :: ErrorMessage) :: b
-- | A description of a custom type error.
data ErrorMessage
-- | Show the text as is.
[Text] :: () => Symbol -> ErrorMessage
-- | Pretty print the type. ShowType :: k -> ErrorMessage
[ShowType] :: forall t. () => t -> ErrorMessage
-- | Put two pieces of error message next to each other.
[:<>:] :: () => ErrorMessage -> ErrorMessage -> ErrorMessage
-- | Stack two pieces of error message on top of each other.
[:$$:] :: () => ErrorMessage -> ErrorMessage -> ErrorMessage
infixl 6 :<>:
infixl 5 :$$:
-- | Provides type-level operations on lists.
module Data.Type.List
-- | Infix-style synonym for concatenation
type (as :: [k]) ++ (bs :: [k]) = Concat as bs
infixr 5 ++
-- | Synonym for a type-level Snoc.
type (ns :: [k]) +: (n :: k) = Snoc ns n
infixl 6 +:
-- | Synonym for a type-level Cons.
type (a :: k) :+ (as :: [k]) = a : as
infixr 5 :+
-- | Empty list, same as '[].
type Empty = ('[] :: [k])
-- | Appending a list, represents an Op counterpart of
-- (':).
type Cons (a :: k) (as :: [k]) = a : as
-- | Appending a list on the other side (injective).
type Snoc (xs :: [k]) (x :: k) = (RunList (Snoc' xs x :: List k) :: [k])
-- | Extract the first element of a list, which must be non-empty.
type family Head (xs :: [k]) :: k
-- | Extract the elements after the head of a list, which must be
-- non-empty.
type family Tail (xs :: [k]) :: [k]
-- | Extract the last element of a list, which must be non-empty.
type family Last (xs :: [k]) :: k
-- | Extract all but last elements of a list, which must be non-empty.
type family Init (xs :: [k]) = (ys :: [k]) | ys -> k
-- | Append two lists.
type family Concat (as :: [k]) (bs :: [k]) :: [k]
-- | Remove prefix as from a list asbs if as is
-- a prefix; fail otherwise.
type family StripPrefix (as :: [k]) (asbs :: [k]) :: [k]
-- | Remove suffix bs from a list asbs if bs is
-- a suffix; fail otherwise.
type family StripSuffix (bs :: [k]) (asbs :: [k]) :: [k]
-- | Reverse elements of a list (injective).
type Reverse (xs :: [k]) = (RunList (Reverse' xs :: List k) :: [k])
-- | Take n xs returns the prefix of a list of length max n
-- (length xs).
type family Take (n :: Nat) (xs :: [k]) :: [k]
-- | Drop n xs drops up to n elements of xs.
type family Drop (n :: Nat) (xs :: [k]) :: [k]
-- | Number of elements in a list.
type family Length (xs :: [k]) :: Nat
-- | All elements of a type list must satisfy the same constraint.
type family All (f :: k -> Constraint) (xs :: [k]) :: Constraint
-- | Map a functor over the elements of a type list.
type family Map (f :: a -> b) (xs :: [a]) :: [b]
-- | Unmap a functor over the elements of a type list.
type family UnMap (f :: a -> b) (xs :: [b]) :: [a]
-- | Check if an item is a member of a list.
type family Elem (x :: k) (xs :: [k]) :: Constraint
-- | Represent a decomposition of a list by appending an element to its
-- end.
class (bs ~ Snoc as a, as ~ Init bs, a ~ Last bs, SnocListCtx as a bs, ConcatList as '[a] bs) => SnocList (as :: [k]) (a :: k) (bs :: [k]) | as a -> bs, bs -> as a, as -> k, a -> a, bs -> k
-- | Represent two lists that are Reverse of each other
class (as ~ Reverse bs, bs ~ Reverse as, ReverseList bs as, ReverseListCtx as bs) => ReverseList (as :: [k]) (bs :: [k]) | as -> bs, bs -> as, as -> k, bs -> k
-- | Represent a triple of lists forming a relation (as ++ bs) ~
-- asbs
--
-- NB: functional dependency bs asbs -> as does not seem to
-- be possible, because dependency checking happens before constraints
-- checking and does not take constraints into account.
class (asbs ~ Concat as bs, as ~ StripSuffix bs asbs, bs ~ StripPrefix as asbs, ConcatListCtx1 as bs asbs, ConcatListCtx2 as bs asbs (bs == asbs)) => ConcatList (as :: [k]) (bs :: [k]) (asbs :: [k]) | as bs -> asbs, as asbs -> bs, as -> k, bs -> k, asbs -> k
-- | Derive ConcatList given StripSuffix
inferStripSuffix :: forall as bs asbs. as ~ StripSuffix bs asbs => Dict (ConcatList as bs asbs)
-- | Derive ConcatList given StripPrefix
inferStripPrefix :: forall as bs asbs. bs ~ StripPrefix as asbs => Dict (ConcatList as bs asbs)
-- | Derive ConcatList given Concat
inferConcat :: forall as bs asbs. asbs ~ Concat as bs => Dict (ConcatList as bs asbs)
-- | Given a Typeable list, infer this constraint for its parts.
inferTypeableCons :: forall ys x xs. (Typeable ys, ys ~ (x : xs)) => Dict (Typeable x, Typeable xs)
-- | 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.
module Numeric.TypedList
-- | Type-indexed list
data TypedList (f :: (k -> Type)) (xs :: [k])
-- | Zero-length type list
pattern U :: forall (k :: Type) (f :: k -> Type) (xs :: [k]). () => xs ~ '[] => TypedList f xs
-- | Constructing a type-indexed list
pattern (:*) :: forall f xs. () => forall y ys. xs ~ (y : ys) => f y -> TypedList f ys -> TypedList f xs
-- | Zero-length type list; synonym to U.
pattern Empty :: forall (k :: Type) (f :: k -> Type) (xs :: [k]). () => xs ~ '[] => TypedList f xs
-- | Pattern matching against this causes RepresentableList instance
-- come into scope. Also it allows constructing a term-level list out of
-- a constraint.
pattern TypeList :: forall xs. () => RepresentableList xs => TypeList xs
-- | Pattern matching against this allows manipulating lists of
-- constraints. Useful when creating functions that change the shape of
-- dimensions.
pattern EvList :: forall c xs. () => (All c xs, RepresentableList xs) => DictList c xs
-- | Constructing a type-indexed list in the canonical way
pattern Cons :: forall f xs. () => forall y ys. xs ~ (y : ys) => f y -> TypedList f ys -> TypedList f xs
-- | Constructing a type-indexed list from the other end
pattern Snoc :: forall f xs. () => forall sy y. SnocList sy y xs => TypedList f sy -> f y -> TypedList f xs
-- | Reverse a typed list
pattern Reverse :: forall f xs. () => forall sx. ReverseList xs sx => TypedList f sx -> TypedList f xs
infixr 5 :*
-- | Representable type lists. Allows getting type information about list
-- structure at runtime.
class RepresentableList xs
-- | Get type-level constructed list
tList :: RepresentableList xs => TypeList xs
-- | Same as Dict, but allows to separate constraint function from
-- the type it is applied to.
data Dict1 :: (k -> Constraint) -> k -> Type
[Dict1] :: c a => Dict1 c a
-- | A list of dicts for the same constraint over several types.
type DictList (c :: k -> Constraint) = (TypedList (Dict1 c) :: [k] -> Type)
-- | A list of type proxies
type TypeList = (TypedList Proxy :: [k] -> Type)
-- | Get a constructible TypeList from any other TypedList;
-- Pattern matching agains the result brings RepresentableList
-- constraint into the scope:
--
--
-- case types ts of TypeList -> ...
--
types :: forall f xs. TypedList f xs -> TypeList xs
-- | 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.
typeables :: forall xs. Typeable xs => TypeList xs
-- | If all elements of a TypedList are Typeable, then
-- the list of these elements is also Typeable.
inferTypeableList :: forall f xs. (Typeable (KindOfEl xs), All Typeable xs) => TypedList f xs -> Dict (Typeable xs)
-- | Return the number of elements in a TypedList (same as
-- length).
order :: forall f xs. TypedList f xs -> Dim (Length xs)
-- | Return the number of elements in a type list xs bound by a
-- constraint RepresentableList xs (same as order, but
-- takes no value arguments).
order' :: forall xs. RepresentableList xs => Dim (Length xs)
-- | O(1) append an element in front of a TypedList (same
-- as `(:)` for lists).
cons :: forall f x xs. f x -> TypedList f xs -> TypedList f (x :+ xs)
-- | O(n) append an element to the end of a TypedList.
snoc :: forall f xs x. TypedList f xs -> f x -> TypedList f (xs +: x)
-- | O(n) return elements of a TypedList in reverse order.
reverse :: forall f xs. TypedList f xs -> TypedList f (Reverse xs)
-- | 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.
take :: forall (n :: Nat) f xs. Dim n -> TypedList f xs -> TypedList f (Take n xs)
-- | 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.
drop :: forall (n :: Nat) f xs. Dim n -> TypedList f xs -> TypedList f (Drop n xs)
-- | O(1) Extract the first element of a TypedList, which
-- must be non-empty.
head :: forall f xs. TypedList f xs -> f (Head xs)
-- | O(1) Extract the elements after the head of a
-- TypedList, which must be non-empty.
tail :: forall f xs. TypedList f xs -> TypedList f (Tail xs)
-- | O(n) Extract the last element of a TypedList, which
-- must be non-empty.
last :: forall f xs. TypedList f xs -> f (Last xs)
-- | O(n) Return all the elements of a TypedList except the
-- last one (the list must be non-empty).
init :: forall f xs. TypedList f xs -> TypedList f (Init xs)
-- | 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.
splitAt :: forall (n :: Nat) f xs. Dim n -> TypedList f xs -> (TypedList f (Take n xs), TypedList f (Drop n xs))
-- | 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.
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))
-- | 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.
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))
-- | Returns two things at once: (Evidence that types of lists match,
-- value-level equality).
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)
-- | Concat two TypedLists. It calls `Prelude.(++)` under the
-- hood, so expect the same behavior.
concat :: forall f xs ys. TypedList f xs -> TypedList f ys -> TypedList f (xs ++ ys)
-- | Return the number of elements in a TypedList (same as
-- order).
length :: forall f xs. TypedList f xs -> Dim (Length xs)
-- | Map a function over contents of a typed list
map :: forall f g xs. (forall a. f a -> g a) -> TypedList f xs -> TypedList g xs
-- | Generic show function for a TypedList.
typedListShowsPrecC :: forall c f xs. All c xs => String -> (forall x. c x => Int -> f x -> ShowS) -> Int -> TypedList f xs -> ShowS
-- | Generic show function for a TypedList.
typedListShowsPrec :: forall f xs. (forall x. Int -> f x -> ShowS) -> Int -> TypedList f xs -> ShowS
-- | Generic read function for a TypedList. Requires a "template"
-- to enforce the structure of the type list.
typedListReadPrec :: forall c f xs g. All c xs => String -> (forall x. c x => ReadPrec (f x)) -> TypedList g xs -> ReadPrec (TypedList f xs)
-- | Generic read function for a TypedList of unknown length.
withTypedListReadPrec :: forall f (r :: Type). (forall (z :: Type). (forall x. f x -> z) -> ReadPrec z) -> (forall xs. TypedList f xs -> r) -> ReadPrec r
instance forall k (p :: k -> GHC.Types.Constraint) (a :: k). GHC.Classes.Eq (Numeric.TypedList.Dict1 p a)
instance forall k (p :: k -> GHC.Types.Constraint) (a :: k). GHC.Classes.Ord (Numeric.TypedList.Dict1 p a)
instance forall k (p :: k -> GHC.Types.Constraint) (a :: k). GHC.Show.Show (Numeric.TypedList.Dict1 p a)
instance Numeric.TypedList.RepresentableList '[]
instance forall k (xs :: [k]) (x :: k). Numeric.TypedList.RepresentableList xs => Numeric.TypedList.RepresentableList (x : xs)
instance forall k (p :: k -> GHC.Types.Constraint) (a :: k). (Data.Typeable.Internal.Typeable k, Data.Typeable.Internal.Typeable p, Data.Typeable.Internal.Typeable a, p a) => Data.Data.Data (Numeric.TypedList.Dict1 p a)
instance forall k (f :: k -> *) (xs :: [k]). GHC.Generics.Generic (Numeric.TypedList.TypedList f xs)
instance forall k (f :: k -> *) (xs :: [k]). (Data.Typeable.Internal.Typeable k, Data.Typeable.Internal.Typeable f, Data.Typeable.Internal.Typeable xs, Data.Type.List.All Data.Data.Data (Data.Type.List.Map f xs)) => Data.Data.Data (Numeric.TypedList.TypedList f xs)
module Numeric.Tuple.Strict
-- | This is an almost complete copy of Identity by (c) Andy Gill
-- 2001.
newtype Id a
Id :: a -> Id a
[runId] :: Id a -> a
-- | A tuple indexed by a list of types
type Tuple = (TypedList Id :: [Type] -> Type)
-- | Type-indexed list
data TypedList (f :: (k -> Type)) (xs :: [k])
-- | Zero-length type list
pattern U :: forall (k :: Type) (f :: k -> Type) (xs :: [k]). () => xs ~ '[] => TypedList f xs
-- | Constructing a type-indexed list
pattern (:*) :: forall f xs. () => forall y ys. xs ~ (y : ys) => f y -> TypedList f ys -> TypedList f xs
-- | Constructing a type-indexed list
pattern (:$) :: forall (xs :: [Type]). () => forall (y :: Type) (ys :: [Type]). xs ~ (y : ys) => y -> Tuple ys -> Tuple xs
-- | Constructing a type-indexed list
pattern (:!) :: forall (xs :: [Type]). () => forall (y :: Type) (ys :: [Type]). xs ~ (y : ys) => y -> Tuple ys -> Tuple xs
-- | Zero-length type list; synonym to U.
pattern Empty :: forall (k :: Type) (f :: k -> Type) (xs :: [k]). () => xs ~ '[] => TypedList f xs
-- | Pattern matching against this causes RepresentableList instance
-- come into scope. Also it allows constructing a term-level list out of
-- a constraint.
pattern TypeList :: forall xs. () => RepresentableList xs => TypeList xs
-- | Constructing a type-indexed list in the canonical way
pattern Cons :: forall f xs. () => forall y ys. xs ~ (y : ys) => f y -> TypedList f ys -> TypedList f xs
-- | Constructing a type-indexed list from the other end
pattern Snoc :: forall f xs. () => forall sy y. SnocList sy y xs => TypedList f sy -> f y -> TypedList f xs
-- | Reverse a typed list
pattern Reverse :: forall f xs. () => forall sx. ReverseList xs sx => TypedList f sx -> TypedList f xs
infixr 5 :$
infixr 5 :!
infixr 5 :*
-- | Grow a tuple on the left O(1).
(*$) :: x -> Tuple xs -> Tuple (x :+ xs)
infixr 5 *$
-- | Grow a tuple on the right. Note, it traverses an element list inside
-- O(n).
($*) :: Tuple xs -> x -> Tuple (xs +: x)
infixl 5 $*
-- | Grow a tuple on the left while evaluating arguments to WHNF O(1).
(*!) :: x -> Tuple xs -> Tuple (x :+ xs)
infixr 5 *!
-- | Grow a tuple on the right while evaluating arguments to WHNF. Note, it
-- traverses an element list inside O(n).
(!*) :: Tuple xs -> x -> Tuple (xs +: x)
infixl 5 !*
instance Data.Traversable.Traversable Numeric.Tuple.Strict.Id
instance Foreign.Storable.Storable a => Foreign.Storable.Storable (Numeric.Tuple.Strict.Id a)
instance GHC.Base.Semigroup a => GHC.Base.Semigroup (Numeric.Tuple.Strict.Id a)
instance GHC.Float.RealFloat a => GHC.Float.RealFloat (Numeric.Tuple.Strict.Id a)
instance GHC.Real.RealFrac a => GHC.Real.RealFrac (Numeric.Tuple.Strict.Id a)
instance GHC.Real.Real a => GHC.Real.Real (Numeric.Tuple.Strict.Id a)
instance GHC.Classes.Ord a => GHC.Classes.Ord (Numeric.Tuple.Strict.Id a)
instance GHC.Num.Num a => GHC.Num.Num (Numeric.Tuple.Strict.Id a)
instance GHC.Base.Monoid a => GHC.Base.Monoid (Numeric.Tuple.Strict.Id a)
instance GHC.Arr.Ix a => GHC.Arr.Ix (Numeric.Tuple.Strict.Id a)
instance Data.String.IsString a => Data.String.IsString (Numeric.Tuple.Strict.Id a)
instance GHC.Real.Integral a => GHC.Real.Integral (Numeric.Tuple.Strict.Id a)
instance GHC.Generics.Generic1 Numeric.Tuple.Strict.Id
instance GHC.Generics.Generic (Numeric.Tuple.Strict.Id a)
instance GHC.Real.Fractional a => GHC.Real.Fractional (Numeric.Tuple.Strict.Id a)
instance GHC.Float.Floating a => GHC.Float.Floating (Numeric.Tuple.Strict.Id a)
instance Data.Bits.FiniteBits a => Data.Bits.FiniteBits (Numeric.Tuple.Strict.Id a)
instance GHC.Classes.Eq a => GHC.Classes.Eq (Numeric.Tuple.Strict.Id a)
instance GHC.Enum.Enum a => GHC.Enum.Enum (Numeric.Tuple.Strict.Id a)
instance Data.Data.Data a => Data.Data.Data (Numeric.Tuple.Strict.Id a)
instance GHC.Enum.Bounded a => GHC.Enum.Bounded (Numeric.Tuple.Strict.Id a)
instance Data.Bits.Bits a => Data.Bits.Bits (Numeric.Tuple.Strict.Id a)
instance Data.Type.List.All GHC.Base.Semigroup xs => GHC.Base.Semigroup (Numeric.Tuple.Strict.Tuple xs)
instance (Numeric.TypedList.RepresentableList xs, Data.Type.List.All GHC.Base.Semigroup xs, Data.Type.List.All GHC.Base.Monoid xs) => GHC.Base.Monoid (Numeric.Tuple.Strict.Tuple xs)
instance (Numeric.TypedList.RepresentableList xs, Data.Type.List.All GHC.Enum.Bounded xs) => GHC.Enum.Bounded (Numeric.Tuple.Strict.Tuple xs)
instance Data.Type.List.All GHC.Classes.Eq xs => GHC.Classes.Eq (Numeric.Tuple.Strict.Tuple xs)
instance (Data.Type.List.All GHC.Classes.Eq xs, Data.Type.List.All GHC.Classes.Ord xs) => GHC.Classes.Ord (Numeric.Tuple.Strict.Tuple xs)
instance Data.Type.List.All GHC.Show.Show xs => GHC.Show.Show (Numeric.Tuple.Strict.Tuple xs)
instance (Data.Type.List.All GHC.Read.Read xs, Numeric.TypedList.RepresentableList xs) => GHC.Read.Read (Numeric.Tuple.Strict.Tuple xs)
instance GHC.Read.Read a => GHC.Read.Read (Numeric.Tuple.Strict.Id a)
instance GHC.Show.Show a => GHC.Show.Show (Numeric.Tuple.Strict.Id a)
instance Data.Functor.Classes.Read1 Numeric.Tuple.Strict.Id
instance Data.Functor.Classes.Show1 Numeric.Tuple.Strict.Id
instance Data.Functor.Classes.Eq1 Numeric.Tuple.Strict.Id
instance Data.Functor.Classes.Ord1 Numeric.Tuple.Strict.Id
instance Data.Foldable.Foldable Numeric.Tuple.Strict.Id
instance GHC.Base.Functor Numeric.Tuple.Strict.Id
instance GHC.Base.Applicative Numeric.Tuple.Strict.Id
instance GHC.Base.Monad Numeric.Tuple.Strict.Id
instance Control.Monad.Fix.MonadFix Numeric.Tuple.Strict.Id
instance Control.Monad.Zip.MonadZip Numeric.Tuple.Strict.Id
module Numeric.Tuple.Lazy
-- | This is an almost complete copy of Identity by (c) Andy Gill
-- 2001.
newtype Id a
Id :: a -> Id a
[runId] :: Id a -> a
-- | A tuple indexed by a list of types
type Tuple = (TypedList Id :: [Type] -> Type)
-- | Type-indexed list
data TypedList (f :: (k -> Type)) (xs :: [k])
-- | Zero-length type list
pattern U :: forall (k :: Type) (f :: k -> Type) (xs :: [k]). () => xs ~ '[] => TypedList f xs
-- | Constructing a type-indexed list
pattern (:*) :: forall f xs. () => forall y ys. xs ~ (y : ys) => f y -> TypedList f ys -> TypedList f xs
-- | Constructing a type-indexed list
pattern (:$) :: forall (xs :: [Type]). () => forall (y :: Type) (ys :: [Type]). xs ~ (y : ys) => y -> Tuple ys -> Tuple xs
-- | Constructing a type-indexed list
pattern (:!) :: forall (xs :: [Type]). () => forall (y :: Type) (ys :: [Type]). xs ~ (y : ys) => y -> Tuple ys -> Tuple xs
-- | Zero-length type list; synonym to U.
pattern Empty :: forall (k :: Type) (f :: k -> Type) (xs :: [k]). () => xs ~ '[] => TypedList f xs
-- | Pattern matching against this causes RepresentableList instance
-- come into scope. Also it allows constructing a term-level list out of
-- a constraint.
pattern TypeList :: forall xs. () => RepresentableList xs => TypeList xs
-- | Constructing a type-indexed list in the canonical way
pattern Cons :: forall f xs. () => forall y ys. xs ~ (y : ys) => f y -> TypedList f ys -> TypedList f xs
-- | Constructing a type-indexed list from the other end
pattern Snoc :: forall f xs. () => forall sy y. SnocList sy y xs => TypedList f sy -> f y -> TypedList f xs
-- | Reverse a typed list
pattern Reverse :: forall f xs. () => forall sx. ReverseList xs sx => TypedList f sx -> TypedList f xs
infixr 5 :$
infixr 5 :!
infixr 5 :*
-- | Grow a tuple on the left O(1).
(*$) :: x -> Tuple xs -> Tuple (x :+ xs)
infixr 5 *$
-- | Grow a tuple on the right. Note, it traverses an element list inside
-- O(n).
($*) :: Tuple xs -> x -> Tuple (xs +: x)
infixl 5 $*
-- | Grow a tuple on the left while evaluating arguments to WHNF O(1).
(*!) :: x -> Tuple xs -> Tuple (x :+ xs)
infixr 5 *!
-- | Grow a tuple on the right while evaluating arguments to WHNF. Note, it
-- traverses an element list inside O(n).
(!*) :: Tuple xs -> x -> Tuple (xs +: x)
infixl 5 !*
instance Data.Traversable.Traversable Numeric.Tuple.Lazy.Id
instance Foreign.Storable.Storable a => Foreign.Storable.Storable (Numeric.Tuple.Lazy.Id a)
instance GHC.Base.Semigroup a => GHC.Base.Semigroup (Numeric.Tuple.Lazy.Id a)
instance GHC.Float.RealFloat a => GHC.Float.RealFloat (Numeric.Tuple.Lazy.Id a)
instance GHC.Real.RealFrac a => GHC.Real.RealFrac (Numeric.Tuple.Lazy.Id a)
instance GHC.Real.Real a => GHC.Real.Real (Numeric.Tuple.Lazy.Id a)
instance GHC.Classes.Ord a => GHC.Classes.Ord (Numeric.Tuple.Lazy.Id a)
instance GHC.Num.Num a => GHC.Num.Num (Numeric.Tuple.Lazy.Id a)
instance GHC.Base.Monoid a => GHC.Base.Monoid (Numeric.Tuple.Lazy.Id a)
instance GHC.Arr.Ix a => GHC.Arr.Ix (Numeric.Tuple.Lazy.Id a)
instance Data.String.IsString a => Data.String.IsString (Numeric.Tuple.Lazy.Id a)
instance GHC.Real.Integral a => GHC.Real.Integral (Numeric.Tuple.Lazy.Id a)
instance GHC.Generics.Generic1 Numeric.Tuple.Lazy.Id
instance GHC.Generics.Generic (Numeric.Tuple.Lazy.Id a)
instance GHC.Real.Fractional a => GHC.Real.Fractional (Numeric.Tuple.Lazy.Id a)
instance GHC.Float.Floating a => GHC.Float.Floating (Numeric.Tuple.Lazy.Id a)
instance Data.Bits.FiniteBits a => Data.Bits.FiniteBits (Numeric.Tuple.Lazy.Id a)
instance GHC.Classes.Eq a => GHC.Classes.Eq (Numeric.Tuple.Lazy.Id a)
instance GHC.Enum.Enum a => GHC.Enum.Enum (Numeric.Tuple.Lazy.Id a)
instance Data.Data.Data a => Data.Data.Data (Numeric.Tuple.Lazy.Id a)
instance GHC.Enum.Bounded a => GHC.Enum.Bounded (Numeric.Tuple.Lazy.Id a)
instance Data.Bits.Bits a => Data.Bits.Bits (Numeric.Tuple.Lazy.Id a)
instance Data.Type.List.All GHC.Base.Semigroup xs => GHC.Base.Semigroup (Numeric.Tuple.Lazy.Tuple xs)
instance (Numeric.TypedList.RepresentableList xs, Data.Type.List.All GHC.Base.Semigroup xs, Data.Type.List.All GHC.Base.Monoid xs) => GHC.Base.Monoid (Numeric.Tuple.Lazy.Tuple xs)
instance (Numeric.TypedList.RepresentableList xs, Data.Type.List.All GHC.Enum.Bounded xs) => GHC.Enum.Bounded (Numeric.Tuple.Lazy.Tuple xs)
instance Data.Type.List.All GHC.Classes.Eq xs => GHC.Classes.Eq (Numeric.Tuple.Lazy.Tuple xs)
instance (Data.Type.List.All GHC.Classes.Eq xs, Data.Type.List.All GHC.Classes.Ord xs) => GHC.Classes.Ord (Numeric.Tuple.Lazy.Tuple xs)
instance Data.Type.List.All GHC.Show.Show xs => GHC.Show.Show (Numeric.Tuple.Lazy.Tuple xs)
instance (Data.Type.List.All GHC.Read.Read xs, Numeric.TypedList.RepresentableList xs) => GHC.Read.Read (Numeric.Tuple.Lazy.Tuple xs)
instance GHC.Read.Read a => GHC.Read.Read (Numeric.Tuple.Lazy.Id a)
instance GHC.Show.Show a => GHC.Show.Show (Numeric.Tuple.Lazy.Id a)
instance Data.Functor.Classes.Read1 Numeric.Tuple.Lazy.Id
instance Data.Functor.Classes.Show1 Numeric.Tuple.Lazy.Id
instance Data.Functor.Classes.Eq1 Numeric.Tuple.Lazy.Id
instance Data.Functor.Classes.Ord1 Numeric.Tuple.Lazy.Id
instance Data.Foldable.Foldable Numeric.Tuple.Lazy.Id
instance GHC.Base.Functor Numeric.Tuple.Lazy.Id
instance GHC.Base.Applicative Numeric.Tuple.Lazy.Id
instance GHC.Base.Monad Numeric.Tuple.Lazy.Id
instance Control.Monad.Fix.MonadFix Numeric.Tuple.Lazy.Id
instance Control.Monad.Zip.MonadZip Numeric.Tuple.Lazy.Id
module Numeric.Tuple
-- | O(n) Convert a lazy Tuple to a strict Tuple,
-- forcing all its values to the WHNF along the way.
toStrict :: Tuple xs -> Tuple xs
-- | O(n) Convert a strict Tuple to a lazy Tuple
-- by means of a simple coercion.
fromStrict :: Tuple xs -> Tuple xs
-- | This module provides KnownDim class that is similar to
-- KnownNat from TypeNats, but keeps Words instead
-- of Naturals; Also it provides Dim data type serving as a
-- singleton suitable for recovering an instance of the KnownDim
-- class. A set of utility functions provide inference functionality, so
-- that KnownDim can be preserved over some type-level operations.
--
-- Provides a data type Dims ds to keep dimension sizes for
-- multiple-dimensional data. 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.
module Numeric.Dimensions.Dim
-- | (Kind) This is the kind of type-level natural numbers.
data Nat
-- | Either known or unknown at compile-time natural number
data XNat
XN :: Nat -> XNat
N :: Nat -> XNat
-- | Unknown natural number, known to be not smaller than the given Nat
type XN = 'XN
-- | Known natural number
type N = 'N
-- | GADT to support KnownDimType type class. Find out if this type
-- variable is a Nat or XNat, and whether XNat
-- is of known or constrained type.
data DimType (d :: k)
-- | This is a plain Nat
[DimTNat] :: DimType (n :: Nat)
-- | Given XNat is known
[DimTXNatN] :: DimType (N n)
-- | Given XNat is constrained unknown
[DimTXNatX] :: DimType (XN m)
-- | Figure out whether the type-level dimension is Nat, or `N Nat`,
-- or `XN Nat`.
class KnownDimType d
-- | Pattern-match against this to out the value (type) of the dim type
-- variable.
dimType :: KnownDimType d => DimType d
-- | GADT to support KnownDimKind type class. Match against its
-- constructors to know if k is Nat or XNat
data DimKind (k :: Type)
-- | Working on Nat.
[DimKNat] :: DimKind Nat
-- | Working on XNat.
[DimKXNat] :: DimKind XNat
-- | Figure out whether the type-level dimension is Nat or
-- XNat.
class KnownDimKind k
-- | Pattern-match against this to out the kind of the dim type variable.
dimKind :: KnownDimKind k => DimKind k
-- | Singleton type to store type-level dimension value.
--
-- On the one hand, it can be used to let type-inference system know
-- relations between type-level naturals. On the other hand, this is just
-- a newtype wrapper on the Word type.
--
-- Usually, the type parameter of Dim is either Nat or
-- XNat. If dimensionality of your data is known in advance, use
-- Nat; if you know the size of some dimensions, but do not know
-- the size of others, use XNats to represent them.
data Dim (x :: k)
-- | Match against this pattern to bring KnownDim instance into
-- scope.
pattern D :: forall d. KnownDimType d => (KindOf d ~ Nat, KnownDim d) => Dim d
-- | Statically known XNat
pattern Dn :: forall d. KnownDimType d => forall (n :: Nat). (KindOf d ~ XNat, d ~ N n) => Dim n -> Dim d
-- | XNat that is unknown at compile time. Same as SomeNat,
-- but for a dimension: Hide dimension size inside, but allow specifying
-- its minimum possible value.
pattern Dx :: forall d. KnownDimType d => forall (m :: Nat) (n :: Nat). (KindOf d ~ XNat, d ~ XN m, m <= n) => Dim n -> Dim d
-- | Match Dim n against a concrete Nat
pattern D0 :: forall (n :: Nat). () => n ~ 0 => Dim n
-- | Match Dim n against a concrete Nat
pattern D1 :: forall (n :: Nat). () => n ~ 1 => Dim n
-- | Match Dim n against a concrete Nat
pattern D2 :: forall (n :: Nat). () => n ~ 2 => Dim n
-- | Match Dim n against a concrete Nat
pattern D3 :: forall (n :: Nat). () => n ~ 3 => Dim n
-- | Match Dim n against a concrete Nat
pattern D4 :: forall (n :: Nat). () => n ~ 4 => Dim n
-- | Match Dim n against a concrete Nat
pattern D5 :: forall (n :: Nat). () => n ~ 5 => Dim n
-- | Match Dim n against a concrete Nat
pattern D6 :: forall (n :: Nat). () => n ~ 6 => Dim n
-- | Match Dim n against a concrete Nat
pattern D7 :: forall (n :: Nat). () => n ~ 7 => Dim n
-- | Match Dim n against a concrete Nat
pattern D8 :: forall (n :: Nat). () => n ~ 8 => Dim n
-- | Match Dim n against a concrete Nat
pattern D9 :: forall (n :: Nat). () => n ~ 9 => Dim n
-- | Match Dim n against a concrete Nat
pattern D10 :: forall (n :: Nat). () => n ~ 10 => Dim n
-- | Match Dim n against a concrete Nat
pattern D11 :: forall (n :: Nat). () => n ~ 11 => Dim n
-- | Match Dim n against a concrete Nat
pattern D12 :: forall (n :: Nat). () => n ~ 12 => Dim n
-- | Match Dim n against a concrete Nat
pattern D13 :: forall (n :: Nat). () => n ~ 13 => Dim n
-- | Match Dim n against a concrete Nat
pattern D14 :: forall (n :: Nat). () => n ~ 14 => Dim n
-- | Match Dim n against a concrete Nat
pattern D15 :: forall (n :: Nat). () => n ~ 15 => Dim n
-- | Match Dim n against a concrete Nat
pattern D16 :: forall (n :: Nat). () => n ~ 16 => Dim n
-- | Match Dim n against a concrete Nat
pattern D17 :: forall (n :: Nat). () => n ~ 17 => Dim n
-- | Match Dim n against a concrete Nat
pattern D18 :: forall (n :: Nat). () => n ~ 18 => Dim n
-- | Match Dim n against a concrete Nat
pattern D19 :: forall (n :: Nat). () => n ~ 19 => Dim n
-- | Match Dim n against a concrete Nat
pattern D20 :: forall (n :: Nat). () => n ~ 20 => Dim n
-- | Match Dim n against a concrete Nat
pattern D21 :: forall (n :: Nat). () => n ~ 21 => Dim n
-- | Match Dim n against a concrete Nat
pattern D22 :: forall (n :: Nat). () => n ~ 22 => Dim n
-- | Match Dim n against a concrete Nat
pattern D23 :: forall (n :: Nat). () => n ~ 23 => Dim n
-- | Match Dim n against a concrete Nat
pattern D24 :: forall (n :: Nat). () => n ~ 24 => Dim n
-- | Match Dim n against a concrete Nat
pattern D25 :: forall (n :: Nat). () => n ~ 25 => Dim n
-- | Same as SomeNat
type SomeDim = Dim (XN 0)
-- | This class provides the Dim associated with a type-level
-- natural.
--
-- Note, kind of the KnownDim argument is usually Nat,
-- because it is impossible to create a unique KnownDim (XN m)
-- instance. Nevertheless, you can have KnownDim (N n), which is
-- useful in some cases.
class KnownDim n
-- | Get value of type-level dim at runtime.
--
-- Note, this function is supposed to be used with
-- TypeApplications. For example, you can type:
--
--
-- >>> :set -XTypeApplications
--
-- >>> :set -XDataKinds
--
-- >>> :t dim @3
-- dim @3 :: Dim 3
--
--
--
-- >>> :set -XTypeOperators
--
-- >>> :t dim @(13 - 6)
-- dim @(13 - 6) :: Dim 7
--
dim :: KnownDim n => Dim n
-- | If you have KnownDim d, then d can only be
-- Nat or a known type of XNat (i.e. N n).
-- This function assures the type checker that this is indeed the case.
withKnownXDim :: forall (d :: XNat) (rep :: RuntimeRep) (r :: TYPE rep). KnownDim d => ((KnownDim (DimBound d), ExactDim d, KnownDimType d, FixedDim d (DimBound d)) => r) -> r
-- | Get a minimal or exact bound of a Dim.
--
-- To satisfy the BoundedDim means to be equal to N n
-- or be not less than XN m.
class (KnownDimKind (KindOf d), KnownDimType d, KnownDim (DimBound d)) => BoundedDim d where {
-- | Minimal or exact bound of a Dim. Useful for indexing: it is
-- safe to index something by an index less than DimBound n (for
-- both Nat and Xnat indexed dims).
type family DimBound d :: Nat;
}
-- | Get such a minimal Dim (DimBound n), that Dim n is
-- guaranteed to be not less than dimBound if n ~ XN a,
-- otherwise, the return Dim is the same as n.
dimBound :: BoundedDim d => Dim (DimBound d)
-- | If the runtime value of Dim y satisfies dimBound
-- x, then coerce to Dim x. Otherwise, return
-- Nothing@.
--
-- To satisfy the dimBound means to be equal to N n or
-- be not less than XN m.
constrainDim :: forall y. BoundedDim d => Dim y -> Maybe (Dim d)
-- | Returns the minimal Dim that satisfies the
-- BoundedDim constraint (this is the exact dim for
-- Nats and the minimal bound for XNats).
minimalDim :: forall n. BoundedDim n => Dim n
-- | This is either Nat, or a known XNat (i.e. N
-- n).
type family ExactDim (d :: k) :: Constraint
-- | Constraints given by an XNat type on possible values of a Nat hidden
-- inside.
type family FixedDim (x :: XNat) (n :: Nat) :: Constraint
-- | Similar to natVal from TypeNats, but returns
-- Word.
dimVal :: forall x. Dim x -> Word
-- | Similar to natVal from TypeNats, but returns
-- Word.
dimVal' :: forall n. KnownDim n => Word
-- | Construct a Dim n if there is an instance of Typeable
-- n around.
--
-- Note: we can do this only for Nat-indexed dim, because the
-- type XN m does not have enough information to create a dim at
-- runtime.
typeableDim :: forall (n :: Nat). Typeable n => Dim n
-- | Similar to someNatVal from TypeNats.
someDimVal :: Word -> SomeDim
-- | We either get evidence that this function was instantiated with the
-- same type-level numbers, or Nothing.
--
-- Note, this function works on Nat-indexed dimensions only,
-- because Dim (XN x) does not have runtime evidence to infer
-- x and `KnownDim x` does not imply `KnownDim (XN x)`.
sameDim :: forall (x :: Nat) (y :: Nat). Dim x -> Dim y -> Maybe (Dict (x ~ y))
-- | We either get evidence that this function was instantiated with the
-- same type-level numbers, or Nothing.
sameDim' :: forall (x :: Nat) (y :: Nat). (KnownDim x, KnownDim y) => Maybe (Dict (x ~ y))
-- | We either get evidence that x is not greater than y,
-- or Nothing.
lessOrEqDim :: forall (x :: Nat) (y :: Nat). Dim x -> Dim y -> Maybe (Dict (x <= y))
-- | We either get evidence that x is not greater than y,
-- or Nothing.
lessOrEqDim' :: forall (x :: Nat) (y :: Nat). (KnownDim x, KnownDim y) => Maybe (Dict (x <= y))
-- | Ordering of dimension values.
--
-- Note: CmpNat forces type parameters to kind Nat; if you
-- want to compare unknown XNats, use Ord instance of
-- Dim.
compareDim :: forall (a :: Nat) (b :: Nat). Dim a -> Dim b -> SOrdering (CmpNat a b)
-- | Ordering of dimension values.
--
-- Note: CmpNat forces type parameters to kind Nat; if you
-- want to compare unknown XNats, use Ord instance of
-- Dim.
compareDim' :: forall (a :: Nat) (b :: Nat). (KnownDim a, KnownDim b) => SOrdering (CmpNat a b)
-- | constrainDim with explicitly-passed constraining Dim
-- to avoid AllowAmbiguousTypes.
constrainBy :: forall x p y. BoundedDim x => p x -> Dim y -> Maybe (Dim x)
-- | Decrease minimum allowed size of a Dim (XN x).
relax :: forall (m :: Nat) (n :: Nat). (<=) m n => Dim (XN n) -> Dim (XN m)
-- | Same as `Prelude.(+)`. Pattern-matching against the result would
-- produce the evindence KnownDim (n + m).
plusDim :: forall (n :: Nat) (m :: Nat). Dim n -> Dim m -> Dim (n + m)
-- | Same as `Prelude.(-)`. Pattern-matching against the result would
-- produce the evindence KnownDim (n - m).
minusDim :: forall (n :: Nat) (m :: Nat). (<=) m n => Dim n -> Dim m -> Dim (n - m)
-- | Similar to minusDim, but returns Nothing if the result
-- would be negative. Pattern-matching against the result would produce
-- the evindence KnownDim (n - m).
minusDimM :: forall (n :: Nat) (m :: Nat). Dim n -> Dim m -> Maybe (Dim (n - m))
-- | Same as `Prelude.(*)`. Pattern-matching against the result would
-- produce the evindence KnownDim (n * m).
timesDim :: forall (n :: Nat) (m :: Nat). Dim n -> Dim m -> Dim ((*) n m)
-- | Same as `Prelude.(^)`. Pattern-matching against the result would
-- produce the evindence KnownDim (n ^ m).
powerDim :: forall (n :: Nat) (m :: Nat). Dim n -> Dim m -> Dim ((^) n m)
-- | Same as div. Pattern-matching against the result would produce
-- the evindence KnownDim (Div n m).
divDim :: forall (n :: Nat) (m :: Nat). Dim n -> Dim m -> Dim (Div n m)
-- | Same as mod. Pattern-matching against the result would produce
-- the evindence KnownDim (Mod n m).
modDim :: forall (n :: Nat) (m :: Nat). Dim n -> Dim m -> Dim (Mod n m)
-- | Returns log base 2 (round down). Pattern-matching against the result
-- would produce the evindence KnownDim (Log2 n).
log2Dim :: forall (n :: Nat). Dim n -> Dim (Log2 n)
-- | Same as min. Pattern-matching against the result would produce
-- the evindence KnownDim (Min n m).
minDim :: forall (n :: Nat) (m :: Nat). Dim n -> Dim m -> Dim (Min n m)
-- | Same as max. Pattern-matching against the result would produce
-- the evindence KnownDim (Max n m).
maxDim :: forall (n :: Nat) (m :: Nat). Dim n -> Dim m -> Dim (Max n m)
-- | Comparison of type-level naturals, as a function.
type family CmpNat (a :: Nat) (b :: Nat) :: Ordering
-- | Singleton-style version of Ordering. Pattern-match againts its
-- constructor to witness the result of type-level comparison.
data SOrdering :: Ordering -> Type
[SLT] :: SOrdering 'LT
[SEQ] :: SOrdering 'EQ
[SGT] :: SOrdering 'GT
-- | Addition of type-level naturals.
type family (+) (a :: Nat) (b :: Nat) :: Nat
infixl 6 +
-- | Subtraction of type-level naturals.
type family (-) (a :: Nat) (b :: Nat) :: Nat
infixl 6 -
-- | Multiplication of type-level naturals.
type family (*) (a :: Nat) (b :: Nat) :: Nat
infixl 7 *
-- | Exponentiation of type-level naturals.
type family (^) (a :: Nat) (b :: Nat) :: Nat
infixr 8 ^
-- | Comparison of type-level naturals, as a constraint.
type (<=) (a :: Nat) (b :: Nat) = LE a b (CmpNat a b)
-- | Miminum among two type-level naturals.
type Min (a :: Nat) (b :: Nat) = Min' a b (CmpNat a b)
-- | Maximum among two type-level naturals.
type Max (a :: Nat) (b :: Nat) = Min' a b (CmpNat a b)
-- | Type-level dimensionality.
type Dims = (TypedList Dim :: [k] -> Type)
-- | Same as SomeNat, but for Dimensions: Hide all information about
-- Dimensions inside
data SomeDims
SomeDims :: Dims ns -> SomeDims
-- | Put runtime evidence of Dims value inside function constraints.
-- Similar to KnownDim or KnownNat, but for lists of
-- numbers.
--
-- Note, kind of the Dimensions list is usually Nat,
-- restricted by KnownDim being also Nat-indexed (it is
-- impossible to create a unique KnownDim (XN m) instance).
-- Nevertheless, you can have KnownDim (N n), which is useful in
-- some cases.
class Dimensions ds
-- | Get dimensionality of a space at runtime, represented as a list of
-- Dim.
--
-- Note, this function is supposed to be used with
-- TypeApplications. For example, you can type:
--
--
-- >>> :set -XTypeApplications
--
-- >>> :set -XDataKinds
--
-- >>> :t dims @'[17, 12]
-- dims @'[17, 12] :: Dims '[17, 12]
--
--
--
-- >>> :t dims @'[]
-- dims @'[] :: Dims '[]
--
--
--
-- >>> :t dims @(Tail '[3,2,5,7])
-- dims @(Tail '[3,2,5,7]) :: Dims '[2, 5, 7]
--
dims :: Dimensions ds => Dims ds
-- | If you have Dimensions ds, then ds can only be
-- [Nat] or a known type of [XNa]t (i.e. all N
-- n). This function assures the type checker that this is indeed
-- the case.
withKnownXDims :: forall (ds :: [XNat]) (rep :: RuntimeRep) (r :: TYPE rep). Dimensions ds => ((Dimensions (DimsBound ds), ExactDims ds, All KnownDimType ds, FixedDims ds (DimsBound ds)) => r) -> r
-- | Get a minimal or exact bound of Dims.
--
-- This is a plural form of BoundedDim.
--
-- BoundedDims is a somewhat weaker form of Dimensions:
--
--
-- - It is defined for both [Nat] and [XNat];
-- - Instance of Dimensions ds always implies BoundedDims
-- ds.
--
--
-- BoundedDims is a powerful inference tool: its instances do
-- not require much, but it provides a lot via the superclass
-- constraints.
class (KnownDimKind (KindOfEl ds), All BoundedDim ds, RepresentableList ds, Dimensions (DimsBound ds), BoundedDimsTail ds) => BoundedDims ds
-- | Plural form for dimBound
dimsBound :: BoundedDims ds => Dims (DimsBound ds)
-- | Plural form for constrainDim.
--
-- Given a Dims ys, test if its runtime value satisfies
-- constraints imposed by BoundedDims xs, and returns it back
-- coerced to Dims xs on success.
--
-- This function allows to guess safely individual dimension values, as
-- well as the length of the dimension list. It returns Nothing
-- if xs and ys have different length or if any of the
-- values in ys are less than the corresponding values of
-- xs.
constrainDims :: forall ys. BoundedDims ds => Dims ys -> Maybe (Dims ds)
-- | Minimal or exact bound of Dims. This is a plural form of
-- DimBound.
type family DimsBound (ds :: [k]) :: [Nat]
-- | Minimal runtime Dims ds value that satifies the constraints
-- imposed by the type signature of Dims ds (this is the exact
-- dims for Nats and the minimal bound for
-- XNats).
minimalDims :: forall ds. BoundedDims ds => Dims ds
-- | Every dim in a list is either Nat, or a known XNat
-- (i.e. N n).
type family ExactDims (d :: [k]) :: Constraint
-- | Constrain Nat dimensions hidden behind XNats. This
-- is a link connecting the two types of type-level dims; you often need
-- it to convert Dims, Idxs, and data.
type family FixedDims (xns :: [XNat]) (ns :: [Nat]) :: Constraint
-- | Try to instantiate the FixedDims constraint given two
-- Dims lists.
--
-- The first Dims is assumed to be the output of
-- minimalDims, i.e. listDims xns == toList (listDims
-- xns).
--
-- If you input a list that is not equal to its type-level
-- DimsBound, you will just have a lower chance to get Just
-- Dict result.
inferFixedDims :: forall (xns :: [XNat]) (ns :: [Nat]). All KnownDimType xns => Dims xns -> Dims ns -> Maybe (Dict (FixedDims xns ns))
-- | Infer FixedDims if you know that all of dims are exact (d ~
-- N n). This function is totally safe and faithful.
inferExactFixedDims :: forall (ds :: [XNat]). ExactDims ds => Dims (DimsBound ds) -> Dict (All KnownDimType ds, FixedDims ds (DimsBound ds))
-- | Type-indexed list
data TypedList (f :: (k -> Type)) (xs :: [k])
-- | O(1) Pattern-matching against this constructor brings a
-- Dimensions instance into the scope. Thus, you can do arbitrary
-- operations on your dims and use this pattern at any time to
-- reconstruct the class instance at runtime.
pattern Dims :: forall ds. KnownDimKind (KindOfEl ds) => (KindOfEl ds ~ Nat, Dimensions ds) => Dims ds
-- | O(n) Pattern-matching against this constructor reveals
-- Nat-kinded list of dims, pretending the dimensionality is known at
-- compile time within the scope of the pattern match. This is the main
-- recommended way to get Dims at runtime; for example, reading a
-- list of dimensions from a file.
pattern XDims :: forall ds. KnownDimKind (KindOfEl ds) => forall (ns :: [Nat]). (KindOfEl ds ~ XNat, FixedDims ds ns) => Dims ns -> Dims ds
-- | O(Length ds) A heavy weapon against all sorts of type errors
pattern KnownDims :: forall (ds :: [Nat]). () => (All KnownDim ds, All BoundedDim ds, RepresentableList ds, Dimensions ds) => Dims ds
-- | Zero-length type list
pattern U :: forall (k :: Type) (f :: k -> Type) (xs :: [k]). () => xs ~ '[] => TypedList f xs
-- | Constructing a type-indexed list
pattern (:*) :: forall f xs. () => forall y ys. xs ~ (y : ys) => f y -> TypedList f ys -> TypedList f xs
-- | Zero-length type list; synonym to U.
pattern Empty :: forall (k :: Type) (f :: k -> Type) (xs :: [k]). () => xs ~ '[] => TypedList f xs
-- | Pattern matching against this causes RepresentableList instance
-- come into scope. Also it allows constructing a term-level list out of
-- a constraint.
pattern TypeList :: forall xs. () => RepresentableList xs => TypeList xs
-- | Constructing a type-indexed list in the canonical way
pattern Cons :: forall f xs. () => forall y ys. xs ~ (y : ys) => f y -> TypedList f ys -> TypedList f xs
-- | Constructing a type-indexed list from the other end
pattern Snoc :: forall f xs. () => forall sy y. SnocList sy y xs => TypedList f sy -> f y -> TypedList f xs
-- | Reverse a typed list
pattern Reverse :: forall f xs. () => forall sx. ReverseList xs sx => TypedList f sx -> TypedList f xs
infixr 5 :*
-- | Construct a Dims ds if there is an instance of Typeable
-- ds around.
typeableDims :: forall (ds :: [Nat]). Typeable ds => Dims ds
-- | Dims (ds :: [Nat]) is always Typeable.
inferTypeableDims :: forall (ds :: [Nat]). Dims ds -> Dict (Typeable ds)
-- | O(1) Convert Dims xs to a plain haskell list of
-- dimension sizes.
--
-- Note, for XNat-indexed list it returns actual content
-- dimensions, not the constraint numbers (XN m)
listDims :: forall xs. Dims xs -> [Word]
-- | Convert a plain haskell list of dimension sizes into an unknown
-- type-level dimensionality O(1).
someDimsVal :: [Word] -> SomeDims
-- | Product of all dimension sizes O(Length xs).
totalDim :: forall xs. Dims xs -> Word
-- | Product of all dimension sizes O(Length xs).
totalDim' :: forall xs. Dimensions xs => Word
-- | We either get evidence that this function was instantiated with the
-- same type-level Dimensions, or Nothing O(Length xs).
sameDims :: forall (as :: [Nat]) (bs :: [Nat]). Dims as -> Dims bs -> Maybe (Dict (as ~ bs))
-- | We either get evidence that this function was instantiated with the
-- same type-level Dimensions, or Nothing O(Length xs).
sameDims' :: forall (as :: [Nat]) (bs :: [Nat]) (p :: [Nat] -> Type) (q :: [Nat] -> Type). (Dimensions as, Dimensions bs) => p as -> q bs -> Maybe (Dict (as ~ bs))
-- | Restricted version of const, similar to asProxyTypeOf;
-- to be used on such implicit functions as dims, dimsBound
-- etc.
inSpaceOf :: forall ds p q. p ds -> q ds -> p ds
-- | Drop the given prefix from a Dims list. It returns Nothing if the list
-- did not start with the prefix given, or Just the Dims after the
-- prefix, if it does.
stripPrefixDims :: forall (xs :: [Nat]) (ys :: [Nat]). Dims xs -> Dims ys -> Maybe (Dims (StripPrefix xs ys))
-- | Drop the given suffix from a Dims list. It returns Nothing if the list
-- did not end with the suffix given, or Just the Dims before the suffix,
-- if it does.
stripSuffixDims :: forall (xs :: [Nat]) (ys :: [Nat]). Dims xs -> Dims ys -> Maybe (Dims (StripSuffix xs ys))
-- | Representable type lists. Allows getting type information about list
-- structure at runtime.
class RepresentableList xs
-- | Get type-level constructed list
tList :: RepresentableList xs => TypeList xs
-- | A list of type proxies
type TypeList = (TypedList Proxy :: [k] -> Type)
-- | Get a constructible TypeList from any other TypedList;
-- Pattern matching agains the result brings RepresentableList
-- constraint into the scope:
--
--
-- case types ts of TypeList -> ...
--
types :: forall f xs. TypedList f xs -> TypeList xs
-- | Return the number of elements in a TypedList (same as
-- length).
order :: forall f xs. TypedList f xs -> Dim (Length xs)
-- | Return the number of elements in a type list xs bound by a
-- constraint RepresentableList xs (same as order, but
-- takes no value arguments).
order' :: forall xs. RepresentableList xs => Dim (Length xs)
-- | Get the kind of a given type. Useful when we don't want to introduce
-- another type parameter into a type signature (because the kind is
-- determined by the type), but need to have some constraints on the
-- type's kind.
type KindOf (t :: k) = k
-- | Get the kind of a given list type. Useful when we don't want to
-- introduce another type parameter into a type signature (because the
-- kind is determined by the type), but need to have some constraints on
-- the type's kind.
type KindOfEl (ts :: [k]) = k
instance Numeric.Dimensions.Dim.Dimensions ns => Numeric.Dimensions.Dim.BoundedDims ns
instance Numeric.Dimensions.Dim.BoundedDims '[]
instance (Numeric.Dimensions.Dim.BoundedDim n, Numeric.Dimensions.Dim.BoundedDims ns) => Numeric.Dimensions.Dim.BoundedDims (n : ns)
instance forall k (xs :: [k]). Numeric.Dimensions.Dim.BoundedDims xs => GHC.Read.Read (Numeric.Dimensions.Dim.Dims xs)
instance Numeric.Dimensions.Dim.Dimensions '[]
instance forall k (d :: k) (ds :: [k]). (Numeric.Dimensions.Dim.KnownDim d, Numeric.Dimensions.Dim.Dimensions ds) => Numeric.Dimensions.Dim.Dimensions (d : ds)
instance GHC.Classes.Eq Numeric.Dimensions.Dim.SomeDims
instance GHC.Classes.Ord Numeric.Dimensions.Dim.SomeDims
instance GHC.Show.Show Numeric.Dimensions.Dim.SomeDims
instance GHC.Read.Read Numeric.Dimensions.Dim.SomeDims
instance Numeric.Dimensions.Dim.KnownDim n => Numeric.Dimensions.Dim.BoundedDim n
instance Numeric.Dimensions.Dim.KnownDim n => Numeric.Dimensions.Dim.BoundedDim (Numeric.Dimensions.Dim.N n)
instance Numeric.Dimensions.Dim.KnownDim m => Numeric.Dimensions.Dim.BoundedDim (Numeric.Dimensions.Dim.XN m)
instance forall k (x :: k). Numeric.Dimensions.Dim.BoundedDim x => GHC.Read.Read (Numeric.Dimensions.Dim.Dim x)
instance GHC.TypeNats.KnownNat n => Numeric.Dimensions.Dim.KnownDim n
instance Numeric.Dimensions.Dim.KnownDim 0
instance Numeric.Dimensions.Dim.KnownDim 1
instance Numeric.Dimensions.Dim.KnownDim 2
instance Numeric.Dimensions.Dim.KnownDim 3
instance Numeric.Dimensions.Dim.KnownDim 4
instance Numeric.Dimensions.Dim.KnownDim 5
instance Numeric.Dimensions.Dim.KnownDim 6
instance Numeric.Dimensions.Dim.KnownDim 7
instance Numeric.Dimensions.Dim.KnownDim 8
instance Numeric.Dimensions.Dim.KnownDim 9
instance Numeric.Dimensions.Dim.KnownDim 10
instance Numeric.Dimensions.Dim.KnownDim 11
instance Numeric.Dimensions.Dim.KnownDim 12
instance Numeric.Dimensions.Dim.KnownDim 13
instance Numeric.Dimensions.Dim.KnownDim 14
instance Numeric.Dimensions.Dim.KnownDim 15
instance Numeric.Dimensions.Dim.KnownDim 16
instance Numeric.Dimensions.Dim.KnownDim 17
instance Numeric.Dimensions.Dim.KnownDim 18
instance Numeric.Dimensions.Dim.KnownDim 19
instance Numeric.Dimensions.Dim.KnownDim 20
instance Numeric.Dimensions.Dim.KnownDim 21
instance Numeric.Dimensions.Dim.KnownDim 22
instance Numeric.Dimensions.Dim.KnownDim 23
instance Numeric.Dimensions.Dim.KnownDim 24
instance Numeric.Dimensions.Dim.KnownDim 25
instance Numeric.Dimensions.Dim.KnownDim n => Numeric.Dimensions.Dim.KnownDim (Numeric.Dimensions.Dim.N n)
instance Data.Constraint.Class (GHC.TypeNats.KnownNat n) (Numeric.Dimensions.Dim.KnownDim n)
instance Numeric.Dimensions.Dim.KnownDim d => GHC.Generics.Generic (Numeric.Dimensions.Dim.Dim d)
instance GHC.Classes.Eq (Numeric.Dimensions.Dim.Dims ds)
instance GHC.Classes.Eq (Numeric.Dimensions.Dim.Dims ds)
instance GHC.Classes.Ord (Numeric.Dimensions.Dim.Dims ds)
instance GHC.Classes.Ord (Numeric.Dimensions.Dim.Dims ds)
instance forall k (xs :: [k]). GHC.Show.Show (Numeric.Dimensions.Dim.Dims xs)
instance Data.Typeable.Internal.Typeable d => Data.Data.Data (Numeric.Dimensions.Dim.Dim d)
instance GHC.Classes.Eq (Numeric.Dimensions.Dim.Dim n)
instance GHC.Classes.Eq (Numeric.Dimensions.Dim.Dim x)
instance GHC.Classes.Ord (Numeric.Dimensions.Dim.Dim n)
instance GHC.Classes.Ord (Numeric.Dimensions.Dim.Dim x)
instance forall k (x :: k). GHC.Show.Show (Numeric.Dimensions.Dim.Dim x)
instance Numeric.Dimensions.Dim.KnownDimKind GHC.Types.Nat
instance Numeric.Dimensions.Dim.KnownDimKind Numeric.Dimensions.Dim.XNat
instance forall k (n :: k). Data.Constraint.Class (Numeric.Dimensions.Dim.KnownDimKind k) (Numeric.Dimensions.Dim.KnownDimType n)
instance Numeric.Dimensions.Dim.KnownDimType n
instance Numeric.Dimensions.Dim.KnownDimType ('Numeric.Dimensions.Dim.N n)
instance Numeric.Dimensions.Dim.KnownDimType ('Numeric.Dimensions.Dim.XN n)
-- | Provides a data type Idx to index Dim and Idxs
-- that enumerates through multiple dimensions.
--
-- 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.
--
-- Type safety
--
-- Same as Dim and Dims, Idx and Idxs defined
-- in this module incorporate two different indexing mechanics. Both of
-- them can be specified with exact Nat values (when d ::
-- Nat or d ~ N n), or with lower bound values (i.e. d
-- ~ XN m). In the former case, the Idx/Idxs type
-- itself guarantees that the value inside is within the
-- Dim/Dims bounds. In the latter case,
-- Idx/Idxs can contain any values of type
-- Word. In other words:
--
--
-- - (d :: Nat) || (d ~ N n) => using Idx d to
-- index data is always safe, but creating an index using unsafe
-- functions can yield an OutOfDimBounds exception at
-- runtime.
-- - (d ~ XN m) => using Idx d to index data can
-- result in an OutOfDimBounds exception, but you can safely
-- manipulate the index itself using familiar interfaces, such as
-- Enum, Num, etc; as if Idx d was a plain
-- synonym to Word.
--
module Numeric.Dimensions.Idx
-- | This type is used to index a single dimension.
--
--
-- - (k ~ Nat) => the range of indices is from 0
-- to d-1.
-- - (d ~ N n) => the range of indices is from 0
-- to n-1.
-- - (d ~ XN m) => the range of indices is from 0
-- to maxBound :: Word.
--
--
-- That is, using Idx (n :: Nat) or Idx (N n) is
-- guaranteed to be safe by the type system. But an index of type Idx
-- (XN m) can have any value, and using it may yield an
-- OutOfDimBounds exception -- just the same as a generic
-- index function that takes a plain Int or
-- Word as an argument. Thus, if you have data indexed by
-- (XN m), I would suggest to use lookup-like functions
-- that return Maybe. You're warned.
data Idx (d :: k)
-- | Convert between Word and Idx.
--
-- Converting from Idx to Word is always safe.
--
-- Converting from Word to Idx generally is unsafe:
--
--
-- - (k ~ Nat) => if w >= d, it fails with an
-- OutOfDimBounds exception.
-- - (d ~ N n) => if w >= n, it fails with an
-- OutOfDimBounds exception.
-- - (d ~ XN m) => the constructor always succeeds, but
-- using the result for indexing may fail with an OutOfDimBounds
-- exception later.
--
--
-- If unsafeindices flag it turned on, this function always
-- succeeds.
pattern Idx :: forall d. BoundedDim d => Word -> Idx d
-- | Type-level dimensional indexing with arbitrary Word values inside.
-- Most of the operations on it require Dimensions or
-- BoundedDims constraint, because the Idxs itself does
-- not store info about dimension bounds.
type Idxs = (TypedList Idx :: [k] -> Type)
-- | Convert an arbitrary Word to Idx. This is a safe alternative
-- to the pattern Idx.
--
-- Note, when (d ~ XN m), it returns Nothing if w
-- >= m. Thus, the resulting index is always safe to use (but you
-- cannot index stuff beyond DimBound d this way).
idxFromWord :: forall d. BoundedDim d => Word -> Maybe (Idx d)
-- | Get the value of an Idx.
idxToWord :: forall d. Idx d -> Word
-- | O(1) Convert Idxs xs to a plain list of words.
listIdxs :: forall ds. Idxs ds -> [Word]
-- | O(n) Convert a plain list of words into an Idxs, while
-- checking the index bounds.
--
-- Same as with idxFromWord, it is always safe to use the
-- resulting index, but you cannot index stuff outside of the
-- DimsBound ds this way.
idxsFromWords :: forall ds. BoundedDims ds => [Word] -> Maybe (Idxs ds)
-- | O(1) Coerce a Nat-indexed list of indices into a
-- XNat-indexed one. This function does not need any runtime
-- checks and thus runs in constant time.
liftIdxs :: forall (ds :: [XNat]) (ns :: [Nat]). FixedDims ds ns => Idxs ns -> Idxs ds
-- | O(n) Coerce a XNat-indexed list of indices into a
-- Nat-indexed one. This function checks if an index is within
-- Dim bounds for every dimension.
unliftIdxs :: forall (ds :: [XNat]) (ns :: [Nat]). (FixedDims ds ns, Dimensions ns) => Idxs ds -> Maybe (Idxs ns)
-- | Coerce a XNat-indexed list of indices into a
-- Nat-indexed one. Can throw an OutOfDimBounds exception
-- unless unsafeindices flag is active.
unsafeUnliftIdxs :: forall (ds :: [XNat]) (ns :: [Nat]). (FixedDims ds ns, Dimensions ns) => Idxs ds -> Idxs ns
-- | Type-indexed list
data TypedList (f :: (k -> Type)) (xs :: [k])
-- | Transform between Nat-indexed and XNat-indexed
-- Idxs.
--
-- Note, this pattern is not a COMPLETE match, because
-- converting from XNat to Nat indexed Idxs
-- may fail (see unliftIdxs).
pattern XIdxs :: forall (ds :: [XNat]) (ns :: [Nat]). (FixedDims ds ns, Dimensions ns) => Idxs ns -> Idxs ds
-- | Zero-length type list
pattern U :: forall (k :: Type) (f :: k -> Type) (xs :: [k]). () => xs ~ '[] => TypedList f xs
-- | Constructing a type-indexed list
pattern (:*) :: forall f xs. () => forall y ys. xs ~ (y : ys) => f y -> TypedList f ys -> TypedList f xs
-- | Zero-length type list; synonym to U.
pattern Empty :: forall (k :: Type) (f :: k -> Type) (xs :: [k]). () => xs ~ '[] => TypedList f xs
-- | Constructing a type-indexed list in the canonical way
pattern Cons :: forall f xs. () => forall y ys. xs ~ (y : ys) => f y -> TypedList f ys -> TypedList f xs
-- | Constructing a type-indexed list from the other end
pattern Snoc :: forall f xs. () => forall sy y. SnocList sy y xs => TypedList f sy -> f y -> TypedList f xs
-- | Reverse a typed list
pattern Reverse :: forall f xs. () => forall sx. ReverseList xs sx => TypedList f sx -> TypedList f xs
infixr 5 :*
-- | Typically, this exception can occur in the following cases:
--
--
-- - Converting from integral values to Idx d when d ~ N
-- n or d :: Nat.
-- - Using Enum and Num when d ~ N n or
-- d :: Nat.
-- - Converting from Idx (XN m :: XNat) to Idx (n ::
-- Nat).
-- - Indexing or slicing data using Idx (XN m :: XNat).
--
--
-- If you are mad and want to avoid any overhead related to bounds
-- checking and the related error handling, you can turn on the
-- unsafeindices flag to remove all of this from the library at
-- once.
data OutOfDimBounds
OutOfDimBounds :: Integer -> Word -> Maybe Word -> Maybe ([Word], [Word]) -> String -> Maybe CallStack -> OutOfDimBounds
-- | A value that should have been a valid Idx
[oodIdx] :: OutOfDimBounds -> Integer
-- | A runtime value of a Dim
[oodDim] :: OutOfDimBounds -> Word
-- | When used for slicing, this should have satisfied oodIdx +
-- oodSubDim <= oodDim.
[oodSubDim] :: OutOfDimBounds -> Maybe Word
-- | If available, contains (Dims xns, Idxs xns).
[oodDimsCtx] :: OutOfDimBounds -> Maybe ([Word], [Word])
-- | Short description of the error location, typically a function name.
[oodName] :: OutOfDimBounds -> String
-- | Function call stack, if available. Note, this field is ignored in the
-- Eq and Ord instances.
[oodCallStack] :: OutOfDimBounds -> Maybe CallStack
-- | Throw an OutOfDimBounds exception.
outOfDimBounds :: (HasCallStack, Integral i) => String -> i -> Word -> Maybe Word -> Maybe ([Word], [Word]) -> a
-- | Throw an OutOfDimBounds exception without the CallStack
-- attached.
outOfDimBoundsNoCallStack :: Integral i => String -> i -> Word -> Maybe Word -> Maybe ([Word], [Word]) -> a
instance forall k (d :: k). GHC.Classes.Ord (Numeric.Dimensions.Idx.Idx d)
instance forall k (d :: k). GHC.Classes.Eq (Numeric.Dimensions.Idx.Idx d)
instance forall k (d :: k). Foreign.Storable.Storable (Numeric.Dimensions.Idx.Idx d)
instance forall k (d :: k). GHC.Generics.Generic (Numeric.Dimensions.Idx.Idx d)
instance forall k (d :: k). (Data.Typeable.Internal.Typeable d, Data.Typeable.Internal.Typeable k) => Data.Data.Data (Numeric.Dimensions.Idx.Idx d)
instance forall k (d :: k). Numeric.Dimensions.Dim.BoundedDim d => GHC.Enum.Enum (Numeric.Dimensions.Idx.Idx d)
instance forall k (d :: k). Numeric.Dimensions.Dim.BoundedDim d => GHC.Real.Integral (Numeric.Dimensions.Idx.Idx d)
instance forall k (d :: k). Numeric.Dimensions.Dim.BoundedDim d => GHC.Real.Real (Numeric.Dimensions.Idx.Idx d)
instance forall k (d :: k). Numeric.Dimensions.Dim.BoundedDim d => GHC.Num.Num (Numeric.Dimensions.Idx.Idx d)
instance GHC.Classes.Eq Numeric.Dimensions.Idx.OutOfDimBounds
instance GHC.Classes.Ord Numeric.Dimensions.Idx.OutOfDimBounds
instance GHC.Show.Show Numeric.Dimensions.Idx.OutOfDimBounds
instance GHC.Exception.Type.Exception Numeric.Dimensions.Idx.OutOfDimBounds
instance forall k (xs :: [k]). GHC.Classes.Eq (Numeric.Dimensions.Idx.Idxs xs)
instance forall k (xs :: [k]). GHC.Classes.Ord (Numeric.Dimensions.Idx.Idxs xs)
instance forall k (xs :: [k]). GHC.Show.Show (Numeric.Dimensions.Idx.Idxs xs)
instance forall k (xs :: [k]). Numeric.Dimensions.Dim.BoundedDims xs => GHC.Read.Read (Numeric.Dimensions.Idx.Idxs xs)
instance forall k (ds :: [k]). Numeric.Dimensions.Dim.BoundedDims ds => GHC.Enum.Bounded (Numeric.Dimensions.Idx.Idxs ds)
instance forall k (ds :: [k]). Numeric.Dimensions.Dim.Dimensions ds => GHC.Enum.Enum (Numeric.Dimensions.Idx.Idxs ds)
instance forall k (d :: k). Numeric.Dimensions.Dim.BoundedDim d => GHC.Read.Read (Numeric.Dimensions.Idx.Idx d)
instance forall k (d :: k). GHC.Show.Show (Numeric.Dimensions.Idx.Idx d)
instance forall k (d :: k). Numeric.Dimensions.Dim.BoundedDim d => GHC.Enum.Bounded (Numeric.Dimensions.Idx.Idx d)
instance Numeric.Dimensions.Dim.KnownDim n => GHC.Enum.Enum (Numeric.Dimensions.Idx.Idx n)
instance Numeric.Dimensions.Dim.KnownDim n => GHC.Num.Num (Numeric.Dimensions.Idx.Idx n)
-- | 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.
module Numeric.Dimensions
-- | 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.
mapDict :: () => (a :- b) -> Dict a -> Dict b
-- | Operator version of withDict, with the arguments flipped
(\\) :: HasDict c e => (c -> r) -> e -> r
infixl 1 \\
-- | 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.
data Dict a
[Dict] :: forall a. a => Dict a
-- | 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.
newtype (:-) a b
Sub :: (a -> Dict b) -> (:-) a b
infixr 9 :-