TensorSafe.Network

This module is the core of TensorSafe. It defines all Network data structures -- and types functions that respresent Layers modifications of shapes, as well as -- all needed information for compiling the Network structures to CNetworks for later code -- generation.

Documentation

data Network :: [Type] -> Type where

A network that defines a specific sequence of layers

Constructors

NNil :: Network '[]

(:~~) :: Layer x => !x -> !(Network xs) -> Network (x ': xs) infixr 5

Instances

(Show x, Show (Network xs)) => Show (Network (x ': xs))

Defined in TensorSafe.Network

Methods

showsPrec :: Int -> Network (x ': xs) -> ShowS

show :: Network (x ': xs) -> String

showList :: [Network (x ': xs)] -> ShowS

Show (Network ([] :: [Type]))

Defined in TensorSafe.Network

Methods

showsPrec :: Int -> Network [] -> ShowS

show :: Network [] -> String

showList :: [Network []] -> ShowS

data INetwork :: [Type] -> [Shape] -> Type where

A network that defines a specific sequence of layers with the corresponding shape transformation along the network. It's an Instance of a Network: given a Network and a initial Shape, this type structure can be generated automatically using the type functions defined in this module, like Out and MkINetwork.

Constructors

INNil :: SingI i => INetwork '[] '[i]

(:~>) :: (SingI i, SingI h, Layer x) => !x -> !(INetwork xs (h ': hs)) -> INetwork (x ': xs) (i ': (h ': hs)) infixr 5

Instances

(Show x, Show (INetwork xs rs)) => Show (INetwork (x ': xs) (i ': rs))

Defined in TensorSafe.Network

Methods

showsPrec :: Int -> INetwork (x ': xs) (i ': rs) -> ShowS

show :: INetwork (x ': xs) (i ': rs) -> String

showList :: [INetwork (x ': xs) (i ': rs)] -> ShowS

Show (INetwork ([] :: [Type]) (i ': ([] :: [Shape])))

Defined in TensorSafe.Network

Methods

showsPrec :: Int -> INetwork [] (i ': []) -> ShowS

show :: INetwork [] (i ': []) -> String

showList :: [INetwork [] (i ': [])] -> ShowS

ValidNetwork ls ss => Layer (INetwork ls ss)

This instance of INetwork as a Layer makes possible nesting INetworks

Defined in TensorSafe.Network

Methods

layer :: INetwork ls ss

compile :: INetwork ls ss -> InputShape -> CNetwork

type family ComputeOut (layers :: [Type]) (s :: Shape) :: Shape where ...

Returns the result of applying all the layers transformation to a specific shape. Given a list of layers, this returns the expected output for the computation of each layer starting with the first layer transforming the Shape s. For example, if the initial Shape is [28, 28] and the layers are [Relu, Flatten], the result will be [784].

Equations

ComputeOut '[] s = s

ComputeOut (l ': ls) s = ComputeOut ls (Out l s)

type family ComposeOut' (layers :: [Type]) (s :: Shape) :: [Shape] where ...

Returns a list of shapes describing ALL the transformations applied to a specific shape. Given a list of layers return a type with all the Shapes from the initial Shape until the last one. In theory, the last Shape should be the same than the ComputeOut function applied to this same parameters.

Equations

ComposeOut' '[] s = '[]

ComposeOut' (l ': ls) s = Out l s ': ComposeOut' ls (Out l s)

type family ComposeOut (layers :: [Type]) (s :: Shape) :: [Shape] where ...

Same than ComposeOut' but the Shape list includes the initial Shape

Equations

ComposeOut '[] s = '[]

ComposeOut ls s = s ': ComposeOut' ls s

type family ValidateOutput (layers :: [Type]) (sIn :: Shape) (sOut :: Shape) :: Bool where ...

Compares the layers shape computation and the expected output

Equations

ValidateOutput ls sIn sOut = ShapeEquals' (ComputeOut ls sIn) sOut

type family MkINetworkUnconstrained (layers :: [Type]) (s :: Shape) :: Type where ...

Creates an INetwork type, and by "unconstrained" I mean that I don't check for an expected output

Equations

MkINetworkUnconstrained ls s = INetwork ls (ComposeOut ls s)

type family MaybeType (t :: Type) (b :: Bool) :: Type where ...

If the second type argument is 'True, then it returns the type t, otherwise it returns a default type. Note that for this example, ValidateOutput would raise an exception if the expected output and the actual one do not match.

Equations

MaybeType t False = Type

MaybeType t True = t

type family MkINetwork (layers :: [Type]) (sIn :: Shape) (sOut :: Shape) :: Type where ...

Creates an INetwork type validating the the expected output and the computed one match.

Equations

MkINetworkUnconstrained ls sIn sOut = MaybeType (INetwork ls (ComposeOut ls sIn)) (ValidateOutput ls sIn sOut)

type family MaybeShape (s :: Shape) (b :: Bool) :: Shape where ...

Equations

MaybeType s False = D1 0

MaybeType s True = s

type family Add' (layers :: [Type]) (layers2 :: [Type]) (shape :: Shape) where ...

Equations

Add' ls1 _ sIn = ComputeOut ls1 sIn

type family Out (l :: Type) (s :: Shape) :: Shape where ...

Defines the expected output of a layer This type function should be instanciated for each of the Layers defined.

Equations

Out (INetwork ls (s ': ss)) s = ComputeOut ls s

Out (Add ls1 ls2) sIn = Add' ls1 ls2 sIn

Out (BatchNormalization _ _ _) s = s

Out (Conv2D 1 1 k k' s s') (D2 inputRows inputColumns) = D2 (1 + Div (inputRows - k) s) (1 + Div (inputColumns - k') s')

Out (Conv2D 1 filters k k' s s') (D2 inputRows inputColumns) = D3 (1 + Div (inputRows - k) s) (1 + Div (inputColumns - k') s') filters

Out (Conv2D channels 1 k k' s s') (D3 inputRows inputColumns channels) = D2 (1 + Div (inputRows - k) s) (1 + Div (inputColumns - k') s')

Out (Conv2D channels filters k k' s s') (D3 inputRows inputColumns channels) = D3 (1 + Div (inputRows - k) s) (1 + Div (inputColumns - k') s') filters

Out (Dense i o) (D1 i) = D1 o

Out (Dropout rate seed) s = s

Out Flatten (D1 x) = D1 x

Out Flatten (D2 x y) = D1 (x * y)

Out Flatten (D3 x y z) = D1 ((x * y) * z)

Out GlobalAvgPooling2D (D3 _ _ z) = D1 z

Out Input s = s

Out (LSTM units False) _ = D1 units

Out (LSTM units True) (D2 x _) = D2 x units

Out (LSTM units True) (D3 x _ _) = D2 x units

Out (MaxPooling k k' s s') (D2 inputRows inputColumns) = D2 (1 + Div (inputRows - k) s) (1 + Div (inputColumns - k') s')

Out (MaxPooling k k' s s') (D3 inputRows inputColumns channels) = D3 (1 + Div (inputRows - k) s) (1 + Div (inputColumns - k') s') channels

Out Relu s = s

Out Sigmoid s = s

Out (ZeroPadding2D padding_rows padding_cols) (D2 inputRows inputColumns) = D2 (inputRows + (2 * padding_rows)) (inputColumns + (2 * padding_cols))

Out (ZeroPadding2D padding_rows padding_cols) (D3 inputRows inputColumns channels) = D3 (inputRows + (2 * padding_rows)) (inputColumns + (2 * padding_cols)) channels

Out l sIn = TypeError ((((Text "Couldn't apply the Layer \"" :<>: ShowType l) :<>: Text "\" with the input Shape \"") :<>: ShowType sIn) :<>: Text "\"")

class ValidNetwork (xs :: [Type]) (ss :: [Shape]) where

Instanciates a Network after defining a type definition, using MkINetworkUnconstrained or MkINetwork, for example. After defining a variable with INetwork type, you can instanciate that variable like this: ``` myNet :: MNIST myNet = mkINetwork ```

Methods

mkINetwork :: INetwork xs ss

Makes a valid instance of INetwork

Instances

SingI i => ValidNetwork ([] :: [Type]) (i ': ([] :: [Shape]))

Defined in TensorSafe.Network

Methods

mkINetwork :: INetwork [] (i ': [])

(SingI i, SingI o, Layer x, ValidNetwork xs (o ': rs), Out x i ~ o) => ValidNetwork (x ': xs) (i ': (o ': rs))

Defined in TensorSafe.Network

Methods

mkINetwork :: INetwork (x ': xs) (i ': (o ': rs))

toCNetwork :: forall i x xs ss. (SingI i, Layer x, ValidNetwork (x ': xs) (i ': ss)) => INetwork (x ': xs) (i ': ss) -> CNetwork

Compilation: Gets the initial shape using Singleton instances. Since this is the function we run for transforming an INetwork to CNetwork, the nested argument of toCNetwork' is set to False.

toCNetwork' :: INetwork xs ss -> Bool -> Maybe String -> CNetwork

Helper function for toCNetwork