dimensions-0.3.1.0: Safe type-level dimensionality for multidimensional data.

Copyright(c) Artem Chirkin
LicenseBSD3
Maintainerchirkin@arch.ethz.ch
Safe HaskellNone
LanguageHaskell2010

Numeric.TypeLits

Contents

Description

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.

Synopsis

Documentation

data XNat Source #

Either known or unknown at compile-time natural number

Constructors

XN Nat 
N Nat 

Instances

XDimensions ([] XNat) Source # 

Methods

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

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

Methods

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

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

Methods

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

type XN n = XN n Source #

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

type N n = N n Source #

Known natural number

Nats backed by Int

someIntNatVal :: Int -> Maybe SomeIntNat Source #

Similar to someNatVal, but for a single dimension

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

Similar to natVal from TypeLits, but returns Int.

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.

Minimal complete definition

dimVal'

Methods

dimVal' :: Int Source #

Get value of type-level dim at runtime

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

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 Source #

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 Source #

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

Constructors

Evidence :: a => Evidence a 

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

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

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

inferPlusKnownDim :: forall n m. (KnownDim n, KnownDim m) => Evidence (KnownDim (n + m)) 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 #

inferTimesKnownDim :: forall n m. (KnownDim n, KnownDim m) => Evidence (KnownDim (n * m)) Source #

Re-export original 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) 
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)