Copyright | (c) Artem Chirkin |
---|---|
License | BSD3 |
Maintainer | chirkin@arch.ethz.ch |
Safe Haskell | None |
Language | Haskell2010 |
- data XNat
- type XN n = XN n
- type N n = N n
- data SomeIntNat = KnownDim n => SomeIntNat (Proxy n)
- someIntNatVal :: Int -> Maybe SomeIntNat
- intNatVal :: forall n proxy. KnownDim n => proxy n -> Int
- reifyDim :: forall r. Int -> (forall n. KnownDim n => Proxy# n -> r) -> r
- class KnownDim n where
- type family KnownDims (ns :: [Nat]) :: Constraint where ...
- dimVal# :: forall n. KnownDim n => Proxy# n -> Int
- data Proxy# :: forall k. k -> TYPE VoidRep
- proxy# :: Proxy# k a
- data Evidence :: Constraint -> Type where
- withEvidence :: Evidence a -> (a => r) -> r
- sumEvs :: Evidence a -> Evidence b -> Evidence (a, b)
- (+!+) :: Evidence a -> Evidence b -> Evidence (a, b)
- inferPlusKnownDim :: forall n m. (KnownDim n, KnownDim m) => Evidence (KnownDim (n + m))
- inferMinusKnownDim :: forall n m. (KnownDim n, KnownDim m, m <= n) => Evidence (KnownDim (n - m))
- inferMinusKnownDimM :: forall n m. (KnownDim n, KnownDim m) => Maybe (Evidence (KnownDim (n - m)))
- inferTimesKnownDim :: forall n m. (KnownDim n, KnownDim m) => Evidence (KnownDim (n * m))
- module GHC.TypeLits
- data Proxy k t :: forall k. k -> * = Proxy
Documentation
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 # | |
Nats backed by Int
data SomeIntNat Source #
Same as SomeNat, but for Dimensions: Hide all information about Dimensions inside
KnownDim n => SomeIntNat (Proxy n) |
someIntNatVal :: Int -> Maybe SomeIntNat Source #
Similar to someNatVal
, but for a single dimension
reifyDim :: forall r. Int -> (forall n. KnownDim n => Proxy# n -> r) -> r Source #
This function does GHC's magic to convert user-supplied dimVal'
function
to create an instance of KnownDim typeclass at runtime.
The trick is taken from Edward Kmett's reflection library explained
in https://www.schoolofhaskell.com/user/thoughtpolice/using-reflection
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.
data Proxy# :: forall k. k -> TYPE VoidRep #
The type constructor Proxy#
is used to bear witness to some
type variable. It's used when you want to pass around proxy values
for doing things like modelling type applications. A Proxy#
is not only unboxed, it also has a polymorphic kind, and has no
runtime representation, being totally free.
Dynamically constructing evidence
data Evidence :: Constraint -> Type where Source #
Bring an instance of certain class or constaint satisfaction evidence into scope.
withEvidence :: Evidence a -> (a => r) -> r Source #
inferMinusKnownDim :: forall n m. (KnownDim n, KnownDim m, m <= n) => Evidence (KnownDim (n - m)) Source #
inferMinusKnownDimM :: forall n m. (KnownDim n, KnownDim m) => Maybe (Evidence (KnownDim (n - m))) Source #
Re-export original GHC TypeLits
module GHC.TypeLits
data Proxy k t :: forall k. k -> * #
A concrete, poly-kinded proxy type
Monad (Proxy *) | |
Functor (Proxy *) | |
Applicative (Proxy *) | |
Foldable (Proxy *) | |
Generic1 (Proxy *) | |
Alternative (Proxy *) | |
MonadPlus (Proxy *) | |
Bounded (Proxy k s) | |
Enum (Proxy k s) | |
Eq (Proxy k s) | |
Ord (Proxy k s) | |
Read (Proxy k s) | |
Show (Proxy k s) | |
Ix (Proxy k s) | |
Generic (Proxy k t) | |
Monoid (Proxy k s) | |
type Rep1 (Proxy *) | |
type Rep (Proxy k t) | |