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

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

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

Minimal complete definition

mkINetwork

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

mkINetwork :: ValidNetwork xs ss => INetwork xs ss

Makes a valid instance of INetwork

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.