Numeric.TypeLits

This modules is based on TypeLits and re-exports its functionality. It provides KnownDim class that is similar to KnownNat, but keeps Ints instead of Integers. A set of utility functions provide inference functionality, so that KnownDim can be preserved over some type-level operations.

Documentation

data XNat

Either known or unknown at compile-time natural number

Constructors

XN Nat

N Nat

Instances

XDimensions ([] XNat)

Methods

wrapDim :: ([XNat] ~ FixedXDim [XNat] ds) [XNat] => Dim [Nat] ds -> Dim [XNat] [XNat]

XDimensions xs => XDimensions ((:) XNat (N n) xs)

Methods

wrapDim :: ([XNat] ~ FixedXDim ((XNat ': N n) xs) ds) ((XNat ': N n) xs) => Dim [Nat] ds -> Dim [XNat] ((XNat ': N n) xs)

XDimensions xs => XDimensions ((:) XNat (XN m) xs)

Methods

wrapDim :: ([XNat] ~ FixedXDim ((XNat ': XN m) xs) ds) ((XNat ': XN m) xs) => Dim [Nat] ds -> Dim [XNat] ((XNat ': XN m) xs)

type XN n = XN n

Unknown natural number, known to be not smaller than the given Nat

type N n = N n

Known natural number

Nats backed by Int

data SomeIntNat

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

Constructors

KnownDim n => SomeIntNat (Proxy n)

Instances

Eq SomeIntNat

Methods

(==) :: SomeIntNat -> SomeIntNat -> Bool

(/=) :: SomeIntNat -> SomeIntNat -> Bool

Ord SomeIntNat

Methods

compare :: SomeIntNat -> SomeIntNat -> Ordering

(<) :: SomeIntNat -> SomeIntNat -> Bool

(<=) :: SomeIntNat -> SomeIntNat -> Bool

(>) :: SomeIntNat -> SomeIntNat -> Bool

(>=) :: SomeIntNat -> SomeIntNat -> Bool

max :: SomeIntNat -> SomeIntNat -> SomeIntNat

min :: SomeIntNat -> SomeIntNat -> SomeIntNat

Read SomeIntNat

Methods

readsPrec :: Int -> ReadS SomeIntNat

readList :: ReadS [SomeIntNat]

readPrec :: ReadPrec SomeIntNat

readListPrec :: ReadPrec [SomeIntNat]

Show SomeIntNat

Methods

showsPrec :: Int -> SomeIntNat -> ShowS

show :: SomeIntNat -> String

showList :: [SomeIntNat] -> ShowS

someIntNatVal :: Int -> Maybe SomeIntNat

Similar to someNatVal, but for a single dimension

intNatVal :: forall n proxy. KnownDim n => proxy n -> Int

Similar to natVal from TypeLits, but returns Int.

reifyDim :: forall r. Int -> (forall n. KnownDim n => Proxy# n -> r) -> r

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

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

Minimal complete definition

dimVal'

Methods

dimVal' :: Int

Get value of type-level dim at runtime

Instances

KnownNat n => KnownDim n

Methods

dimVal' :: Int

KnownDim 0

Methods

dimVal' :: Int

KnownDim 1

Methods

dimVal' :: Int

KnownDim 2

Methods

dimVal' :: Int

KnownDim 3

Methods

dimVal' :: Int

KnownDim 4

Methods

dimVal' :: Int

KnownDim 5

Methods

dimVal' :: Int

KnownDim 6

Methods

dimVal' :: Int

KnownDim 7

Methods

dimVal' :: Int

KnownDim 8

Methods

dimVal' :: Int

KnownDim 9

Methods

dimVal' :: Int

KnownDim 10

Methods

dimVal' :: Int

KnownDim 11

Methods

dimVal' :: Int

KnownDim 12

Methods

dimVal' :: Int

KnownDim 13

Methods

dimVal' :: Int

KnownDim 14

Methods

dimVal' :: Int

KnownDim 15

Methods

dimVal' :: Int

KnownDim 16

Methods

dimVal' :: Int

KnownDim 17

Methods

dimVal' :: Int

KnownDim 18

Methods

dimVal' :: Int

KnownDim 19

Methods

dimVal' :: Int

KnownDim 20

Methods

dimVal' :: Int

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

A constraint family that makes sure all subdimensions are known.

Equations

KnownDims '[] = ()

KnownDims (x ': xs) = (KnownDim x, KnownDims xs)

dimVal# :: forall n. KnownDim n => Proxy# n -> Int

A variant of dimVal' that gets Proxy# as an argument.

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.

proxy# :: Proxy# k a

Witness for an unboxed Proxy# value, which has no runtime representation.

Dynamically constructing evidence

data Evidence :: Constraint -> Type where

Bring an instance of certain class or constaint satisfaction evidence into scope.

Constructors

Evidence :: a => Evidence a

withEvidence :: Evidence a -> (a => r) -> r

sumEvs :: Evidence a -> Evidence b -> Evidence (a, b)

(+!+) :: Evidence a -> Evidence b -> Evidence (a, b) infixl 4

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))

Re-export original GHC TypeLits

module GHC.TypeLits

data Proxy k t :: forall k. k -> *

A concrete, poly-kinded proxy type

Constructors

Proxy

Instances

Monad (Proxy *)

Methods

(>>=) :: Proxy * a -> (a -> Proxy * b) -> Proxy * b

(>>) :: Proxy * a -> Proxy * b -> Proxy * b

return :: a -> Proxy * a

fail :: String -> Proxy * a

Functor (Proxy *)

Methods

fmap :: (a -> b) -> Proxy * a -> Proxy * b

(<$) :: a -> Proxy * b -> Proxy * a

Applicative (Proxy *)

Methods

pure :: a -> Proxy * a

(<*>) :: Proxy * (a -> b) -> Proxy * a -> Proxy * b

(*>) :: Proxy * a -> Proxy * b -> Proxy * b

(<*) :: Proxy * a -> Proxy * b -> Proxy * a

Foldable (Proxy *)

Methods

fold :: Monoid m => Proxy * m -> m

foldMap :: Monoid m => (a -> m) -> Proxy * a -> m

foldr :: (a -> b -> b) -> b -> Proxy * a -> b

foldr' :: (a -> b -> b) -> b -> Proxy * a -> b

foldl :: (b -> a -> b) -> b -> Proxy * a -> b

foldl' :: (b -> a -> b) -> b -> Proxy * a -> b

foldr1 :: (a -> a -> a) -> Proxy * a -> a

foldl1 :: (a -> a -> a) -> Proxy * a -> a

toList :: Proxy * a -> [a]

null :: Proxy * a -> Bool

length :: Proxy * a -> Int

elem :: Eq a => a -> Proxy * a -> Bool

maximum :: Ord a => Proxy * a -> a

minimum :: Ord a => Proxy * a -> a

sum :: Num a => Proxy * a -> a

product :: Num a => Proxy * a -> a

Generic1 (Proxy *)

Associated Types

type Rep1 (Proxy * :: * -> *) :: * -> *

Methods

from1 :: Proxy * a -> Rep1 (Proxy *) a

to1 :: Rep1 (Proxy *) a -> Proxy * a

Alternative (Proxy *)

Methods

empty :: Proxy * a

(<|>) :: Proxy * a -> Proxy * a -> Proxy * a

some :: Proxy * a -> Proxy * [a]

many :: Proxy * a -> Proxy * [a]

MonadPlus (Proxy *)

Methods

mzero :: Proxy * a

mplus :: Proxy * a -> Proxy * a -> Proxy * a

Bounded (Proxy k s)

Methods

minBound :: Proxy k s

maxBound :: Proxy k s

Enum (Proxy k s)

Methods

succ :: Proxy k s -> Proxy k s

pred :: Proxy k s -> Proxy k s

toEnum :: Int -> Proxy k s

fromEnum :: Proxy k s -> Int

enumFrom :: Proxy k s -> [Proxy k s]

enumFromThen :: Proxy k s -> Proxy k s -> [Proxy k s]

enumFromTo :: Proxy k s -> Proxy k s -> [Proxy k s]

enumFromThenTo :: Proxy k s -> Proxy k s -> Proxy k s -> [Proxy k s]

Eq (Proxy k s)

Methods

(==) :: Proxy k s -> Proxy k s -> Bool

(/=) :: Proxy k s -> Proxy k s -> Bool

Ord (Proxy k s)

Methods

compare :: Proxy k s -> Proxy k s -> Ordering

(<) :: Proxy k s -> Proxy k s -> Bool

(<=) :: Proxy k s -> Proxy k s -> Bool

(>) :: Proxy k s -> Proxy k s -> Bool

(>=) :: Proxy k s -> Proxy k s -> Bool

max :: Proxy k s -> Proxy k s -> Proxy k s

min :: Proxy k s -> Proxy k s -> Proxy k s

Read (Proxy k s)

Methods

readsPrec :: Int -> ReadS (Proxy k s)

readList :: ReadS [Proxy k s]

readPrec :: ReadPrec (Proxy k s)

readListPrec :: ReadPrec [Proxy k s]

Show (Proxy k s)

Methods

showsPrec :: Int -> Proxy k s -> ShowS

show :: Proxy k s -> String

showList :: [Proxy k s] -> ShowS

Ix (Proxy k s)

Methods

range :: (Proxy k s, Proxy k s) -> [Proxy k s]

index :: (Proxy k s, Proxy k s) -> Proxy k s -> Int

unsafeIndex :: (Proxy k s, Proxy k s) -> Proxy k s -> Int

inRange :: (Proxy k s, Proxy k s) -> Proxy k s -> Bool

rangeSize :: (Proxy k s, Proxy k s) -> Int

unsafeRangeSize :: (Proxy k s, Proxy k s) -> Int

Generic (Proxy k t)

Associated Types

type Rep (Proxy k t) :: * -> *

Methods

from :: Proxy k t -> Rep (Proxy k t) x

to :: Rep (Proxy k t) x -> Proxy k t

Monoid (Proxy k s)

Methods

mempty :: Proxy k s

mappend :: Proxy k s -> Proxy k s -> Proxy k s

mconcat :: [Proxy k s] -> Proxy k s

type Rep1 (Proxy *)

type Rep1 (Proxy *) = D1 (MetaData "Proxy" "Data.Proxy" "base" False) (C1 (MetaCons "Proxy" PrefixI False) U1)

type Rep (Proxy k t)

type Rep (Proxy k t) = D1 (MetaData "Proxy" "Data.Proxy" "base" False) (C1 (MetaCons "Proxy" PrefixI False) U1)