MathFlow.Core

Documentation

type family IsSubSamp (f :: [Nat]) (m :: [Nat]) (n :: [Nat]) :: Bool where ...

IsSubSamp // Subsampling constraint

• (f :: [Nat]) // strides for subsampling
• (m :: [Nat]) // dimensions of original tensor
• (n :: [Nat]) // dimensions of subsampled tensor
• :: Bool

Equations

IsSubSamp (1 ': fs) (m ': ms) (n ': ns) = IsSubSamp fs ms ns

IsSubSamp (f ': fs) (m ': ms) (n ': ns) = ((n * f) :== m) :&& IsSubSamp fs ms ns

IsSubSamp '[] '[] '[] = True

IsSubSamp _ _ _ = False

type family IsMatMul (m :: [Nat]) (o :: [Nat]) (n :: [Nat]) :: Bool where ...

IsMatMul // A constraint for matrix multiplication

• (m :: [Nat]) // dimensions of a[..., i, k]
• (o :: [Nat]) // dimensions of b[..., k, j]
• (n :: [Nat]) // dimensions of output[..., i, j] = sum_k (a[..., i, k] * b[..., k, j]), for all indices i, j.
• :: Bool

Equations

IsMatMul m o n = (Last n :== Last o) :&& ((Last m :== Head (Tail (Reverse o))) :&& ((Tail (Reverse n) :== Tail (Reverse m)) :&& (Tail (Tail (Reverse n)) :== Tail (Tail (Reverse o)))))

type family IsConcat (m :: [Nat]) (o :: [Nat]) (n :: [Nat]) :: Bool where ...

IsConcat // A constraint for concatination of tensor

• (m :: [Nat]) // dimensions of a[..., i, ...]
• (o :: [Nat]) // dimensions of b[..., k, ...]
• (n :: [Nat]) // dimensions of output[..., i+k, ...] = concat (a,b)
• :: Bool

Equations

IsConcat (m ': mx) (o ': ox) (n ': nx) = (((m :== o) :&& (m :== n)) :|| ((m + o) :== n)) :&& IsConcat mx ox nx

IsConcat '[] '[] '[] = True

IsConcat _ _ _ = False

type family IsSameProduct (m :: [Nat]) (n :: [Nat]) :: Bool where ...

IsSameProduct // A constraint for reshaping tensor

• (m :: [Nat]) // dimensions of original tensor
• (n :: [Nat]) // dimensions of reshaped tensor
• :: Bool

Equations

IsSameProduct (m ': mx) (n ': nx) = (m :== n) :&& (Product mx :== Product nx)

IsSameProduct mx nx = Product mx :== Product nx

data Tensor n t a

Dependently typed tensor model

This model includes basic arithmetic operators and tensorflow functions.

Constructors

Num t => TScalar t

Scalar value

Tensor a

Transform a value to dependently typed value

TAdd (Tensor n t a) (Tensor n t a)

+ of Num

TSub (Tensor n t a) (Tensor n t a)

• of Num

TMul (Tensor n t a) (Tensor n t a)

• of Num

TAbs (Tensor n t a)

abs of Num

TSign (Tensor n t a)

signum of Num

TRep (Tensor (Tail n) t a)

vector wise operator

TTr (Tensor (Reverse n) t a)

tensor tansporse operator

(SingI o, SingI m, SingI n, IsMatMul m o n ~ True) => TMatMul (Tensor m t a) (Tensor o t a)

matrix multiply

(SingI o, SingI m, SingI n, IsConcat m o n ~ True) => TConcat (Tensor m t a) (Tensor o t a)

concat operator

(SingI m, IsSameProduct m n ~ True) => TReshape (Tensor m t a)

reshape function

(SingI o, SingI m, Last n ~ Last o, Last m ~ Head (Tail (Reverse o)), Tail (Reverse n) ~ Tail (Reverse m)) => TConv2d (Tensor m t a) (Tensor o t a)

conv2d function

(SingI f, SingI m, IsSubSamp f m n ~ True) => TMaxPool (Sing f) (Tensor m t a)

max pool

TSoftMax (Tensor n t a)

TReLu (Tensor n t a)

TNorm (Tensor n t a)

(SingI f, SingI m, IsSubSamp f m n ~ True) => TSubSamp (Sing f) (Tensor m t a)

subsampling function

TApp (Tensor n t a) (Tensor m t2 a)

TFunc String (Tensor n t a)

TSym String

TArgT String (Tensor n t a)

TArgS String String

TArgI String Integer

TArgF String Float

TArgD String Double

SingI f => TArgSing String (Sing (f :: [Nat]))

TLabel String (Tensor n t a)

When generating code, this label is used.

Instances

Num t => Num (Tensor n t a)

Methods

(+) :: Tensor n t a -> Tensor n t a -> Tensor n t a

(-) :: Tensor n t a -> Tensor n t a -> Tensor n t a

(*) :: Tensor n t a -> Tensor n t a -> Tensor n t a

negate :: Tensor n t a -> Tensor n t a

abs :: Tensor n t a -> Tensor n t a

signum :: Tensor n t a -> Tensor n t a

fromInteger :: Integer -> Tensor n t a

SingI [Nat] n => Dimension (Tensor n t a)

Methods

dim :: Tensor n t a -> [Integer]

(<+>) :: forall n t a m t2. Tensor n t a -> Tensor m t2 a -> Tensor n t a infixr 4

class Dimension a where

get dimension from tensor

>>> dim (Tensor 1 :: Tensor '[192,10] Float Int)
[192,10]

Minimal complete definition

dim

Methods

dim :: a -> [Integer]

Instances

Dimension (Sing [Nat] n)

Methods

dim :: Sing [Nat] n -> [Integer]

SingI [Nat] n => Dimension (Tensor n t a)

Methods

dim :: Tensor n t a -> [Integer]

toValue :: forall n t a. Sing (n :: [Nat]) -> a -> Tensor n t a

(%*) :: forall o m n t a. (SingI o, SingI m, SingI n, IsMatMul m o n ~ True) => Tensor m t a -> Tensor o t a -> Tensor n t a

(<--) :: SingI n => String -> Tensor n t a -> Tensor n t a

class FromTensor a where

Minimal complete definition

fromTensor, toString, run

Methods

fromTensor :: Tensor n t a -> a

toString :: Tensor n t a -> String

run :: Tensor n t a -> IO (Int, String, String)

Instances

FromTensor PyString

Methods

fromTensor :: Tensor n t PyString -> PyString

toString :: Tensor n t PyString -> String

run :: Tensor n t PyString -> IO (Int, String, String)