packages feed

tensor-safe (empty) → 0.1.0.0

raw patch · 27 files changed

+1459/−0 lines, 27 filesdep +basedep +casingdep +cmdargssetup-changed

Dependencies added: base, casing, cmdargs, containers, extra, formatting, ghc-typelits-extra, hint, singletons, tensor-safe, text, vector, vector-sized

Files

+ LICENSE view
@@ -0,0 +1,30 @@+Copyright Leonardo Pineyro (c) 2019++All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are met:++    * Redistributions of source code must retain the above copyright+      notice, this list of conditions and the following disclaimer.++    * Redistributions in binary form must reproduce the above+      copyright notice, this list of conditions and the following+      disclaimer in the documentation and/or other materials provided+      with the distribution.++    * Neither the name of Leonardo Pineyro nor the names of other+      contributors may be used to endorse or promote products derived+      from this software without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ README.md view
@@ -0,0 +1,152 @@+# Tensor Safe++`tensor-safe` is a dependently typed framework to define deep learning models which structure is verified on+compilation time. If the models are valid, these can be compiled to Keras framework in Python or JavaScript.++## Building instructions and development tools++1. Install `ghc-mod`, `hpack` and `stylish-haskell` with `stack install`++   ```+   cd ~+   stack install ghc-mod hpack stylish-haskell+   ```++2. Run `stack build` in project folder+3. Install `Intero`++   Run `stack build intero` in the project folder++   Ref: https://gitlab.com/vannnns/haskero/blob/master/client/doc/installation.md++## Generate `.cabal` file++Run `hpack` in the root of the project and the file `tensor-safe.cabal` will be generated++## Model definition++Models can be defined as a type using the `MkINetwork` type function. The `MkINetwork` defines a+valid instance of a Network model given a list of `Layers` and a spected input and iutput `Shapes`.++Here's an example of how to define a simple model for the `MNIST` dataset, using `Dense` layers:++```haskell+type MNIST = MkINetwork+    '[+        Flatten,+        Dense 784 42,+        Relu,+        Dense 42 10,+        Sigmoid+    ]+    ('D3 28 28 1)    -- Input+    ('D1 10)         -- Output+```++After that, variable with the model type can be verified with the function `mkINetwork` like this:++```haskell+mnist :: MNIST+mnist = mkINetwork+```++## Nesting networks definitions++You can nest networks definitions easily by adding the networks as layers. For example, in the case of the `MNIST` model defined above, we can abstract the use of Dense and a activation function like this:++```haskell+type DenseRelu i o =+    MkINetwork '[ Dense i o, Relu ] ('D1 i) ('D1 o)++type DenseSigmoid i o =+    MkINetwork '[ Dense i o, Sigmoid ] ('D1 i) ('D1 o)++type MNIST = MkINetwork+    '[+        Flatten,+        DenseRelu 784 42,+        DenseSigmoid 42 10+    ]+    ('D3 28 28 1)    -- Input+    ('D1 10)         -- Output+```++## Command line interface++> This interface will change in the near future++You can install `tensor-safe` command line tool by running `stack build`. Then you can use it by using `stack exec tensor-safe -- check --path ./path-to-model.hs` or `stack exec tensor-safe -- compile --path ./path-to-model.hs --module-name SomeModule`.++## Tools for JavaScript environment++Add as development dependency the packages `babel-plugin-tensor-safe` and `eslint-plugin-tensor-safe`. These can be found in the `extra/javascript` folder in this project.++You can add them directly from this project like this:++```bash+yarn add --dev file/:<path-to-tensor-safe>/extra/javascript/babel-plugin-tensor-safe++yarn add --dev file/:<path-to-tensor-safe>/extra/javascript/eslint-plugin-tensor-safe+```++Then add to the `.eslintrc.js` file in your JavaScript project the plugin `tensor-safe` and the rule `tensor-safe-model-invalid` like this:++```js+module.exports = {+  plugins: [+     ...+     "tensor-safe"+   ],+  ...+  rules: {+    ...+    "tensor-safe/invalid-model": 1+    ...+  }+};+```++And for the Babel plugin add `"@babel/plugin-tensor-safe"` to the plugins list in the `.babelrc` file inside your JavaScript project.++Then, you can write your deep learning model inside your JS files as in the following example:++```js+function createConvModel() {+  safeModel`+    '[+        Conv2D 1 16 3 3 1 1,+        Relu,+        MaxPooling 2 2 2 2,+        Conv2D 16 32 3 3 1 1,+        Relu,+        MaxPooling 2 2 2 2,+        Conv2D 32 32 3 3 1 1,+        Relu,+        Flatten,+        Dense 288 64,+        Sigmoid,+        Dense 64 10,+        Sigmoid+    ]+    ('D3 28 28 1)  -- Input+    ('D1 10)       -- Output+`;++  return model;+}+```++## Related projects++This project was highly influenciated by [Grenade](https://github.com/HuwCampbell/grenade) 💣.+Grenade is a really cool library to define deep neural networks which are validated using dependent types.+What differences TensorSafe from Grenade the most is that TensorSafe doesn't run nor train the models, instead+it compiles the model to external languages that are capable of performing all computations – like Keras+for Python or JavaScript. Also, TensorSafe doesn't need to specifically declare all Shapes transformations+for all the model layers, instead, it just needs the `input` and `output` Shapes to validate the model.++Another worth looking library is [TensorFlow for Haskell](https://github.com/tensorflow/haskell).+This library has all bindings for TensorFlow in C. The issue with this is that it doesn't perform+a lot of type checkings at compilation time. However, there's an open branch that uses dependent+types to solve many of these issues: https://github.com/helq/tensorflow-haskell-deptyped, but the+solution still seems rather complicated for real use.
+ Setup.hs view
@@ -0,0 +1,2 @@+import           Distribution.Simple+main = defaultMain
+ app/Main.hs view
@@ -0,0 +1,50 @@+{-# LANGUAGE DeriveDataTypeable #-}+module Main where++import           System.Console.CmdArgs++import           TensorSafe.Commands.Check    (check)+import           TensorSafe.Commands.Compile  (compile)+import           TensorSafe.Commands.Examples (examples)++data Backend = JavaScript | Python deriving (Data, Eq, Show, Typeable)++data TensorSafe = Check   { path :: FilePath }+                | Compile {+                    path        :: FilePath,+                    module_name :: String,+                    backend     :: Backend,+                    out         :: Maybe FilePath+                  }+                | Examples+                deriving (Data, Eq, Show, Typeable)++cCheck :: TensorSafe+cCheck = Check+    { path = def &= typ "PATH" &= help "Path to Haskell module with TensorSafe model inside"+    } &= help "Checks if a Neural Network model is valid or not"++cCompile :: TensorSafe+cCompile = Compile+    { path = def &= typ "PATH" &= help "Path to Haskell module with TensorSafe model inside"+    , module_name = def &= help "The module name inside the TensorSafe model file"+    , backend = enum+        [ JavaScript &= help "Compile to JavaScript backend"+        , Python     &= help "Compile to Python backend"]+    , out = def &= help "If specified, the output file path to which the network will be generated"+    } &= help "Compiles module and outputs Neural Network model for the specified backend"++cExamples :: TensorSafe+cExamples = Examples &= help "Show some examples"++tensorSafe :: IO TensorSafe+tensorSafe = cmdArgs (modes [cCompile, cCheck, cExamples])++main :: IO ()+main = do+    -- print =<< tensorSafe+    r <- tensorSafe+    case r of+        Check { path = p }                                           -> check p+        Compile { path = p, module_name = m, backend = b, out = o }  -> compile p m (show b) o+        Examples                                                     -> examples
+ src/TensorSafe.hs view
@@ -0,0 +1,17 @@+{-# LANGUAGE DataKinds           #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-| This module declares what is visible to use TensorSafe as an API. -}+module TensorSafe (+    JavaScript (..),+    Python (..),+    generate,+    generateFile,+    INetwork,+    MkINetwork,+    mkINetwork,+    toCNetwork+) where++import           TensorSafe.Compile.Expr+import           TensorSafe.Network      (INetwork, MkINetwork, mkINetwork,+                                          toCNetwork)
+ src/TensorSafe/Commands/Check.hs view
@@ -0,0 +1,18 @@+{-| This module provides checking and interpretation functions using the "hint" library. -}+module TensorSafe.Commands.Check (check) where++import           Language.Haskell.Interpreter+import           System.Exit++import           TensorSafe.Commands.Utils++-- | Checks if the file at the specified path compiles successfully.+check :: String -> IO ()+check path = do+    r <- runInterpreter $ loadModules [path]+    case r of+        Left err -> do+            putStrLn $ errorString err+            exitWith $ ExitFailure 1+        Right () -> do+            exitWith $ ExitSuccess
+ src/TensorSafe/Commands/Compile.hs view
@@ -0,0 +1,36 @@+{-| This module provides compilation and interpretation functions using the "hint" library. -}+module TensorSafe.Commands.Compile (compile) where++import           Language.Haskell.Interpreter+import           System.Exit++import           TensorSafe.Commands.Utils++-- | Compilation interface for the `compile` command. Given a path, module name.+compile :: String -> String -> String -> Maybe FilePath -> IO ()+compile path moduleName backend out = do+    r <- runInterpreter $ checkAndCompile path moduleName backend out+    case r of+        Left err -> do+            putStrLn $ errorString err+            exitWith $ ExitFailure 1+        Right () -> do+            exitWith $ ExitSuccess++-- | Invokes `Language.Haskell.Interpreter` to generate the CNetwork in the file with the specified+-- path.+-- Depending on the out parameter, the output will be redirected to the stdout or the the out+-- path.+checkAndCompile :: String -> String -> String -> Maybe FilePath -> Interpreter ()+checkAndCompile path moduleName backend out = do+    loadModules [path]+    setTopLevelModules [moduleName]+    setImportsQ [("TensorSafe", Nothing), ("Data.Text.Lazy", Nothing)]++    case out of+        Nothing -> do+            r <- interpret ("unpack $ generate " ++ backend ++ " (toCNetwork nn)") (as :: String)+            liftIO $ putStrLn r+        Just f -> do+            r <- interpret ("unpack $ generateFile " ++ backend ++ " (toCNetwork nn)") (as :: String)+            liftIO $ writeFile f r
+ src/TensorSafe/Commands/Examples.hs view
@@ -0,0 +1,14 @@+{-| This module implements the examples command for TensorSafe. -}+module TensorSafe.Commands.Examples (examples) where++import           TensorSafe.Examples.Examples++-- | Outputs to stdout the results of the examples+examples :: IO ()+examples = do+    simpleExample+    putStrLn $ "\n\n"+    mnistExample+    putStrLn $ "\n\n"+    mnistExampleDense+
+ src/TensorSafe/Commands/Utils.hs view
@@ -0,0 +1,21 @@+{-| This module provides simple IO functions to operate with command line programs. -}+module TensorSafe.Commands.Utils (+    errorString,+    say+) where++import           Data.List+import           Language.Haskell.Interpreter++-- | Transforms an InterpreterError into a string.+errorString :: InterpreterError -> String+errorString (WontCompile es) =+    intercalate "\n" (header : map unbox es)+    where+        header = "Compilation error:"+        unbox (GhcError e) = e+errorString e = show e++-- | Lifts putStrLn to the Interpreter.+say :: String -> Interpreter ()+say = liftIO . putStrLn
+ src/TensorSafe/Compile/Expr.hs view
@@ -0,0 +1,168 @@+{-# LANGUAGE OverloadedStrings #-}+{-| This module describes the expression structure of a INetwork instance.+-- The INetwork can be structured into a Data structure called CNetwork, with which later+-- to compilation external languages can be done.+-}+module TensorSafe.Compile.Expr (+    DLayer (..),+    CNetwork (..),+    JavaScript (..),+    Python (..),+    Generator,+    generate,+    generateFile+) where++import           Data.Map+import           Data.Text.Lazy as T+import           Formatting+import           Text.Casing    (camel, quietSnake)++-- | 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+            | DDense+            | DDropout+            | DFlatten+            | DLSTM+            | DMaxPooling+            | DRelu+            | DActivation+            deriving Show++-- | Defines the+data CNetwork = CNSequence CNetwork+              | CNCons CNetwork CNetwork+              | CNLayer DLayer (Map String String)+              | CNReturn  -- End of initial sequence network+              | CNNil     -- End of possible nested sequence networks+              deriving Show++-- | Support for JavaScript compilation+data JavaScript = JavaScript deriving Show++-- | Support for Python compilation+data Python = Python deriving Show++-- | Defines how are the layers going to be translated to the domain language+-- This translates DLayer to String for each supported language+class LayerGenerator l where+    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"++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"++-- | Class that defines which languages are supported for CNetworks generation to text+class Generator l where++    -- | Adds supports for a language. Generates a CNetwork to Text+    generate :: l -> CNetwork -> Text++    -- | Similar to 'generate', but also adds necessary header and module lines of text so as to+    -- have the CNetwork compiled at a separate file.+    generateFile :: l -> CNetwork -> Text++instance Generator JavaScript where+    generate l =+        T.intercalate "\n" . generateJS+        where+            generateJS :: CNetwork -> [Text]+            generateJS (CNSequence cn)  = ["var model = tf.sequential();"] ++ generateJS cn+            generateJS (CNCons cn1 cn2) = (generateJS cn1) ++ (generateJS cn2)+            generateJS CNNil = []+            generateJS CNReturn = []+            generateJS (CNLayer layer params) =+                [format+                    ("model.add(tf.layers." % string % "(" % string % "));")+                    (generateName l layer)+                    (paramsToJS params)+                ]++    generateFile l cn =+        startCode `append` (generate l cn) `append` endCode+        where+            startCode :: Text+            startCode = T.intercalate "\n"+                [ "// Autogenerated code"+                , "var tf = require(\"@tensorflow/tfjs\");"+                , "function model() {"+                , "\n"+                ]++            endCode :: Text+            endCode = T.intercalate "\n"+                [ "\n"+                , "return model;"+                , "}"+                , "\n"+                , "module.exports = model();"+                ]++-- | Converts a map to a parameter object in JavaScript+paramsToJS :: Map String String -> String+paramsToJS m =+    (foldrWithKey showParam "{ " m) ++ "}"+    where+        showParam :: String -> String -> String -> String+        showParam key value accum = accum ++ (camel key) ++ ": " ++ value ++ ", "++instance Generator Python where+    generate l =+        T.intercalate "\n" . generatePy+        where+            generatePy :: CNetwork -> [Text]+            generatePy (CNSequence cn)  = ["model = tf.keras.models.Sequential()"] ++ generatePy cn+            generatePy (CNCons cn1 cn2) = (generatePy cn1) ++ (generatePy cn2)+            generatePy CNNil = []+            generatePy CNReturn = []+            generatePy (CNLayer layer params) =+                [format+                    ("model.add(tf.layers." % string % "(" % string % "))")+                    (generateName l layer)+                    (paramsToPython params)]++    generateFile l cn =+        startCode `append` (generate l cn)+        where+            startCode :: Text+            startCode = T.intercalate "\n"+                [ "// Autogenerated code"+                , "import tensorflow as tf"+                , "\n"+                ]++-- | Converts a map to keyword arguments in Python+paramsToPython :: Map String String -> String+paramsToPython =+    foldrWithKey showParam ""+    where+        showParam :: String -> String -> String -> String+        showParam key value accum = accum ++ (transform key) ++ "=" ++ value ++ ", "++        -- | Translates keys to python keys of layers+        --+        --   There are some minor changes in names of keys for layers with respect to JS.+        --   Those changes should be delcared here. For most of the keys, transforming them to+        --   snake case does the trick.+        transform :: String -> String+        transform key+            | key == "inputDim" = "input_shape"+            | otherwise         = quietSnake key
+ src/TensorSafe/Core.hs view
@@ -0,0 +1,48 @@+{-# LANGUAGE DataKinds            #-}+{-# LANGUAGE GADTs                #-}+{-# LANGUAGE TypeFamilies         #-}+{-# LANGUAGE TypeOperators        #-}+{-# LANGUAGE UndecidableInstances #-}+{-| This module adds some meaningfull type operations that are of use throughout all the project.+-}+module TensorSafe.Core where++import           Data.Kind    (Type)+import           GHC.TypeLits as N++-- | Multiplies all numbers on a list of natural numbers+type family ShapeProduct (s :: [Nat]) :: Nat where+    ShapeProduct '[] = 1+    ShapeProduct (m ': s) = m N.* (ShapeProduct s)++-- | Compares two types in kinds level+type family TypeEquals (s1 :: Type) (s2 :: Type) :: Bool where+    TypeEquals s s = 'True+    TypeEquals _ _ = 'False++-- | Compares two types in kinds level and raises error if they don't match+type family TypeEquals' s1 s2 :: Type where+    TypeEquals' s s = s+    TypeEquals' s1 s2 =+        TypeError ( 'Text "Couldn't match the type "+              ':<>: 'ShowType s1+              ':<>: 'Text " with type "+              ':<>: 'ShowType s2)++-- | Wrapper for a Nat value+data R (n :: Nat) where+    R :: (KnownNat n) => R n++instance KnownNat n => Show (R n) where+    -- show = show . typeOf+    show n = show (natVal n)++-- | Wrapper for a tuple of 2 Nat values+data L (m :: Nat) (n :: Nat) where+    L :: (KnownNat m, KnownNat n) => L m n++instance (KnownNat m, KnownNat n) => Show (L m n) where+    -- show = show . typeOf+    show n = show (natVal n)++
+ src/TensorSafe/Examples/Examples.hs view
@@ -0,0 +1,66 @@+{-# LANGUAGE DataKinds           #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-| This module wraps all examples in simple fuctions. -}+module TensorSafe.Examples.Examples (+    mnistExample,+    mnistExampleDense,+    simpleExample+) where++import           Data.Text.Lazy                    (unpack)++import           TensorSafe.Compile.Expr           (JavaScript (..), generate)+import           TensorSafe.Examples.MnistExample+import           TensorSafe.Examples.SimpleExample+import           TensorSafe.Network                (toCNetwork)+++-- | Puts simple examples results to stdout+simpleExample :: IO ()+simpleExample =+    do+        putStrLn $ "Simple network example"+        putStrLn $ "----------------------"+        putStrLn $ show myNet+        putStrLn $ "Simple network example"+        putStrLn $ "----------------------"+        putStrLn $ show myNet2+        putStrLn $ "Simple network example"+        putStrLn $ "----------------------"+        putStrLn $ show myNet3+        putStrLn $ "Simple LSTM network example"+        putStrLn $ "----------------------"+        putStrLn $ show lstm++-- | Puts MNIST examples results to stdout+mnistExample :: IO ()+mnistExample =+    do+        putStrLn $ "MNIST example"+        putStrLn $ "-------------"+        putStrLn $ show mnist+        putStrLn $ "\n"+        putStrLn $ "MNIST compilation"+        putStrLn $ "-------------"+        putStrLn $ show (toCNetwork mnist)+        putStrLn $ "\n"+        putStrLn $ "MNIST generation"+        putStrLn $ "-------------"+        putStrLn $ unpack $ generate JavaScript (toCNetwork mnist)++-- | Puts MNIST Dense examples results to stdout+mnistExampleDense :: IO ()+mnistExampleDense =+    do+        putStrLn $ "MNIST Dense example"+        putStrLn $ "-------------"+        putStrLn $ show mnistDense+        putStrLn $ "\n"+        putStrLn $ "MNIST compilation"+        putStrLn $ "-------------"+        putStrLn $ show (toCNetwork mnistDense)+        putStrLn $ "\n"+        putStrLn $ "MNIST generation"+        putStrLn $ "-------------"+        putStrLn $ unpack $ generate JavaScript (toCNetwork mnistDense)+
+ src/TensorSafe/Examples/MnistExample.hs view
@@ -0,0 +1,52 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE GADTs     #-}+{-| This module implements the MNIST examples using Convs and Dense layers. -}+module TensorSafe.Examples.MnistExample (+    mnist,+    mnistDense+) where++import           TensorSafe.Layers+import           TensorSafe.Network (MkINetwork, mkINetwork)+import           TensorSafe.Shape++type DenseRelu i o =+    MkINetwork '[ Dense i o, Relu ] ('D1 i) ('D1 o)++type DenseSigmoid i o =+    MkINetwork '[ Dense i o, Sigmoid ] ('D1 i) ('D1 o)++type MNIST = MkINetwork+    '[+        Conv2D 1 16 3 3 1 1,+        Relu,+        MaxPooling 2 2 2 2,+        Conv2D 16 32 3 3 1 1,+        Relu,+        MaxPooling 2 2 2 2,+        Conv2D 32 32 3 3 1 1,+        Relu,+        Flatten,+        DenseSigmoid 288 64,+        DenseSigmoid 64 10+    ]+    ('D3 28 28 1)    -- Input+    ('D1 10)       -- Output++-- | MNIST implementation using Convolutional layers+mnist :: MNIST+mnist = mkINetwork+++type MNISTDense = MkINetwork+    '[+        Flatten,+        DenseRelu 784 42,+        DenseSigmoid 42 10+    ]+    ('D3 28 28 1)    -- Input+    ('D1 10)       -- Output++-- | MNIST implementation using just Dense layers+mnistDense :: MNISTDense+mnistDense = mkINetwork
+ src/TensorSafe/Examples/SimpleExample.hs view
@@ -0,0 +1,45 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE GADTs     #-}+{-| This module implements a very simple example of a deep neural network. -}+module TensorSafe.Examples.SimpleExample (+    myNet,+    myNet2,+    myNet3,+    lstm+) where+++import           TensorSafe        (MkINetwork, mkINetwork)+import           TensorSafe.Layers+import           TensorSafe.Shape++type MyNet = MkINetwork '[ Sigmoid, Flatten, Relu, Flatten ] ('D2 28 28) ('D1 784)++-- | Simple network example+myNet :: MyNet+myNet = mkINetwork++type MyNet2 = MkINetwork '[ Sigmoid, Flatten, Dense 784 80, Relu, Flatten ] ('D2 28 28) ('D1 80)++-- | Simple network example+myNet2 :: MyNet2+myNet2 = mkINetwork++-- | Simple network example+myNet3 :: MkINetwork+    '[+        MaxPooling 2 2 2 2,+        Flatten,+        Dense 196 10,+        Sigmoid,+        Relu+    ]+    ('D2 28 28)+    ('D1 10)+myNet3 = mkINetwork++type MyLSTM = MkINetwork '[LSTM 8 'True] ('D2 10 20) ('D2 10 8)++-- | Simple LSTM network example+lstm :: MyLSTM+lstm = mkINetwork
+ src/TensorSafe/Layer.hs view
@@ -0,0 +1,26 @@+{-| This module defines the Layer class from which all Layers should have instances of. -}+module TensorSafe.Layer (+    InputShape,+    Layer,+    compile,+    layer+) where++import           Data.Maybe              ()++import           TensorSafe.Compile.Expr++-- | Auxiliary type for Input Shape parameter+type InputShape = Maybe String++-- | Defines that a type is a Layer+--   Each layer can be compilated into a specific CNetwork expression which can later be used+--   to generate code to a specific backend.+class Layer x where+    -- | The layer type+    layer :: x++    -- | Given the layer and a optional inputShape generates a CNetwork structure+    compile :: x -> InputShape -> CNetwork++    {-# MINIMAL compile, layer #-}
+ src/TensorSafe/Layers.hs view
@@ -0,0 +1,20 @@+{-| This module exposes all Layers declared at TensorSafe.Layers. -}+module TensorSafe.Layers (+    Conv2D,+    Dense,+    Dropout,+    Flatten,+    LSTM,+    MaxPooling,+    Relu,+    Sigmoid+) where++import           TensorSafe.Layers.Conv2D+import           TensorSafe.Layers.Dense+import           TensorSafe.Layers.Dropout+import           TensorSafe.Layers.Flatten+import           TensorSafe.Layers.LSTM+import           TensorSafe.Layers.MaxPooling+import           TensorSafe.Layers.Relu+import           TensorSafe.Layers.Sigmoid
+ src/TensorSafe/Layers/Conv2D.hs view
@@ -0,0 +1,46 @@+{-# LANGUAGE DataKinds           #-}+{-# LANGUAGE GADTs               #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeFamilies        #-}+{-| This module declares the 2D convolutional layer data type. -}+module TensorSafe.Layers.Conv2D where++import           Data.Kind               (Type)+import           Data.Map+import           Data.Proxy+import           GHC.TypeLits++import           TensorSafe.Compile.Expr+import           TensorSafe.Layer+++-- | A 2D Convolutional layer+data Conv2D :: Nat -> Nat -> Nat -> Nat -> Nat -> Nat -> Type where+    Conv2D :: Conv2D channels filters kernelRows kernelColumns strideRows strideColumns+    deriving Show++instance ( KnownNat channels+         , KnownNat filters+         , KnownNat kernelRows+         , KnownNat kernelColumns+         , KnownNat strideRows+         , KnownNat strideColumns+         ) => Layer (Conv2D channels filters kernelRows kernelColumns strideRows strideColumns) where+    layer = Conv2D+    compile _ inputShape =+        let filters = natVal (Proxy :: Proxy filters)+            kernelRows = natVal (Proxy :: Proxy kernelRows)+            kernelColumns = natVal (Proxy :: Proxy kernelColumns)+            strideRows = natVal (Proxy :: Proxy strideRows)+            strideColumns = natVal (Proxy :: Proxy strideColumns)++            initialParams = case inputShape of+                Just shape -> fromList [("inputShape", shape)]+                Nothing    -> empty+            params = union initialParams (fromList [+                    ("kernelSize", show [kernelRows, kernelColumns]),+                    ("filters", show filters),+                    ("strides", show [strideRows, strideColumns])+                ])+        in+            CNLayer DConv2D params
+ src/TensorSafe/Layers/Dense.hs view
@@ -0,0 +1,31 @@+{-# LANGUAGE DataKinds           #-}+{-# LANGUAGE GADTs               #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeFamilies        #-}+{-| This module declares the Dense, a.k.a. FullyConnected, layer data type. -}+module TensorSafe.Layers.Dense where++import           Data.Kind               (Type)+import           Data.Map+import           Data.Proxy+import           GHC.TypeLits++import           TensorSafe.Compile.Expr+import           TensorSafe.Layer+++-- | A classic Dense, or FullyConnected, layer with input and output parameters.+data Dense :: Nat -> Nat -> Type where+    Dense :: Dense input output+    deriving Show++instance (KnownNat input, KnownNat output) => Layer (Dense input output) where+    layer = Dense+    compile _ _ =+        let input = show $ natVal (Proxy :: Proxy input)+            output = show $ natVal (Proxy :: Proxy output)+        in+            CNLayer DDense (fromList [+              ("inputDim", input),+              ("units", output)+            ])
+ src/TensorSafe/Layers/Dropout.hs view
@@ -0,0 +1,30 @@+{-# LANGUAGE DataKinds           #-}+{-# LANGUAGE GADTs               #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeFamilies        #-}+{-| This module declares the Dropout layer data type. -}+module TensorSafe.Layers.Dropout (Dropout) where++import           Data.Kind               (Type)+import           Data.Map+import           Data.Proxy+import           GHC.TypeLits++import           TensorSafe.Compile.Expr+import           TensorSafe.Layer++-- | A Dropout layer with rate and seed arguments+data Dropout :: Nat -> Nat -> Type where+    Dropout :: Dropout rate seed+    deriving Show++instance (KnownNat rate, KnownNat seed) => Layer (Dropout rate seed) where+    layer = Dropout+    compile _ _ =+        let rate = show $ natVal (Proxy :: Proxy rate)+            seed = show $ natVal (Proxy :: Proxy seed)+        in+            CNLayer DDropout (fromList [+                ("rate", rate),+                ("seed", seed)+            ])
+ src/TensorSafe/Layers/Flatten.hs view
@@ -0,0 +1,19 @@+{-| This module declares the Flatten layer data type. -}+module TensorSafe.Layers.Flatten (Flatten) where++import           Data.Map++import           TensorSafe.Compile.Expr+import           TensorSafe.Layer++-- | Flattens the dimensions of the shapes to a list of values with shape D1+data Flatten = Flatten deriving Show++instance Layer Flatten where+    layer = Flatten+    compile _ inputShape =+        let params = case inputShape of+                        Just shape -> fromList [("inputShape", shape)]+                        Nothing    -> empty+        in+            CNLayer DFlatten params
+ src/TensorSafe/Layers/LSTM.hs view
@@ -0,0 +1,32 @@+{-# LANGUAGE DataKinds           #-}+{-# LANGUAGE GADTs               #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeFamilies        #-}+{-| This module declares the classing LSTM layer data type. -}+module TensorSafe.Layers.LSTM where++import           Data.Kind               (Type)+import           Data.Map+import           Data.Proxy+import           GHC.TypeLits++import           TensorSafe.Compile.Expr+import           TensorSafe.Layer+++-- | A LSTM layer with a number of units and a option to return the original sequences.+data LSTM :: Nat -> Bool -> Type where+    LSTM :: LSTM units returnSequences+    deriving Show++instance (KnownNat units) => Layer (LSTM units b) where+    layer = LSTM+    compile _ _ =+        let units = show $ natVal (Proxy :: Proxy units)+            returnSequences = show $ (Proxy :: Proxy returnSequences)+        in+            CNLayer DLSTM (fromList [+                ("units", units),+                ("returnSequences", returnSequences)+            ])+
+ src/TensorSafe/Layers/MaxPooling.hs view
@@ -0,0 +1,37 @@+{-# LANGUAGE DataKinds           #-}+{-# LANGUAGE GADTs               #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeFamilies        #-}+{-| This module declares the 2D MaxPooling layer data type. -}+module TensorSafe.Layers.MaxPooling where++import           Data.Kind               (Type)+import           Data.Map+import           Data.Proxy+import           GHC.TypeLits++import           TensorSafe.Compile.Expr+import           TensorSafe.Layer++-- | A 2D MaxPooling pooling that works for D2 and D3 shapes+data MaxPooling :: Nat -> Nat -> Nat -> Nat -> Type where+    MaxPooling :: MaxPooling kernelRows kernelColumns strideRows strideColumns+    deriving Show++instance ( KnownNat kernelRows+         , KnownNat kernelColumns+         , KnownNat strideRows+         , KnownNat strideColumns+         ) => Layer (MaxPooling kernelRows kernelColumns strideRows strideColumns) where+    layer = MaxPooling+    compile _ _ =+        let kernelRows = natVal (Proxy :: Proxy kernelRows)+            kernelColumns = natVal (Proxy :: Proxy kernelColumns)+            strideRows = natVal (Proxy :: Proxy strideRows)+            strideColumns = natVal (Proxy :: Proxy strideColumns)+        in+            CNLayer DMaxPooling (+                fromList [+                    ("poolSize", show [kernelRows, kernelColumns]),+                    ("strides", show [strideRows, strideColumns])+                ])
+ src/TensorSafe/Layers/Relu.hs view
@@ -0,0 +1,14 @@+{-| This module declares the ReLu activation layer data type. -}+module TensorSafe.Layers.Relu (Relu) where++import           Data.Map++import           TensorSafe.Compile.Expr+import           TensorSafe.Layer++-- | A ReLu activation function+data Relu = Relu deriving Show++instance Layer Relu where+    layer = Relu+    compile _ _ = CNLayer DRelu empty
+ src/TensorSafe/Layers/Sigmoid.hs view
@@ -0,0 +1,14 @@+{-| This module declares the Sigmoid activation layer data type. -}+module TensorSafe.Layers.Sigmoid (Sigmoid) where++import           Data.Map++import           TensorSafe.Compile.Expr+import           TensorSafe.Layer++-- | A Sigmoid activation function+data Sigmoid = Sigmoid deriving Show++instance Layer Sigmoid where+    layer = Sigmoid+    compile _ _ = CNLayer DActivation (fromList [("activation", "\"sigmoid\"")])
+ src/TensorSafe/Network.hs view
@@ -0,0 +1,284 @@+{-# LANGUAGE DataKinds             #-}+{-# LANGUAGE FlexibleContexts      #-}+{-# LANGUAGE FlexibleInstances     #-}+{-# LANGUAGE GADTs                 #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE ScopedTypeVariables   #-}+{-# LANGUAGE TypeFamilies          #-}+{-# LANGUAGE TypeOperators         #-}+{-# LANGUAGE UndecidableInstances  #-}+{-# OPTIONS_GHC -fplugin GHC.TypeLits.Extra.Solver #-}+{-| 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.+-}+module TensorSafe.Network (+    Network (..),+    INetwork (..),+    MkINetwork,+    ValidNetwork,+    mkINetwork,+    toCNetwork+) where++import           Data.Kind               (Type)+import           Data.Singletons+import           GHC.TypeLits            as N+import           GHC.TypeLits.Extra      (Div)++import           TensorSafe.Compile.Expr+import           TensorSafe.Layer        (Layer, compile, layer)+import           TensorSafe.Layers+import           TensorSafe.Shape++-- | A network that defines a specific sequence of layers+data Network :: [Type] -> Type where+  NNil  :: Network '[]++  (:~~) :: Layer x+        => !x+        -> !(Network xs)+        -> Network (x ': xs)+infixr 5 :~~++instance Show (Network '[]) where+    show NNil = "NNil"++instance (Show x, Show (Network xs)) => Show (Network (x ': xs)) where+    show (x :~~ xs) = show x ++ "\n :~~ " ++ show xs++-- | 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`.+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)+infixr 5 :~>++instance Show (INetwork '[] '[i]) where+    show INNil = "NNil"++instance (Show x, Show (INetwork xs rs)) => Show (INetwork (x ': xs) (i ': rs)) where+    show (x :~> xs) = show x ++ "\n :~> " ++ show xs++-- | This instance of INetwork as a Layer makes possible nesting INetworks+instance ValidNetwork ls ss => Layer (INetwork ls ss) where+    layer = mkINetwork+    compile n i = toCNetwork' n True i++--+-- COMPUTING RESULTING SHAPES FROM A LIST OF LAYERS.+--++-- | 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].+type family ComputeOut (layers :: [Type]) (s :: Shape) :: Shape where+    ComputeOut '[] s      = s+    ComputeOut (l : ls) s = ComputeOut ls (Out l s)++-- | 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.+type family ComposeOut' (layers :: [Type]) (s :: Shape) :: [Shape] where+    ComposeOut' '[] s      = '[]+    ComposeOut' (l : ls) s = ((Out l s) ': (ComposeOut' ls (Out l s)))++-- | Same than ComposeOut' but the Shape list includes the initial Shape+type family ComposeOut (layers :: [Type]) (s :: Shape) :: [Shape] where+    ComposeOut '[] s = '[]+    ComposeOut ls s  = s ': (ComposeOut' ls s)++-- | Compares the layers shape computation and the expected output+type family ValidateOutput (layers :: [Type]) (sIn :: Shape) (sOut :: Shape) :: Bool where+    ValidateOutput ls sIn sOut = ShapeEquals' (ComputeOut ls sIn) sOut++--+-- CREATE INETWORK TYPE INSTANCES FROM LIST OF LAYERS AND INTIAL AND ENDING SHAPES+--++-- | Creates an INetwork type, and by "unconstrained" I mean that I don't check for an+--   expected output+type family MkINetworkUnconstrained (layers :: [Type]) (s :: Shape) :: Type where+    MkINetworkUnconstrained ls s = INetwork ls (ComposeOut ls s)++-- | 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 MaybeType (t :: Type) (b :: Bool) :: Type where+    MaybeType t 'False = Type -- HACK: ValidateOutput should raise an exception on this case+    MaybeType t 'True  = t++-- | Creates an INetwork type validating the the expected output and the computed one match.+type family MkINetwork (layers :: [Type]) (sIn :: Shape) (sOut :: Shape) :: Type where+    MkINetworkUnconstrained ls sIn sOut =+        MaybeType (INetwork ls (ComposeOut ls sIn)) (ValidateOutput ls sIn sOut)++--+-- MAPPING TRANSFORMATIONS OF LAYERS AND SHAPES+--++-- | 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+    --+    --+    --+    Out (INetwork ls (s : ss)) s = ComputeOut ls 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 N.* y)+    Out Flatten ('D3 x y z) = 'D1 (x N.* y N.* z)++    --+    --+    --+    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++    --+    -- Edge case or not defined raise an error+    --+    Out l sOut =+        TypeError ( 'Text "Couldn't apply the Layer \""+                ':<>: 'ShowType l+                ':<>: 'Text "\" with the output Shape \""+                ':<>: 'ShowType sOut+                ':<>: 'Text "\"")++--+-- INETWORK VALIDATION+--++-- | 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+--   ```+class ValidNetwork (xs :: [Type]) (ss :: [Shape]) where++    -- | Makes a valid instance of INetwork+    mkINetwork :: INetwork xs ss++    {-# MINIMAL mkINetwork #-}++instance (SingI i) => ValidNetwork '[] '[i] where+    mkINetwork = INNil++instance ( SingI i+         , SingI o+         , Layer x+         , ValidNetwork xs (o ': rs)+         , (Out x i) ~ o -- IMPORTANT: validation that the output and the computation of the layer+                         -- will match. Without this constraint we could be able to create an+                         -- instance of ValidNetwork that doesn't satisfies the type constraints+                         -- of MkINetwork for example.+      ) => ValidNetwork (x ': xs) (i ': o ': rs) where+    mkINetwork = layer :~> mkINetwork++--+-- INETWORK MAPPING TO 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 ::+    forall i x xs ss. ( SingI i+                      , Layer x+                      , ValidNetwork (x ': xs) (i ': ss)) => INetwork (x ': xs) (i ': ss) -> CNetwork+toCNetwork n =+    case (sing :: Sing i) of+        D1Sing a     -> CNSequence (toCNetwork' n False (Just $ show [ natVal a]))++        D2Sing a b   -> CNSequence (toCNetwork' n False (Just $ show [ natVal a+                                                                     , natVal b]))++        D3Sing a b c -> CNSequence (toCNetwork' n False (Just $ show [ natVal a+                                                                     , natVal b+                                                                     , natVal c]))+-- | Helper function for `toCNetwork`+toCNetwork' :: INetwork xs ss -> Bool -> Maybe String -> CNetwork+toCNetwork' INNil nested _ =+    if nested+        then CNNil+        else CNReturn+toCNetwork' (l :~> n) nested inputShape =+    let compilatedLayer = compile l inputShape+        compilatedNetwork = toCNetwork' n nested Nothing+    in CNCons compilatedLayer compilatedNetwork
+ src/TensorSafe/Shape.hs view
@@ -0,0 +1,93 @@+{-# LANGUAGE CPP                  #-}+{-# LANGUAGE DataKinds            #-}+{-# LANGUAGE FlexibleContexts     #-}+{-# LANGUAGE GADTs                #-}+{-# LANGUAGE KindSignatures       #-}+{-# LANGUAGE StandaloneDeriving   #-}+{-# LANGUAGE TypeFamilies         #-}+{-# LANGUAGE TypeOperators        #-}+{-# LANGUAGE UndecidableInstances #-}+{-| This module declares all Shape related functions and data structures, as well as all singleton+-- instances for the Shape data type. This module was highly influenciated by Grenade, a Haskell+-- library for deep learning with dependent types. See: https://github.com/HuwCampbell/grenade+-}+module TensorSafe.Shape where++import           Data.Singletons+import           GHC.TypeLits    as N++import           TensorSafe.Core++--+-- Shape definition as in Haskell's Grenade library+--++-- | The current shapes we accept.+--   at the moment this is just one, two, and three dimensional+--   Vectors/Matricies.+--+--   These are only used with DataKinds, as Kind `Shape`, with Types 'D1, 'D2, 'D3.+data Shape+    = D1 Nat+    -- ^ One dimensional vector+    | D2 Nat Nat+    -- ^ Two dimensional matrix. Row, Column.+    | D3 Nat Nat Nat+    -- ^ Three dimensional matrix. Row, Column, Channels.++-- | Concrete data structures for a Shape.+--+--   All shapes are held in contiguous memory.+--   3D is held in a matrix (usually row oriented) which has height depth * rows.+data S (n :: Shape) where+    S1D :: ( KnownNat len )+        => R len+        -> S ('D1 len)++    S2D :: ( KnownNat rows, KnownNat columns )+        => L rows columns+        -> S ('D2 rows columns)++    S3D :: ( KnownNat rows+            , KnownNat columns+            , KnownNat depth+            , KnownNat (rows N.* depth))+        => L (rows N.* depth) columns+        -> S ('D3 rows columns depth)++deriving instance Show (S n)++-- Singleton instances.+-- Check: http://hackage.haskell.org/package/singletons+--+-- These could probably be derived with template haskell, but this seems+-- clear and makes adding the KnownNat constraints simple.+-- We can also keep our code TH free, which is great.+data instance Sing (n :: Shape) where+    D1Sing :: KnownNat a => Sing a -> Sing ('D1 a)+    D2Sing :: (KnownNat a, KnownNat b) => Sing a -> Sing b -> Sing ('D2 a b)+    D3Sing :: (KnownNat a, KnownNat b, KnownNat c) => Sing a -> Sing b -> Sing c -> Sing ('D3 a b c)++instance KnownNat a => SingI ('D1 a) where+    sing = D1Sing sing++instance (KnownNat a, KnownNat b) => SingI ('D2 a b) where+    sing = D2Sing sing sing++instance (KnownNat a, KnownNat b, KnownNat c) => SingI ('D3 a b c) where+    sing = D3Sing sing sing sing++-- | Compares two Shapes at kinds level and returns a Bool kind+type family ShapeEquals (sIn :: Shape) (sOut :: Shape) :: Bool where+    ShapeEquals s s = 'True+    ShapeEquals _ _ = 'False++-- | Same as ShapeEquals, which compares two Shapes at kinds level, but raises a TypeError exception+-- if the Shapes are not the equal.+type family ShapeEquals' (sIn :: Shape) (sOut :: Shape) :: Bool where+    ShapeEquals' s s = 'True+    ShapeEquals' s1 s2 =+        TypeError ( 'Text "Couldn't match the Shape "+              ':<>: 'ShowType s1+              ':<>: 'Text " with the Shape "+              ':<>: 'ShowType s2)
+ tensor-safe.cabal view
@@ -0,0 +1,94 @@+cabal-version: 1.12++-- This file has been generated from package.yaml by hpack version 0.31.1.+--+-- see: https://github.com/sol/hpack+--+-- hash: 7287463c38f034c451472b16083a3110425f6ff06a3f8c12c27b8cf229f332e6++name:           tensor-safe+version:        0.1.0.0+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+homepage:       https://github.com/leopiney/tensor-safe#readme+bug-reports:    https://github.com/leopiney/tensor-safe/issues+author:         Leonardo Pineyro+maintainer:     leopiney@gmail.com+copyright:      2019 Leonardo Pineyro+license:        BSD3+license-file:   LICENSE+build-type:     Simple+extra-source-files:+    README.md++source-repository head+  type: git+  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+      TensorSafe.Commands.Compile+      TensorSafe.Commands.Examples+      TensorSafe.Commands.Utils+      TensorSafe.Compile.Expr+      TensorSafe.Core+      TensorSafe.Examples.Examples+      TensorSafe.Examples.MnistExample+      TensorSafe.Examples.SimpleExample+      TensorSafe.Layer+      TensorSafe.Layers+      TensorSafe.Layers.Conv2D+      TensorSafe.Layers.Dense+      TensorSafe.Layers.Dropout+      TensorSafe.Layers.Flatten+      TensorSafe.Layers.LSTM+      TensorSafe.Layers.MaxPooling+      TensorSafe.Layers.Relu+      TensorSafe.Layers.Sigmoid+      TensorSafe.Network+      TensorSafe.Shape+  other-modules:+      Paths_tensor_safe+  default-language: Haskell2010++executable tensor-safe+  main-is: Main.hs+  other-modules:+      Paths_tensor_safe+  hs-source-dirs:+      app+  ghc-options: -Wall -freduction-depth=0 -threaded -rtsopts -with-rtsopts=-N+  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+    , tensor-safe+    , text >=1.2.3.1 && <1.3+    , vector >=0.12 && <0.13+    , vector-sized >1.2 && <1.3+  default-language: Haskell2010