-- 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.0.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
-- | 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
-- | 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 = '[]
-- | Appending a list, represents an Op counterpart of
-- (':).
type Cons (a :: k) (as :: [k]) = a : as
-- | Appending a list on the other side.
type family Snoc (xs :: [k]) (x :: k) = (ys :: [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]) :: [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]
-- | Returns the elements of a list in reverse order.
type family Reverse (xs :: [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]
-- | Check if an item is a member of a list.
type family Elem (x :: k) (xs :: [k]) :: Constraint
-- | Represent a triple of lists forming a relation (as ++ bs) ~
-- asbs
type ConcatList (as :: [k]) (bs :: [k]) (asbs :: [k]) = (asbs ~ Concat as bs, as ~ StripSuffix bs asbs, bs ~ StripPrefix as asbs)
-- | Derive ConcatList given StripSuffix
evStripSuffix :: forall (k :: Type) (as :: [k]) (bs :: [k]) (asbs :: [k]). (as ~ StripSuffix bs asbs) :- ConcatList as bs asbs
-- | Derive ConcatList given StripPrefix
evStripPrefix :: forall (k :: Type) (as :: [k]) (bs :: [k]) (asbs :: [k]). (bs ~ StripPrefix as asbs) :- ConcatList as bs asbs
-- | Derive ConcatList given Concat
evConcat :: forall (k :: Type) (as :: [k]) (bs :: [k]) (asbs :: [k]). (asbs ~ Concat as bs) :- ConcatList as bs asbs
-- | Given a Typeable list, infer this constraint for its parts.
inferTypeableCons :: forall (k :: Type) (ys :: [k]) (x :: k) (xs :: [k]). (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 (k :: Type) (f :: k -> Type) (xs :: [k]). () => forall (y :: k) (ys :: [k]). 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 (k :: Type) (xs :: [k]). () => 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 (k :: Type) (c :: k -> Constraint) (xs :: [k]). () => (All c xs, RepresentableList xs) => DictList c xs
-- | Constructing a type-indexed list in the canonical way
pattern Cons :: forall (k :: Type) (f :: k -> Type) (xs :: [k]). () => forall (y :: k) (ys :: [k]). xs ~ (y : ys) => f y -> TypedList f ys -> TypedList f xs
-- | Constructing a type-indexed list from the other end
pattern Snoc :: forall (k :: Type) (f :: k -> Type) (xs :: [k]). () => forall (sy :: [k]) (y :: k). xs ~ (sy +: y) => TypedList f sy -> f y -> TypedList f xs
-- | Reverse a typed list
pattern Reverse :: forall (k :: Type) (f :: k -> Type) (xs :: [k]). () => forall (sx :: [k]). (xs ~ Reverse sx, sx ~ Reverse xs) => TypedList f sx -> TypedList f xs
infixr 5 :*
-- | Representable type lists. Allows getting type information about list
-- structure at runtime.
class RepresentableList (xs :: [k])
-- | 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) (xs :: [k]) = TypedList (Dict1 c) xs
-- | A list of type proxies
type TypeList (xs :: [k]) = TypedList Proxy xs
-- | 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 (k :: Type) (f :: k -> Type) (xs :: [k]). 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 (k :: Type) (xs :: [k]). Typeable xs => TypeList xs
-- | If all elements of a TypedList are Typeable, then
-- the list of these elements is also Typeable.
inferTypeableList :: forall (k :: Type) (f :: k -> Type) (xs :: [k]). (Typeable k, All Typeable xs) => TypedList f xs -> Dict (Typeable xs)
order :: forall (k :: Type) (f :: k -> Type) (xs :: [k]). TypedList f xs -> Dim (Length xs)
order' :: forall (k :: Type) (xs :: [k]). RepresentableList xs => Dim (Length xs)
cons :: forall (k :: Type) (f :: k -> Type) (x :: k) (xs :: [k]). f x -> TypedList f xs -> TypedList f (x :+ xs)
snoc :: forall (k :: Type) (f :: k -> Type) (xs :: [k]) (x :: k). TypedList f xs -> f x -> TypedList f (xs +: x)
reverse :: forall (k :: Type) (f :: k -> Type) (xs :: [k]). TypedList f xs -> TypedList f (Reverse xs)
take :: forall (k :: Type) (n :: Nat) (f :: k -> Type) (xs :: [k]). Dim n -> TypedList f xs -> TypedList f (Take n xs)
drop :: forall (k :: Type) (n :: Nat) (f :: k -> Type) (xs :: [k]). Dim n -> TypedList f xs -> TypedList f (Drop n xs)
head :: forall (k :: Type) (f :: k -> Type) (xs :: [k]). TypedList f xs -> f (Head xs)
tail :: forall (k :: Type) (f :: k -> Type) (xs :: [k]). TypedList f xs -> TypedList f (Tail xs)
last :: forall (k :: Type) (f :: k -> Type) (xs :: [k]). TypedList f xs -> f (Last xs)
init :: forall (k :: Type) (f :: k -> Type) (xs :: [k]). TypedList f xs -> TypedList f (Init xs)
splitAt :: forall (k :: Type) (n :: Nat) (f :: k -> Type) (xs :: [k]). Dim n -> TypedList f xs -> (TypedList f (Take n xs), TypedList f (Drop n xs))
stripPrefix :: forall (k :: Type) (f :: k -> Type) (xs :: [k]) (ys :: [k]). (All Typeable xs, All Typeable ys, All Eq (Map f xs)) => TypedList f xs -> TypedList f ys -> Maybe (TypedList f (StripPrefix xs ys))
stripSuffix :: forall (k :: Type) (f :: k -> Type) (xs :: [k]) (ys :: [k]). (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 (k :: Type) (f :: k -> Type) (xs :: [k]) (ys :: [k]). (All Typeable xs, All Typeable ys, All Eq (Map f xs)) => TypedList f xs -> TypedList f ys -> Maybe (xs :~: ys, Bool)
concat :: forall (k :: Type) (f :: k -> Type) (xs :: [k]) (ys :: [k]). TypedList f xs -> TypedList f ys -> TypedList f (xs ++ ys)
length :: forall (k :: Type) (f :: k -> Type) (xs :: [k]). TypedList f xs -> Dim (Length xs)
-- | Map a function over contents of a typed list
map :: forall (k :: Type) (f :: k -> Type) (g :: k -> Type) (xs :: [k]). (forall (a :: k). f a -> g a) -> TypedList f xs -> TypedList g xs
-- | Generic show function for a TypedList.
typedListShowsPrecC :: forall (k :: Type) (c :: k -> Constraint) (f :: k -> Type) (xs :: [k]). All c xs => String -> (forall (x :: k). c x => Int -> f x -> ShowS) -> Int -> TypedList f xs -> ShowS
-- | Generic show function for a TypedList.
typedListShowsPrec :: forall (k :: Type) (f :: k -> Type) (xs :: [k]). (forall (x :: k). 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 (k :: Type) (c :: k -> Constraint) (f :: k -> Type) (xs :: [k]) (g :: k -> Type). All c xs => String -> (forall (x :: k). c x => ReadPrec (f x)) -> TypedList g xs -> ReadPrec (TypedList f xs)
-- | Generic read function for a TypedList of unknown length.
withTypedListReadPrec :: forall (k :: Type) (f :: k -> Type) (r :: Type). (forall (z :: Type). (forall (x :: k). f x -> z) -> ReadPrec z) -> (forall (xs :: [k]). 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 (xs :: [Type]) = TypedList Id xs
-- | 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 (k :: Type) (f :: k -> Type) (xs :: [k]). () => forall (y :: k) (ys :: [k]). 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 (k :: Type) (xs :: [k]). () => RepresentableList xs => TypeList xs
-- | Constructing a type-indexed list in the canonical way
pattern Cons :: forall (k :: Type) (f :: k -> Type) (xs :: [k]). () => forall (y :: k) (ys :: [k]). xs ~ (y : ys) => f y -> TypedList f ys -> TypedList f xs
-- | Constructing a type-indexed list from the other end
pattern Snoc :: forall (k :: Type) (f :: k -> Type) (xs :: [k]). () => forall (sy :: [k]) (y :: k). xs ~ (sy +: y) => TypedList f sy -> f y -> TypedList f xs
-- | Reverse a typed list
pattern Reverse :: forall (k :: Type) (f :: k -> Type) (xs :: [k]). () => forall (sx :: [k]). (xs ~ Reverse sx, sx ~ Reverse xs) => 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 (xs :: [Type]) = TypedList Id xs
-- | 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 (k :: Type) (f :: k -> Type) (xs :: [k]). () => forall (y :: k) (ys :: [k]). 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 (k :: Type) (xs :: [k]). () => RepresentableList xs => TypeList xs
-- | Constructing a type-indexed list in the canonical way
pattern Cons :: forall (k :: Type) (f :: k -> Type) (xs :: [k]). () => forall (y :: k) (ys :: [k]). xs ~ (y : ys) => f y -> TypedList f ys -> TypedList f xs
-- | Constructing a type-indexed list from the other end
pattern Snoc :: forall (k :: Type) (f :: k -> Type) (xs :: [k]). () => forall (sy :: [k]) (y :: k). xs ~ (sy +: y) => TypedList f sy -> f y -> TypedList f xs
-- | Reverse a typed list
pattern Reverse :: forall (k :: Type) (f :: k -> Type) (xs :: [k]). () => forall (sx :: [k]). (xs ~ Reverse sx, sx ~ Reverse xs) => 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
toStrict :: Tuple xs -> Tuple xs
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
-- | 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 (n :: Nat) = 'XN n
-- | Known natural number
type N (n :: Nat) = 'N n
-- | Find out whether XNat is of known or constrained type.
data XNatType :: XNat -> Type
-- | Given XNat is known
[Nt] :: XNatType ( 'N n)
-- | Given XNat is constrained unknown
[XNt] :: XNatType ( 'XN m)
-- | 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 (n :: Nat). () => KnownDim n => Dim n
-- | Statically known XNat
pattern Dn :: forall (xn :: XNat). KnownXNatType xn => forall (n :: Nat). (KnownDim n, xn ~ 'N n) => Dim n -> Dim xn
-- | 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 (xn :: XNat). KnownXNatType xn => forall (n :: Nat) (m :: Nat). (KnownDim n, m <= n, xn ~ 'XN m) => Dim n -> Dim xn
-- | 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 always Nat,
-- because it is impossible to create a unique KnownDim (XN m)
-- instance.
class KnownDim (n :: Nat)
-- | 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
-- | 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 k => BoundedDim (n :: k) 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 n :: 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 n => Dim (DimBound n)
-- | If the runtime value of Dim y satisfies dimBound k
-- 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 (l :: Type) (y :: l). BoundedDim n => Dim y -> Maybe (Dim n)
minDim :: forall (k :: Type) (d :: k). BoundedDim d => Dim d
-- | Find out the type of XNat constructor
class KnownXNatType (n :: XNat)
-- | Pattern-match against this to out the type of XNat constructor
xNatType :: KnownXNatType n => XNatType n
-- | 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 (k :: Type) (x :: k). Dim (x :: k) -> Word
-- | Similar to natVal from TypeNats, but returns
-- Word.
dimVal' :: forall (n :: Nat). KnownDim n => Word
-- | Construct a Dim n if there is an instance of Typeable
-- n around.
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) (p :: Nat -> Type) (q :: Nat -> Type). (KnownDim x, KnownDim y) => p x -> q 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) (p :: Nat -> Type) (q :: Nat -> Type). (KnownDim a, KnownDim b) => p a -> q b -> SOrdering (CmpNat a b)
-- | constrainDim with explicitly-passed constraining Dim
-- to avoid AllowAmbiguousTypes.
constrainBy :: forall (k :: Type) (x :: k) (p :: k -> Type) (l :: Type) (y :: l). 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)
plusDim :: forall (n :: Nat) (m :: Nat). Dim n -> Dim m -> Dim (n + m)
minusDim :: forall (n :: Nat) (m :: Nat). (<=) m n => Dim n -> Dim m -> Dim (n - m)
minusDimM :: forall (n :: Nat) (m :: Nat). Dim n -> Dim m -> Maybe (Dim (n - m))
timesDim :: forall (n :: Nat) (m :: Nat). Dim n -> Dim m -> Dim ((*) n m)
powerDim :: forall (n :: Nat) (m :: Nat). Dim n -> Dim m -> Dim ((^) n m)
divDim :: forall (n :: Nat) (m :: Nat). Dim n -> Dim m -> Dim (Div n m)
modDim :: forall (n :: Nat) (m :: Nat). Dim n -> Dim m -> Dim (Mod n m)
log2Dim :: forall (n :: Nat). Dim n -> Dim (Log2 n)
-- | (Kind) This is the kind of type-level natural numbers.
data Nat
-- | 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)
-- | Figure out whether the type-level dimension is Nat or
-- XNat. Useful for generalized inference functions.
class KnownDimKind (k :: Type)
dimKind :: KnownDimKind k => DimKind k
-- | GADT to support KnownDimKind type class. Match against its
-- constructors to know if k is Nat or XNat
data DimKind :: Type -> Type
-- | Working on Nat.
[DimNat] :: DimKind Nat
-- | Working on XNat.
[DimXNat] :: DimKind XNat
-- | Type-level dimensionality.
type Dims (xs :: [k]) = TypedList Dim xs
-- | 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 always Nat,
-- restricted by KnownDim being also Nat-indexed (it is
-- impossible to create a unique KnownDim (XN m) instance).
class Dimensions (ds :: [Nat])
-- | 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
-- | 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.
--
class KnownDimKind k => BoundedDims (ds :: [k]) where {
-- | Minimal or exact bound of Dims. This is a plural form of
-- DimBound.
type family DimsBound ds :: [Nat];
}
-- | 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 ds, and returns it back
-- coerced to Dims ds on success.
--
-- This function allows to guess safely individual dimension values, as
-- well as the length of the dimension list. It returns Nothing
-- if ds and xds have different length or if any of the
-- values in ys are less than the corresponding values of
-- ds.
constrainDims :: forall (l :: Type) (ys :: [l]). BoundedDims ds => Dims ys -> Maybe (Dims ds)
-- | BoundedDims means every element dim is BoundedDim and also
-- the length of a dim list is known.
--
-- Enforcing this as a superclass would complicate instance relations, so
-- it is better to provide these dictionaries on-demand.
inferAllBoundedDims :: BoundedDims ds => Dict (All BoundedDim ds, RepresentableList ds)
-- | Minimal runtime Dims ds value that satifies the constraints
-- imposed by the type signature of Dims ds.
minDims :: forall (k :: Type) (ds :: [k]). BoundedDims ds => Dims 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 :: [Nat]). () => Dimensions ds => Dims ds
-- | 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.
--
-- In order to use this pattern, one must know XNat type
-- constructors in each dimension at compile time.
pattern XDims :: forall (xns :: [XNat]). KnownXNatTypes xns => forall (ns :: [Nat]). (FixedDims xns ns, Dimensions ns) => Dims ns -> Dims xns
-- | An easy way to convert Nat-indexed dims into XNat-indexed dims.
pattern AsXDims :: forall (ns :: [Nat]). () => (KnownXNatTypes (AsXDims ns), RepresentableList (AsXDims ns)) => Dims (AsXDims ns) -> Dims ns
-- | 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 (k :: Type) (f :: k -> Type) (xs :: [k]). () => forall (y :: k) (ys :: [k]). 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 (k :: Type) (xs :: [k]). () => RepresentableList xs => TypeList xs
-- | Constructing a type-indexed list in the canonical way
pattern Cons :: forall (k :: Type) (f :: k -> Type) (xs :: [k]). () => forall (y :: k) (ys :: [k]). xs ~ (y : ys) => f y -> TypedList f ys -> TypedList f xs
-- | Constructing a type-indexed list from the other end
pattern Snoc :: forall (k :: Type) (f :: k -> Type) (xs :: [k]). () => forall (sy :: [k]) (y :: k). xs ~ (sy +: y) => TypedList f sy -> f y -> TypedList f xs
-- | Reverse a typed list
pattern Reverse :: forall (k :: Type) (f :: k -> Type) (xs :: [k]). () => forall (sx :: [k]). (xs ~ Reverse sx, sx ~ Reverse xs) => 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)
-- | Convert `Dims xs` to a plain haskell list of dimension sizes
-- O(1).
--
-- Note, for XNat-indexed list it returns actual content
-- dimensions, not the constraint numbers (XN m)
listDims :: forall (k :: Type) (xs :: [k]). 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 (k :: Type) (xs :: [k]). Dims xs -> Word
-- | Product of all dimension sizes O(Length xs).
totalDim' :: forall (xs :: [Nat]). 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))
-- | Similar to const or asProxyTypeOf; to be used on such
-- implicit functions as dim, dimMax, etc.
inSpaceOf :: forall (k :: Type) (ds :: [k]) (p :: [k] -> Type) (q :: [k] -> Type). p ds -> q ds -> p ds
-- | Similar to asProxyTypeOf, Give a hint to type checker to fix
-- the type of a function argument.
asSpaceOf :: forall (k :: Type) (ds :: [k]) (p :: [k] -> Type) (q :: [k] -> Type) (r :: Type). p ds -> (q ds -> r) -> q ds -> r
-- | Get XNat-indexed dims given their fixed counterpart.
xDims :: forall (xns :: [XNat]) (ns :: [Nat]). FixedDims xns ns => Dims ns -> Dims xns
-- | Get XNat-indexed dims given their fixed counterpart.
xDims' :: forall (xns :: [XNat]) (ns :: [Nat]). (FixedDims xns ns, Dimensions ns) => Dims xns
-- | 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))
-- | Map Dims onto XDims (injective)
type family AsXDims (ns :: [Nat]) = (xns :: [XNat]) | xns -> ns
-- | Map XDims onto Dims (injective)
type family AsDims (xns :: [XNat]) = (ns :: [Nat]) | ns -> xns
-- | Constrain Nat dimensions hidden behind XNats.
type family FixedDims (xns :: [XNat]) (ns :: [Nat]) :: Constraint
-- | Know the structure of each dimension
type KnownXNatTypes xns = All KnownXNatType xns
-- | Representable type lists. Allows getting type information about list
-- structure at runtime.
class RepresentableList (xs :: [k])
-- | Get type-level constructed list
tList :: RepresentableList xs => TypeList xs
-- | A list of type proxies
type TypeList (xs :: [k]) = TypedList Proxy xs
-- | 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 (k :: Type) (f :: k -> Type) (xs :: [k]). TypedList f xs -> TypeList xs
order :: forall (k :: Type) (f :: k -> Type) (xs :: [k]). TypedList f xs -> Dim (Length xs)
order' :: forall (k :: Type) (xs :: [k]). RepresentableList xs => Dim (Length xs)
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 (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 Numeric.Dimensions.Dim.KnownDimKind GHC.Types.Nat
instance Numeric.Dimensions.Dim.KnownDimKind Numeric.Dimensions.Dim.XNat
instance Numeric.Dimensions.Dim.KnownXNatType ('Numeric.Dimensions.Dim.N n)
instance Numeric.Dimensions.Dim.KnownXNatType ('Numeric.Dimensions.Dim.XN n)
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 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)
-- | 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.
module Numeric.Dimensions.Idx
-- | This type is used to index a single dimension; the range of indices is
-- from 0 to n-1.
data Idx (n :: k)
-- | Convert between Word and Idx.
--
-- If the word is outside of the bounds, fails with an error (unless
-- unsafeindices flag is turned on).
pattern Idx :: forall (k :: Type) (n :: k). BoundedDim n => Word -> Idx n
-- | Type-level dimensional indexing with arbitrary Word values inside.
-- Most of the operations on it require Dimensions constraint,
-- because the Idxs itself does not store info about dimension
-- bounds.
type Idxs (xs :: [k]) = TypedList Idx xs
-- | Convert an arbitrary Word to Idx.
idxFromWord :: forall (k :: Type) (d :: k). BoundedDim d => Word -> Maybe (Idx d)
-- | Convert an arbitrary Word to Idx.
--
-- If the word is outside of the bounds, fails with an error (unless
-- unsafeindices flag is turned on).
unsafeIdxFromWord :: forall (k :: Type) (d :: k). BoundedDim d => Word -> Idx d
-- | Get the value of an Idx.
idxToWord :: forall (k :: Type) (d :: k). Idx d -> Word
listIdxs :: forall (k :: Type) (xs :: [k]). Idxs xs -> [Word]
idxsFromWords :: forall (k :: Type) (xs :: [k]). BoundedDims xs => [Word] -> Maybe (Idxs xs)
instance forall k (n :: k). GHC.Classes.Ord (Numeric.Dimensions.Idx.Idx n)
instance forall k (n :: k). GHC.Classes.Eq (Numeric.Dimensions.Idx.Idx n)
instance forall k (n :: k). Foreign.Storable.Storable (Numeric.Dimensions.Idx.Idx n)
instance forall k (n :: k). Numeric.Dimensions.Dim.BoundedDim n => GHC.Real.Real (Numeric.Dimensions.Idx.Idx n)
instance forall k (n :: k). Numeric.Dimensions.Dim.BoundedDim n => GHC.Real.Integral (Numeric.Dimensions.Idx.Idx n)
instance forall k (n :: k). GHC.Generics.Generic (Numeric.Dimensions.Idx.Idx n)
instance forall k (n :: k). (Data.Typeable.Internal.Typeable n, Data.Typeable.Internal.Typeable k) => Data.Data.Data (Numeric.Dimensions.Idx.Idx n)
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 (n :: k). Numeric.Dimensions.Dim.BoundedDim n => GHC.Num.Num (Numeric.Dimensions.Idx.Idxs '[n])
instance forall k (ds :: [k]). Numeric.Dimensions.Dim.BoundedDims ds => GHC.Enum.Bounded (Numeric.Dimensions.Idx.Idxs ds)
instance Numeric.Dimensions.Dim.Dimensions ds => GHC.Enum.Enum (Numeric.Dimensions.Idx.Idxs ds)
instance forall k (x :: k). Numeric.Dimensions.Dim.BoundedDim x => GHC.Read.Read (Numeric.Dimensions.Idx.Idx x)
instance forall k (x :: k). GHC.Show.Show (Numeric.Dimensions.Idx.Idx x)
instance forall k (n :: k). Numeric.Dimensions.Dim.BoundedDim n => GHC.Enum.Bounded (Numeric.Dimensions.Idx.Idx n)
instance forall k (n :: k). Numeric.Dimensions.Dim.BoundedDim n => GHC.Enum.Enum (Numeric.Dimensions.Idx.Idx n)
instance forall k (n :: k). Numeric.Dimensions.Dim.BoundedDim 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 :-