mathflow-0.1.0.0: Dependently typed tensorflow modeler

Safe HaskellNone
LanguageHaskell2010

MathFlow.Core

Synopsis

Documentation

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

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

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

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

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

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

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

Methods

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

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

class Dimension a where Source #

get dimension from tensor

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

Minimal complete definition

dim

Methods

dim :: a -> [Integer] Source #

Instances

Dimension (Sing [Nat] n) Source # 

Methods

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

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

Methods

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

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

(%*) :: 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 Source #

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

class FromTensor a where Source #

Minimal complete definition

fromTensor, toString, run

Methods

fromTensor :: Tensor n t a -> a Source #

toString :: Tensor n t a -> String Source #

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

Instances