diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -71,6 +71,20 @@ ('D1 10) -- Output ``` +## How to extend layers definitions + +Since this library only implements a subset of features that Keras implement, it's likely that for +new projects you'll need to add new layers. Due to the modularization of the library, this can be +done by adding the layer definitions in specific locations of the project: + +1. First, add a new auxiliary layer entry for the data type `DLayer` in `TensorSafe.Compile.Expr`. + This will make possible the compilation of the layer for all instances of `Generator`. Also, add + to the `LayerGenerator` entry for the newly added layer. +2. Secondly, add the layer definition to the `TensorSafe/Layers` folder. You can copy the + definitions from the currently defined layers. +3. Then, import and expose your layer definition in the `TensorSafe.Layers` module. +4. Finally, declare how your layer transforms a specific Shape in the `Out` type function. + ## Command line interface > This interface will change in the near future diff --git a/src/TensorSafe/Compile/Expr.hs b/src/TensorSafe/Compile/Expr.hs --- a/src/TensorSafe/Compile/Expr.hs +++ b/src/TensorSafe/Compile/Expr.hs @@ -21,18 +21,24 @@ -- | Auxiliary data representation of Layers -- IMPORTANT: If you add new Layers definitions to `TensorSafe.Layers`, you should add -- the corresponding data structure here for the same layer. -data DLayer = DConv2D +data DLayer = DActivation + | DAdd + | DBatchNormalization + | DConv2D | DDense | DDropout | DFlatten + | DGlobalAvgPooling2D + | DInput | DLSTM | DMaxPooling | DRelu - | DActivation + | DZeroPadding2D deriving Show -- | Defines the data CNetwork = CNSequence CNetwork + | CNAdd CNetwork CNetwork | CNCons CNetwork CNetwork | CNLayer DLayer (Map String String) | CNReturn -- End of initial sequence network @@ -51,24 +57,34 @@ generateName :: l -> DLayer -> String instance LayerGenerator JavaScript where - generateName _ DConv2D = "conv2d" - generateName _ DDense = "dense" - generateName _ DDropout = "dropout" - generateName _ DFlatten = "flatten" - generateName _ DLSTM = "lstm" - generateName _ DMaxPooling = "maxPooling2d" - generateName _ DRelu = "reLU" - generateName _ DActivation = "activation" + generateName _ DActivation = "activation" + generateName _ DAdd = "addStrict" + generateName _ DBatchNormalization = "batchNormalization" + generateName _ DConv2D = "conv2d" + generateName _ DDense = "dense" + generateName _ DDropout = "dropout" + generateName _ DFlatten = "flatten" + generateName _ DGlobalAvgPooling2D = "globalAvgeragePooling2D" + generateName _ DInput = "input" + generateName _ DLSTM = "lstm" + generateName _ DMaxPooling = "maxPooling2d" + generateName _ DRelu = "reLU" + generateName _ DZeroPadding2D = "zeroPadding2D" instance LayerGenerator Python where - generateName _ DConv2D = "Conv2D" - generateName _ DDense = "Dense" - generateName _ DDropout = "Dropout" - generateName _ DFlatten = "Flatten" - generateName _ DLSTM = "LSTM" - generateName _ DMaxPooling = "MaxPool2D" - generateName _ DRelu = "ReLu" - generateName _ DActivation = "Activation" + generateName _ DActivation = "Activation" + generateName _ DAdd = "add" + generateName _ DBatchNormalization = "BatchNormalization" + generateName _ DConv2D = "Conv2D" + generateName _ DDense = "Dense" + generateName _ DDropout = "Dropout" + generateName _ DFlatten = "Flatten" + generateName _ DGlobalAvgPooling2D = "GlobalAvgeragePooling2D" + generateName _ DInput = "Input" + generateName _ DLSTM = "LSTM" + generateName _ DMaxPooling = "MaxPool2D" + generateName _ DRelu = "ReLu" + generateName _ DZeroPadding2D = "ZeroPadding2D" -- | Class that defines which languages are supported for CNetworks generation to text class Generator l where diff --git a/src/TensorSafe/Examples/ResNet50Example.hs b/src/TensorSafe/Examples/ResNet50Example.hs new file mode 100644 --- /dev/null +++ b/src/TensorSafe/Examples/ResNet50Example.hs @@ -0,0 +1,86 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE GADTs #-} +{-| This module implements the ResNet50 model using Convs with BatchNormalization. + This implementation is based on the Keras application implementation: + https://github.com/keras-team/keras-applications/blob/master/keras_applications/resnet50.py +-} +module TensorSafe.Examples.ResNet50Example where + +import TensorSafe.Layers +-- import TensorSafe.Network (MkINetwork, mkINetwork) +import TensorSafe.Network +import TensorSafe.Shape + + +type IdentityBlock channels kernel_size filters1 filters2 filters3 = + '[ Conv2D channels filters1 1 1 1 1 + , BatchNormalization 3 99 1 + , Relu + , Conv2D filters1 filters2 kernel_size kernel_size 1 1 + , BatchNormalization 3 99 1 + , ZeroPadding2D 1 1 + , Relu + , Conv2D filters2 filters3 1 1 1 1 + , BatchNormalization 3 99 1 + ] + +type Shortcut channels stride_size filters3 = + '[ Conv2D channels filters3 1 1 stride_size stride_size + , BatchNormalization 3 99 1 + ] + + +type ConvBlock channels kernel_size stride_size filters1 filters2 filters3 = + '[ Conv2D channels filters1 1 1 stride_size stride_size + , BatchNormalization 3 99 1 + , Relu + , Conv2D filters1 filters2 kernel_size kernel_size 1 1 + , ZeroPadding2D 1 1 + , BatchNormalization 3 99 1 + , Relu + , Conv2D filters2 filters3 1 1 1 1 + , BatchNormalization 3 99 1 + ] + +type ResNet50 img_size channels = + MkINetwork + '[ Input + , ZeroPadding2D 3 3 + , Conv2D channels 64 7 7 2 2 + , BatchNormalization 3 99 1 + , Relu + , ZeroPadding2D 1 1 + , MaxPooling 3 3 2 2 + + -- First block + , Add (ConvBlock 64 3 1 64 64 256) (Shortcut 64 1 256) , Relu + , Add (IdentityBlock 256 3 64 64 256) '[Input] , Relu + , Add (IdentityBlock 256 3 64 64 256) '[Input] , Relu + + -- Second block + , Add (ConvBlock 256 3 1 128 128 512) (Shortcut 256 1 512) , Relu + , Add (IdentityBlock 512 3 128 128 512) '[Input] , Relu + , Add (IdentityBlock 512 3 128 128 512) '[Input] , Relu + , Add (IdentityBlock 512 3 128 128 512) '[Input] , Relu + + -- Third block + , Add (ConvBlock 512 3 1 256 256 1024) (Shortcut 512 1 1024) , Relu + , Add (IdentityBlock 1024 3 256 256 1024) '[Input] , Relu + , Add (IdentityBlock 1024 3 256 256 1024) '[Input] , Relu + , Add (IdentityBlock 1024 3 256 256 1024) '[Input] , Relu + , Add (IdentityBlock 1024 3 256 256 1024) '[Input] , Relu + , Add (IdentityBlock 1024 3 256 256 1024) '[Input] , Relu + + -- -- Fourth block + , Add (ConvBlock 1024 3 1 512 512 2048) (Shortcut 1024 1 2048) , Relu + , Add (IdentityBlock 2048 3 512 512 2048) '[Input] , Relu + , Add (IdentityBlock 2048 3 512 512 2048) '[Input] , Relu + + , GlobalAvgPooling2D + , Dense 2048 1000 + ] + ('D3 img_size img_size channels) -- Input + ('D1 1000) -- Output + +resnet50 :: ResNet50 224 1 +resnet50 = mkINetwork diff --git a/src/TensorSafe/Layers.hs b/src/TensorSafe/Layers.hs --- a/src/TensorSafe/Layers.hs +++ b/src/TensorSafe/Layers.hs @@ -1,20 +1,30 @@ {-| This module exposes all Layers declared at TensorSafe.Layers. -} module TensorSafe.Layers ( + Add, + BatchNormalization, Conv2D, Dense, Dropout, Flatten, + GlobalAvgPooling2D, + Input, LSTM, MaxPooling, Relu, - Sigmoid + Sigmoid, + ZeroPadding2D ) where +import TensorSafe.Layers.Add +import TensorSafe.Layers.BatchNormalization import TensorSafe.Layers.Conv2D import TensorSafe.Layers.Dense import TensorSafe.Layers.Dropout import TensorSafe.Layers.Flatten +import TensorSafe.Layers.GlobalAvgPooling2D +import TensorSafe.Layers.Input import TensorSafe.Layers.LSTM import TensorSafe.Layers.MaxPooling import TensorSafe.Layers.Relu import TensorSafe.Layers.Sigmoid +import TensorSafe.Layers.ZeroPadding2D diff --git a/src/TensorSafe/Layers/Add.hs b/src/TensorSafe/Layers/Add.hs new file mode 100644 --- /dev/null +++ b/src/TensorSafe/Layers/Add.hs @@ -0,0 +1,21 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE PolyKinds #-} +{-| This module declares the Add layer data type. -} +module TensorSafe.Layers.Add (Add) where + +import Data.Kind (Type) +import Data.Map + +import TensorSafe.Compile.Expr +import TensorSafe.Layer + +-- | Adds the dimensions of the shapes to a list of values with shape D1 +data Add :: ls1 -> ls2 -> Type where + Add :: Add ls1 ls2 + deriving Show + +-- instance (Layer l1, Layer l2) => Layer (Add l1 l2) where +instance Layer (Add ls1 ls2) where + layer = Add + compile _ _ = CNLayer DAdd empty diff --git a/src/TensorSafe/Layers/BatchNormalization.hs b/src/TensorSafe/Layers/BatchNormalization.hs new file mode 100644 --- /dev/null +++ b/src/TensorSafe/Layers/BatchNormalization.hs @@ -0,0 +1,36 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeFamilies #-} +{-| This module declares the BatchNormalization layer data type. -} +module TensorSafe.Layers.BatchNormalization where + +import Data.Kind (Type) +import Data.Map +import Data.Proxy +import GHC.TypeLits + +import TensorSafe.Compile.Expr +import TensorSafe.Layer + + +-- | A classic BatchNormalization layer with axis, momentum and epsilon parameters +data BatchNormalization :: Nat -> Nat -> Nat -> Type where + BatchNormalization :: BatchNormalization axis momentum epsilon + deriving Show + +instance ( KnownNat axis + , KnownNat momentum + , KnownNat epsilon + ) => Layer (BatchNormalization axis momentum epsilon) where + layer = BatchNormalization + compile _ _ = + let axis = show $ natVal (Proxy :: Proxy axis) + momentum = show $ natVal (Proxy :: Proxy momentum) + epsilon = show $ natVal (Proxy :: Proxy epsilon) + in + CNLayer DBatchNormalization (fromList [ + ("axis", axis), + ("epsilon", epsilon), + ("momentum", momentum) + ]) diff --git a/src/TensorSafe/Layers/GlobalAvgPooling2D.hs b/src/TensorSafe/Layers/GlobalAvgPooling2D.hs new file mode 100644 --- /dev/null +++ b/src/TensorSafe/Layers/GlobalAvgPooling2D.hs @@ -0,0 +1,15 @@ +{-| This module declares the GlobalAvgPooling2D layer data type. -} +module TensorSafe.Layers.GlobalAvgPooling2D (GlobalAvgPooling2D) where + +import Data.Map + +import TensorSafe.Compile.Expr +import TensorSafe.Layer + +-- | A GlobalAvgPooling2D function +data GlobalAvgPooling2D = GlobalAvgPooling2D deriving Show + +instance Layer GlobalAvgPooling2D where + layer = GlobalAvgPooling2D + compile _ _ = CNLayer DGlobalAvgPooling2D empty + diff --git a/src/TensorSafe/Layers/Input.hs b/src/TensorSafe/Layers/Input.hs new file mode 100644 --- /dev/null +++ b/src/TensorSafe/Layers/Input.hs @@ -0,0 +1,19 @@ +{-| This module declares the Input layer data type. -} +module TensorSafe.Layers.Input (Input) where + +import Data.Map + +import TensorSafe.Compile.Expr +import TensorSafe.Layer + +-- | Inputs the dimensions of the shapes to a list of values with shape D1 +data Input = Input deriving Show + +instance Layer Input where + layer = Input + compile _ inputShape = + let params = case inputShape of + Just shape -> fromList [("inputShape", shape)] + Nothing -> empty + in + CNLayer DInput params diff --git a/src/TensorSafe/Layers/ZeroPadding2D.hs b/src/TensorSafe/Layers/ZeroPadding2D.hs new file mode 100644 --- /dev/null +++ b/src/TensorSafe/Layers/ZeroPadding2D.hs @@ -0,0 +1,32 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeFamilies #-} +{-| This module declares the ZeroPadding2D layer data type. -} +module TensorSafe.Layers.ZeroPadding2D (ZeroPadding2D) where + +import Data.Kind (Type) +import Data.Map +import Data.Proxy +import GHC.TypeLits + +import TensorSafe.Compile.Expr +import TensorSafe.Layer + +-- | A ZeroPadding2D layer with padding_rows and padding_cols arguments +data ZeroPadding2D :: Nat -> Nat -> Type where + ZeroPadding2D :: ZeroPadding2D padding_rows padding_cols + deriving Show + +instance ( KnownNat padding_rows + , KnownNat padding_cols + ) => Layer (ZeroPadding2D padding_rows padding_cols) where + layer = ZeroPadding2D + compile _ _ = + let padding_rows = show $ natVal (Proxy :: Proxy padding_rows) + padding_cols = show $ natVal (Proxy :: Proxy padding_cols) + in + CNLayer DZeroPadding2D (fromList [ + ("padding_rows", padding_rows), + ("padding_cols", padding_cols) + ]) diff --git a/src/TensorSafe/Network.hs b/src/TensorSafe/Network.hs --- a/src/TensorSafe/Network.hs +++ b/src/TensorSafe/Network.hs @@ -13,14 +13,15 @@ -- all needed information for compiling the Network structures to CNetworks for later code -- generation. -} -module TensorSafe.Network ( - Network (..), - INetwork (..), - MkINetwork, - ValidNetwork, - mkINetwork, - toCNetwork -) where +-- module TensorSafe.Network ( +-- Network (..), +-- INetwork (..), +-- MkINetwork, +-- ValidNetwork, +-- mkINetwork, +-- toCNetwork +-- ) where +module TensorSafe.Network where import Data.Kind (Type) import Data.Singletons @@ -128,6 +129,14 @@ -- MAPPING TRANSFORMATIONS OF LAYERS AND SHAPES -- +type family MaybeShape (s :: Shape) (b :: Bool) :: Shape where + MaybeType s 'False = 'D1 0 -- HACK: ShapeEquals' should raise an exception on this case + MaybeType s 'True = s + + +type family Add' (layers :: [Type]) (layers2 :: [Type]) (shape :: Shape) where + Add' ls1 _ sIn = ComputeOut ls1 sIn + -- | Defines the expected output of a layer -- This type function should be instanciated for each of the Layers defined. type family Out (l :: Type) (s :: Shape) :: Shape where @@ -139,6 +148,20 @@ -- -- -- + Out (Add ls1 ls2) sIn = Add' ls1 ls2 sIn + -- MaybeShape + -- (ComputeOut ls1 sIn) + -- (ShapeEquals' (ComputeOut ls1 sIn) (ComputeOut ls2 sIn)) -- Validation that computes the same + -- Out (Add (INetwork ls (s : ss))) s = ComputeOut ls s + + -- + -- + -- + 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')) @@ -181,6 +204,16 @@ -- -- -- + 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 @@ -202,21 +235,30 @@ -- -- -- - Out Relu s = s + Out Relu s = s -- -- -- - Out Sigmoid s = s + Out Sigmoid s = s -- + -- + -- + Out (ZeroPadding2D padding_rows padding_cols) ('D2 inputRows inputColumns) = + ('D2 (inputRows + (2 N.* padding_rows)) (inputColumns + (2 N.* padding_cols))) + + Out (ZeroPadding2D padding_rows padding_cols) ('D3 inputRows inputColumns channels) = + ('D3 (inputRows + (2 N.* padding_rows)) (inputColumns + (2 N.* padding_cols)) channels) + + -- -- Edge case or not defined raise an error -- - Out l sOut = + Out l sIn = TypeError ( 'Text "Couldn't apply the Layer \"" ':<>: 'ShowType l - ':<>: 'Text "\" with the output Shape \"" - ':<>: 'ShowType sOut + ':<>: 'Text "\" with the input Shape \"" + ':<>: 'ShowType sIn ':<>: 'Text "\"") -- diff --git a/tensor-safe.cabal b/tensor-safe.cabal --- a/tensor-safe.cabal +++ b/tensor-safe.cabal @@ -4,10 +4,10 @@ -- -- see: https://github.com/sol/hpack -- --- hash: 7287463c38f034c451472b16083a3110425f6ff06a3f8c12c27b8cf229f332e6 +-- hash: 182681ec85bce978c3cc8c3181ac70c130ce8d4102cf4076e965dd7287af2c0a name: tensor-safe -version: 0.1.0.0 +version: 0.1.0.1 synopsis: Create valid deep neural network architectures description: TensorSafe provides a very simple API to create deep neural networks structures which are validated using Dependent Types. Given a list of Layers and an initial Shape, TensorSafe is able to check and corroborate the structure of the network. Also, it's possible to extract the definition and compile it to a target language like Python and JavaScript. category: AI, Dependent Types, Language, Library, Program @@ -27,22 +27,6 @@ location: https://github.com/leopiney/tensor-safe library - hs-source-dirs: - src - ghc-options: -Wall -freduction-depth=0 - build-depends: - base >=4.7 && <5 - , casing >=0.1.4.0 && <0.1.5 - , cmdargs >=0.10.20 && <0.11 - , containers >=0.6.0.1 && <0.7 - , extra >=1.6 && <1.7 - , formatting >=6.3.6 && <6.4 - , ghc-typelits-extra >=0.3 && <0.4 - , hint >=0.9.0 && <1.0 - , singletons >=2.5.1 && <2.6 - , text >=1.2.3.1 && <1.3 - , vector >=0.12 && <0.13 - , vector-sized >1.2 && <1.3 exposed-modules: TensorSafe TensorSafe.Commands.Check @@ -53,21 +37,43 @@ TensorSafe.Core TensorSafe.Examples.Examples TensorSafe.Examples.MnistExample + TensorSafe.Examples.ResNet50Example TensorSafe.Examples.SimpleExample TensorSafe.Layer TensorSafe.Layers + TensorSafe.Layers.Add + TensorSafe.Layers.BatchNormalization TensorSafe.Layers.Conv2D TensorSafe.Layers.Dense TensorSafe.Layers.Dropout TensorSafe.Layers.Flatten + TensorSafe.Layers.GlobalAvgPooling2D + TensorSafe.Layers.Input TensorSafe.Layers.LSTM TensorSafe.Layers.MaxPooling TensorSafe.Layers.Relu TensorSafe.Layers.Sigmoid + TensorSafe.Layers.ZeroPadding2D TensorSafe.Network TensorSafe.Shape other-modules: Paths_tensor_safe + hs-source-dirs: + src + ghc-options: -Wall -freduction-depth=0 + build-depends: + base >=4.7 && <5 + , casing >=0.1.4.0 && <0.1.5 + , cmdargs >=0.10.20 && <0.11 + , containers >=0.6.0.1 && <0.7 + , extra >=1.6 && <1.7 + , formatting >=6.3.6 && <6.4 + , ghc-typelits-extra >=0.3 && <0.4 + , hint >=0.9.0 && <1.0 + , singletons >=2.5.1 && <2.6 + , text >=1.2.3.1 && <1.3 + , vector >=0.12 && <0.13 + , vector-sized >1.2 && <1.3 default-language: Haskell2010 executable tensor-safe