OpenCV.TypeLevel

Kinds and types

data DS a

Dynamically or Statically known values

Mainly used as a promoted type.

Operationally exactly the Maybe type

Constructors

D

Something is dynamically known

S a

Something is statically known, in particular: a

Instances

Functor DS

Methods

fmap :: (a -> b) -> DS a -> DS b

(<$) :: a -> DS b -> DS a

Eq a => Eq (DS a)

Methods

(==) :: DS a -> DS a -> Bool

(/=) :: DS a -> DS a -> Bool

Show a => Show (DS a)

Methods

showsPrec :: Int -> DS a -> ShowS

show :: DS a -> String

showList :: [DS a] -> ShowS

ToInt32 (Proxy a n) => ToNatDS (Proxy (DS a) (S a n))

type level numbers are statically known

Methods

toNatDS :: Proxy (DS a) (S a n) -> DS Int32

ToNatListDS (Proxy a as) => ToShapeDS (Proxy (DS a) (S a as))

Methods

toShapeDS :: Proxy (DS a) (S a as) -> DS [DS Int32]

dsToMaybe :: DS a -> Maybe a

Converts a DS value to the corresponding Maybe value

data Z

End of list

Constructors

Z

Instances

ToShape Z

empty Vector

Methods

toShape :: Z -> Vector Int32

data a ::: b infixr 5

Heterogeneous lists

Implemented as nested 2-tuples.

f :: Int ::: Bool ::: Char ::: Z
f = 3 ::: False ::: 'X' ::: Z

Constructors

a ::: b infixr 5

Instances

(ToInt32 a, ToShape as) => ToShape ((:::) a as)

fold over :::

Methods

toShape :: (a ::: as) -> Vector Int32

Type level to value level conversions

class ToInt32 a where

Minimal complete definition

toInt32

Methods

toInt32 :: a -> Int32

Instances

ToInt32 Int32

value level: identity

Methods

toInt32 :: Int32 -> Int32

KnownNat n => ToInt32 (proxy n)

type level: reify the known natural number n

Methods

toInt32 :: proxy n -> Int32

class ToNatDS a where

Type level to value level conversion of numbers that are either Dynamically or Statically known.

toNatDS (Proxy ('S 42)) == S 42
toNatDS (Proxy 'D) == D

Minimal complete definition

toNatDS

Methods

toNatDS :: a -> DS Int32

Instances

ToNatDS (proxy (D a))

value level numbers are dynamically known

Methods

toNatDS :: proxy (D a) -> DS Int32

ToInt32 (Proxy a n) => ToNatDS (Proxy (DS a) (S a n))

type level numbers are statically known

Methods

toNatDS :: Proxy (DS a) (S a n) -> DS Int32

class ToNatListDS a where

Minimal complete definition

toNatListDS

Methods

toNatListDS :: a -> [DS Int32]

Instances

ToNatListDS (proxy ([] k))

Methods

toNatListDS :: proxy [k] -> [DS Int32]

(ToNatDS (Proxy a a1), ToNatListDS (Proxy [a] as)) => ToNatListDS (Proxy [a] ((:) a a1 as))

Methods

toNatListDS :: Proxy [a] ((a ': a1) as) -> [DS Int32]

Type functions

type family Length (xs :: [a]) :: Nat where ...

Equations

Length '[] = 0

Length (_x ': xs) = 1 + Length xs

type family Elem (e :: a) (xs :: [a]) :: Bool where ...

Equations

Elem _e '[] = False

Elem e (e ': _xs) = True

Elem e (_x ': xs) = Elem e xs

type family Relax (a :: DS ka) (b :: DS kb) :: Bool where ...

Equations

Relax x D = True

Relax (S (x ': xs)) (S (y ': ys)) = Relax x y && Relax (S xs) (S ys)

Relax (S x) (S y) = Relax x y

Relax x x = True

Relax x y = False

Predicates (constraints)

type In e xs = Elem e xs ~ True

type MayRelax a b = Relax a b ~ True

class All p xs

Instances

All k p ([] k)

(p x, All a p xs) => All a p ((:) a x xs)

class PrivateIsStatic ds => IsStatic ds

Instances

IsStatic a (S a a1)

Type conversions

type family DSNat (a :: ka) :: DS Nat where ...

Equations

DSNat Integer = D

DSNat Int32 = D

DSNat (Proxy n) = S n

DSNat (n :: Nat) = S n

type family DSNats (a :: ka) :: [DS Nat] where ...

Equations

DSNats Z = '[]

DSNats (x ::: xs) = DSNat x ': DSNats xs

DSNats ('[] :: [Nat]) = '[]

DSNats (x ': xs) = DSNat x ': DSNats xs