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

License | BSD3 |

Maintainer | chirkin@arch.ethz.ch |

Safe Haskell | None |

Language | Haskell2010 |

Provides a data type `Dim ds` to keep dimension sizes for multiple-dimensional data. Lower indices go first, i.e. assumed enumeration is i = i1 + i2*n1 + i3*n1*n2 + ... + ik*n1*n2*...*n(k-1).

- data Nat :: *
- data XNat
- type XN n = XN n
- type N n = N n
- data Dim ns where
- dimVal :: Dim x -> Int
- totalDim :: forall ds proxy. Dimensions ds => proxy ds -> Int
- fromInt :: forall m. KnownDim m => Int -> Maybe (Dim (XN m))
- data SomeDims = SomeDims (Dim ns)
- data SomeDim = SomeDim (Dim n)
- someDimVal :: Int -> Maybe SomeDim
- someDimsVal :: [Int] -> Maybe SomeDims
- sameDim :: Dim as -> Dim bs -> Maybe (Evidence (as ~ bs))
- compareDim :: Dim as -> Dim bs -> Ordering
- inSpaceOf :: a ds -> b ds -> a ds
- asSpaceOf :: a ds -> (b ds -> c) -> b ds -> c
- class Dimensions ds where
- class KnownDim n where
- type family KnownDims (ns :: [Nat]) :: Constraint where ...
- type family AsXDims (ns :: [Nat]) = (xns :: [XNat]) | xns -> ns where ...
- type family AsDims (xns :: [XNat]) = (ns :: [Nat]) | ns -> xns where ...
- type family WrapDims (x :: [k]) :: [XNat] where ...
- type family UnwrapDims (xns :: [k]) :: [Nat] where ...
- type family ConsDim (x :: l) (xs :: [k]) = (ys :: [k]) | ys -> x xs l where ...
- type family NatKind ks k :: Constraint where ...
- type family FixedDim (xns :: [XNat]) (ns :: [Nat]) :: [Nat] where ...
- type family FixedXDim (xns :: [XNat]) (ns :: [Nat]) :: [XNat] where ...
- type family WrapNat (xn :: XNat) (n :: Nat) :: XNat where ...
- type family (n :: Nat) :< (ns :: [Nat]) :: [Nat] where ...
- type family (ns :: [Nat]) >: (n :: Nat) :: [Nat] where ...
- inferDimensions :: forall ds. (KnownDims ds, FiniteList ds) => Evidence (Dimensions ds)
- inferDimKnownDims :: forall ds. Dimensions ds => Evidence (KnownDims ds)
- inferDimFiniteList :: forall ds. Dimensions ds => Evidence (FiniteList ds)
- inferTailDimensions :: forall ds. Dimensions ds => Maybe (Evidence (Dimensions (Tail ds)))
- inferConcatDimensions :: forall as bs. (Dimensions as, Dimensions bs) => Evidence (Dimensions (as ++ bs))
- inferPrefixDimensions :: forall bs asbs. (IsSuffix bs asbs ~ True, Dimensions bs, Dimensions asbs) => Evidence (Dimensions (Prefix bs asbs))
- inferSuffixDimensions :: forall as asbs. (IsPrefix as asbs ~ True, Dimensions as, Dimensions asbs) => Evidence (Dimensions (Suffix as asbs))
- inferSnocDimensions :: forall xs z. (KnownDim z, Dimensions xs) => Evidence (Dimensions (xs +: z))
- inferInitDimensions :: forall xs. Dimensions xs => Maybe (Evidence (Dimensions (Init xs)))
- inferTakeNDimensions :: forall n xs. (KnownDim n, Dimensions xs) => Evidence (Dimensions (Take n xs))
- inferDropNDimensions :: forall n xs. (KnownDim n, Dimensions xs) => Evidence (Dimensions (Drop n xs))
- inferReverseDimensions :: forall xs. Dimensions xs => Evidence (Dimensions (Reverse xs))
- reifyDimensions :: forall ds. Dim ds -> Evidence (Dimensions ds)
- inferUnSnocDimensions :: forall ds. Dimensions ds => Maybe (Evidence (SnocDimensions ds))
- type SnocDimensions xs = (xs ~ (Init xs +: Last xs), xs ~ (Init xs ++ '[Last xs]), IsPrefix (Init xs) xs ~ True, IsSuffix '[Last xs] xs ~ True, Suffix (Init xs) xs ~ '[Last xs], Prefix '[Last xs] xs ~ Init xs, Dimensions (Init xs), KnownDim (Last xs))
- inferUnConsDimensions :: forall ds. Dimensions ds => Maybe (Evidence (ConsDimensions ds))
- type ConsDimensions xs = (xs ~ (Head xs :+ Tail xs), xs ~ ('[Head xs] ++ Tail xs), IsPrefix '[Head xs] xs ~ True, IsSuffix (Tail xs) xs ~ True, Suffix '[Head xs] xs ~ Tail xs, Prefix (Tail xs) xs ~ '[Head xs], Dimensions (Tail xs), KnownDim (Head xs))

# Dimension data types

(Kind) This is the kind of type-level natural numbers.

Either known or unknown at compile-time natural number

XDimensions ([] XNat) Source # | |

XDimensions xs => XDimensions ((:) XNat (N n) xs) Source # | |

XDimensions xs => XDimensions ((:) XNat (XN m) xs) Source # | |

Type-level dimensionality

D :: Dim '[] | Zero-rank dimensionality - scalar |

(:*) :: forall n ns. NatKind [k] l => !(Dim n) -> !(Dim ns) -> Dim (ConsDim n ns) infixr 5 | List-like concatenation of dimensionality. NatKind constraint is needed here to infer that |

Dn :: forall n. KnownDim n => Dim (n :: Nat) | Proxy-like constructor |

Dx :: forall n m. n <= m => !(Dim m) -> Dim (XN n) | Nat known at runtime packed into existential constructor |

dimVal :: Dim x -> Int Source #

Get value of type-level dim at runtime. Gives a product of all dimensions if is a list.

totalDim :: forall ds proxy. Dimensions ds => proxy ds -> Int Source #

Product of all dimension sizes.

fromInt :: forall m. KnownDim m => Int -> Maybe (Dim (XN m)) Source #

Get runtime-known dim and make sure it is not smaller than the given Nat.

Same as SomeNat, but for Dimensions: Hide all information about Dimensions inside

Same as SomeNat, but for Dimension: Hide all information about Dimension inside

someDimVal :: Int -> Maybe SomeDim Source #

Similar to `someNatVal`

, but for a single dimension

someDimsVal :: [Int] -> Maybe SomeDims Source #

Convert a list of ints into unknown type-level Dimensions list

sameDim :: Dim as -> Dim bs -> Maybe (Evidence (as ~ bs)) Source #

We either get evidence that this function was instantiated with the
same type-level Dimensions, or `Nothing`

.

compareDim :: Dim as -> Dim bs -> Ordering Source #

Compare dimensions by their size in lexicorgaphic order from the last dimension to the first dimension (the last dimension is the most significant one).

asSpaceOf :: a ds -> (b ds -> c) -> b ds -> c Source #

Similar to `asProxyTypeOf`

,
Give a hint to type checker to fix the type of a function argument.

# Dimension constraints

class Dimensions ds where Source #

Dimensions ([] Nat) Source # | |

(KnownDim d, Dimensions ds) => Dimensions ((:) Nat d ds) Source # | |

class KnownDim n where Source #

This class gives the int associated with a type-level natural. Valid known dim must be not less than 0.

KnownNat n => KnownDim n Source # | |

KnownDim 0 Source # | |

KnownDim 1 Source # | |

KnownDim 2 Source # | |

KnownDim 3 Source # | |

KnownDim 4 Source # | |

KnownDim 5 Source # | |

KnownDim 6 Source # | |

KnownDim 7 Source # | |

KnownDim 8 Source # | |

KnownDim 9 Source # | |

KnownDim 10 Source # | |

KnownDim 11 Source # | |

KnownDim 12 Source # | |

KnownDim 13 Source # | |

KnownDim 14 Source # | |

KnownDim 15 Source # | |

KnownDim 16 Source # | |

KnownDim 17 Source # | |

KnownDim 18 Source # | |

KnownDim 19 Source # | |

KnownDim 20 Source # | |

type family KnownDims (ns :: [Nat]) :: Constraint where ... Source #

A constraint family that makes sure all subdimensions are known.

# Type-level programming

type family AsXDims (ns :: [Nat]) = (xns :: [XNat]) | xns -> ns where ... Source #

Map Dims onto XDims (injective)

type family AsDims (xns :: [XNat]) = (ns :: [Nat]) | ns -> xns where ... Source #

Map XDims onto Dims (injective)

type family UnwrapDims (xns :: [k]) :: [Nat] where ... Source #

Treat Dims or XDims uniformly as Dims

UnwrapDims ('[] :: [Nat]) = '[] | |

UnwrapDims ('[] :: [XNat]) = '[] | |

UnwrapDims (N x ': xs) = x ': UnwrapDims xs | |

UnwrapDims (XN _ ': _) = TypeError (Text "Cannot unwrap dimension XN into Nat" :$$: Text "(dimension is not known at compile time)") |

type family ConsDim (x :: l) (xs :: [k]) = (ys :: [k]) | ys -> x xs l where ... Source #

Unify usage of XNat and Nat. This is useful in function and type definitions. Mainly used in the definition of Dim.

type family NatKind ks k :: Constraint where ... Source #

Constraint on kinds; makes sure that the second argument kind is Nat if the first is a list of Nats.

type family FixedDim (xns :: [XNat]) (ns :: [Nat]) :: [Nat] where ... Source #

FixedDim tries not to inspect content of `ns`

and construct it
based only on `xns`

when it is possible.
This means it does not check if `XN m <= n`.

type family FixedXDim (xns :: [XNat]) (ns :: [Nat]) :: [XNat] where ... Source #

FixedXDim tries not to inspect content of `xns`

and construct it
based only on `ns`

when it is possible.
This means it does not check if `XN m <= n`.

type family WrapNat (xn :: XNat) (n :: Nat) :: XNat where ... Source #

WrapNat tries not to inspect content of `xn`

and construct it
based only on `n`

when it is possible.
This means it does not check if `XN m <= n`.

type family (n :: Nat) :< (ns :: [Nat]) :: [Nat] where ... infixr 6 Source #

Synonym for (:+) that treats Nat values 0 and 1 in a special way: it preserves the property that all dimensions are greater than 1.

type family (ns :: [Nat]) >: (n :: Nat) :: [Nat] where ... infixl 6 Source #

Synonym for (+:) that treats Nat values 0 and 1 in a special way: it preserves the property that all dimensions are greater than 1.

# Inference of dimension evidence

inferDimensions :: forall ds. (KnownDims ds, FiniteList ds) => Evidence (Dimensions ds) Source #

Infer `Dimensions`

given that the list is KnownDims and finite

inferDimKnownDims :: forall ds. Dimensions ds => Evidence (KnownDims ds) Source #

`Dimensions`

implies `KnownDims`

inferDimFiniteList :: forall ds. Dimensions ds => Evidence (FiniteList ds) Source #

`Dimensions`

implies `FiniteList`

inferTailDimensions :: forall ds. Dimensions ds => Maybe (Evidence (Dimensions (Tail ds))) Source #

Infer that tail list is also Dimensions

inferConcatDimensions :: forall as bs. (Dimensions as, Dimensions bs) => Evidence (Dimensions (as ++ bs)) Source #

Infer that concatenation is also Dimensions

inferPrefixDimensions :: forall bs asbs. (IsSuffix bs asbs ~ True, Dimensions bs, Dimensions asbs) => Evidence (Dimensions (Prefix bs asbs)) Source #

Infer that prefix is also Dimensions

inferSuffixDimensions :: forall as asbs. (IsPrefix as asbs ~ True, Dimensions as, Dimensions asbs) => Evidence (Dimensions (Suffix as asbs)) Source #

Infer that suffix is also Dimensions

inferSnocDimensions :: forall xs z. (KnownDim z, Dimensions xs) => Evidence (Dimensions (xs +: z)) Source #

Make snoc almost as good as cons

inferInitDimensions :: forall xs. Dimensions xs => Maybe (Evidence (Dimensions (Init xs))) Source #

Init of the list is also Dimensions

inferTakeNDimensions :: forall n xs. (KnownDim n, Dimensions xs) => Evidence (Dimensions (Take n xs)) Source #

Take KnownDim of the list is also Dimensions

inferDropNDimensions :: forall n xs. (KnownDim n, Dimensions xs) => Evidence (Dimensions (Drop n xs)) Source #

Drop KnownDim of the list is also Dimensions

inferReverseDimensions :: forall xs. Dimensions xs => Evidence (Dimensions (Reverse xs)) Source #

Reverse of the list is also Dimensions

reifyDimensions :: forall ds. Dim ds -> Evidence (Dimensions ds) Source #

Use the given `Dim ds` to create an instance of `Dimensions ds` dynamically.

# Cons and Snoc inference

inferUnSnocDimensions :: forall ds. Dimensions ds => Maybe (Evidence (SnocDimensions ds)) Source #

Init of the dimension list is also Dimensions, and the last dimension is KnownDim.

type SnocDimensions xs = (xs ~ (Init xs +: Last xs), xs ~ (Init xs ++ '[Last xs]), IsPrefix (Init xs) xs ~ True, IsSuffix '[Last xs] xs ~ True, Suffix (Init xs) xs ~ '[Last xs], Prefix '[Last xs] xs ~ Init xs, Dimensions (Init xs), KnownDim (Last xs)) Source #

Various evidence for the Snoc operation.

inferUnConsDimensions :: forall ds. Dimensions ds => Maybe (Evidence (ConsDimensions ds)) Source #

Tail of the dimension list is also Dimensions, and the head dimension is KnownDim.

type ConsDimensions xs = (xs ~ (Head xs :+ Tail xs), xs ~ ('[Head xs] ++ Tail xs), IsPrefix '[Head xs] xs ~ True, IsSuffix (Tail xs) xs ~ True, Suffix '[Head xs] xs ~ Tail xs, Prefix (Tail xs) xs ~ '[Head xs], Dimensions (Tail xs), KnownDim (Head xs)) Source #

Various evidence for the Snoc operation.