Safe Haskell | None |
---|---|

Language | Haskell2010 |

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.

## Synopsis

- data Network :: [Type] -> Type where
- data INetwork :: [Type] -> [Shape] -> Type where
- type family ComputeOut (layers :: [Type]) (s :: Shape) :: Shape where ...
- type family ComposeOut' (layers :: [Type]) (s :: Shape) :: [Shape] where ...
- type family ComposeOut (layers :: [Type]) (s :: Shape) :: [Shape] where ...
- type family ValidateOutput (layers :: [Type]) (sIn :: Shape) (sOut :: Shape) :: Bool where ...
- type family MkINetworkUnconstrained (layers :: [Type]) (s :: Shape) :: Type where ...
- type family MaybeType (t :: Type) (b :: Bool) :: Type where ...
- type family MkINetwork (layers :: [Type]) (sIn :: Shape) (sOut :: Shape) :: Type where ...
- type family MaybeShape (s :: Shape) (b :: Bool) :: Shape where ...
- type family Add' (layers :: [Type]) (layers2 :: [Type]) (shape :: Shape) where ...
- type family Out (l :: Type) (s :: Shape) :: Shape where ...
- class ValidNetwork (xs :: [Type]) (ss :: [Shape]) where
- mkINetwork :: INetwork xs ss

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

# Documentation

data Network :: [Type] -> Type where Source #

A network that defines a specific sequence of layers

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

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`

.

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

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

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

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].

ComputeOut '[] s = s | |

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

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

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.

ComposeOut' '[] s = '[] | |

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

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

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

ComposeOut '[] s = '[] | |

ComposeOut ls s = s ': ComposeOut' ls s |

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

Compares the layers shape computation and the expected output

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

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

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

MkINetworkUnconstrained ls s = INetwork ls (ComposeOut ls s) |

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

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.

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

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

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

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

Add' ls1 _ sIn = ComputeOut ls1 sIn |

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

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

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

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 ```

mkINetwork :: INetwork xs ss Source #

Makes a valid instance of INetwork

## Instances

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

Defined in TensorSafe.Network mkINetwork :: INetwork [] (i ': []) Source # | |

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

Defined in TensorSafe.Network mkINetwork :: INetwork (x ': xs) (i ': (o ': rs)) Source # |

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

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

Helper function for `toCNetwork`