Copyright | (c) Artem Chirkin |
---|---|
License | BSD3 |
Maintainer | chirkin@arch.ethz.ch |
Safe Haskell | None |
Language | Haskell2010 |
Some dimensions in a type-level dimension list may by not known at compile time.
- data XDim xns = (FixedDim xns ns ~ ns, FixedXDim xns ns ~ xns) => XDim (Dim ns)
- xdim :: forall ds xds. (Dimensions ds, XDimensions xds, FixedXDim xds ds ~ xds) => Dim xds
- xDimVal :: Dim (xns :: [XNat]) -> XDim xns
- class XDimensions xds where
Data types
Similar to SomeNat, hide some dimensions under an existential constructor. In contrast to SomeDim, it preserves the order of dimensions, and it can keep some of the dimensions in the list static while making other dimensions known only at runtime.
xdim :: forall ds xds. (Dimensions ds, XDimensions xds, FixedXDim xds ds ~ xds) => Dim xds Source #
Loose compile-time information about dimensionalities
Constraints
class XDimensions xds where Source #
XDimensions ([] XNat) Source # | |
XDimensions xs => XDimensions ((:) XNat (N n) xs) Source # | |
XDimensions xs => XDimensions ((:) XNat (XN m) xs) Source # | |