Safe Haskell	None
Language	Haskell2010

TensorSafe.Network

Description

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
- NNil :: Network '[]
- (:~~) :: Layer x => !x -> !(Network xs) -> Network (x ': xs)
data INetwork :: [Type] -> [Shape] -> Type where
- INNil :: SingI i => INetwork '[] '[i]
- (:~>) :: (SingI i, SingI h, Layer x) => !x -> !(INetwork xs (h ': hs)) -> INetwork (x ': xs) (i ': (h ': hs))
type family MkINetwork (layers :: [Type]) (sIn :: Shape) (sOut :: Shape) :: Type where ...
class ValidNetwork (xs :: [Type]) (ss :: [Shape])
mkINetwork :: ValidNetwork xs ss => INetwork xs ss
toCNetwork :: forall i x xs ss. (SingI i, Layer x, ValidNetwork (x ': xs) (i ': ss)) => INetwork (x ': xs) (i ': ss) -> CNetwork

Documentation

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

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)) Source #
Instance details Defined in TensorSafe.Network Methods showsPrec :: Int -> Network (x ': xs) -> ShowS # show :: Network (x ': xs) -> String # showList :: [Network (x ': xs)] -> ShowS #
Show (Network ([] :: [Type])) Source #
Instance details Defined in TensorSafe.Network Methods showsPrec :: Int -> Network [] -> ShowS # show :: Network [] -> String # showList :: [Network []] -> ShowS #

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.

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)) Source #
Instance details 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]))) Source #
Instance details 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) Source #	This instance of INetwork as a Layer makes possible nesting INetworks
Instance details Defined in TensorSafe.Network Methods layer :: INetwork ls ss Source # compile :: INetwork ls ss -> InputShape -> CNetwork Source #

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.

Equations

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

class ValidNetwork (xs :: [Type]) (ss :: [Shape]) 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 ```

Minimal complete definition

mkINetwork

Instances

SingI i => ValidNetwork ([] :: [Type]) (i ': ([] :: [Shape])) Source #
Instance details Defined in TensorSafe.Network Methods 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 #
Instance details Defined in TensorSafe.Network Methods mkINetwork :: INetwork (x ': xs) (i ': (o ': rs)) Source #

mkINetwork :: ValidNetwork xs ss => INetwork xs ss Source #

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