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 +30/−0
- README.md +152/−0
- Setup.hs +2/−0
- app/Main.hs +50/−0
- src/TensorSafe.hs +17/−0
- src/TensorSafe/Commands/Check.hs +18/−0
- src/TensorSafe/Commands/Compile.hs +36/−0
- src/TensorSafe/Commands/Examples.hs +14/−0
- src/TensorSafe/Commands/Utils.hs +21/−0
- src/TensorSafe/Compile/Expr.hs +168/−0
- src/TensorSafe/Core.hs +48/−0
- src/TensorSafe/Examples/Examples.hs +66/−0
- src/TensorSafe/Examples/MnistExample.hs +52/−0
- src/TensorSafe/Examples/SimpleExample.hs +45/−0
- src/TensorSafe/Layer.hs +26/−0
- src/TensorSafe/Layers.hs +20/−0
- src/TensorSafe/Layers/Conv2D.hs +46/−0
- src/TensorSafe/Layers/Dense.hs +31/−0
- src/TensorSafe/Layers/Dropout.hs +30/−0
- src/TensorSafe/Layers/Flatten.hs +19/−0
- src/TensorSafe/Layers/LSTM.hs +32/−0
- src/TensorSafe/Layers/MaxPooling.hs +37/−0
- src/TensorSafe/Layers/Relu.hs +14/−0
- src/TensorSafe/Layers/Sigmoid.hs +14/−0
- src/TensorSafe/Network.hs +284/−0
- src/TensorSafe/Shape.hs +93/−0
- tensor-safe.cabal +94/−0
+ 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