TensorSafe.Core

This module adds some meaningfull type operations that are of use throughout all the project.

Documentation

type family ShapeProduct (s :: [Nat]) :: Nat where ...

Multiplies all numbers on a list of natural numbers

Equations

ShapeProduct '[] = 1

ShapeProduct (m ': s) = m * ShapeProduct s

type family TypeEquals (s1 :: Type) (s2 :: Type) :: Bool where ...

Compares two types in kinds level

Equations

TypeEquals s s = True

TypeEquals _ _ = False

type family TypeEquals' s1 s2 :: Type where ...

Compares two types in kinds level and raises error if they don't match

Equations

TypeEquals' s s = s

TypeEquals' s1 s2 = TypeError (((Text "Couldn't match the type " :<>: ShowType s1) :<>: Text " with type ") :<>: ShowType s2)

data R (n :: Nat) where

Wrapper for a Nat value

Constructors

R :: KnownNat n => R n

Instances

KnownNat n => Show (R n)

Defined in TensorSafe.Core

Methods

showsPrec :: Int -> R n -> ShowS

show :: R n -> String

showList :: [R n] -> ShowS

data L (m :: Nat) (n :: Nat) where

Wrapper for a tuple of 2 Nat values

Constructors

L :: (KnownNat m, KnownNat n) => L m n

Instances

(KnownNat m, KnownNat n) => Show (L m n)

Defined in TensorSafe.Core

Methods

showsPrec :: Int -> L m n -> ShowS

show :: L m n -> String

showList :: [L m n] -> ShowS