diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -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.
diff --git a/README.md b/README.md
new file mode 100644
--- /dev/null
+++ b/README.md
@@ -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.
diff --git a/Setup.hs b/Setup.hs
new file mode 100644
--- /dev/null
+++ b/Setup.hs
@@ -0,0 +1,2 @@
+import           Distribution.Simple
+main = defaultMain
diff --git a/app/Main.hs b/app/Main.hs
new file mode 100644
--- /dev/null
+++ b/app/Main.hs
@@ -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
diff --git a/src/TensorSafe.hs b/src/TensorSafe.hs
new file mode 100644
--- /dev/null
+++ b/src/TensorSafe.hs
@@ -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)
diff --git a/src/TensorSafe/Commands/Check.hs b/src/TensorSafe/Commands/Check.hs
new file mode 100644
--- /dev/null
+++ b/src/TensorSafe/Commands/Check.hs
@@ -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
diff --git a/src/TensorSafe/Commands/Compile.hs b/src/TensorSafe/Commands/Compile.hs
new file mode 100644
--- /dev/null
+++ b/src/TensorSafe/Commands/Compile.hs
@@ -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
diff --git a/src/TensorSafe/Commands/Examples.hs b/src/TensorSafe/Commands/Examples.hs
new file mode 100644
--- /dev/null
+++ b/src/TensorSafe/Commands/Examples.hs
@@ -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
+
diff --git a/src/TensorSafe/Commands/Utils.hs b/src/TensorSafe/Commands/Utils.hs
new file mode 100644
--- /dev/null
+++ b/src/TensorSafe/Commands/Utils.hs
@@ -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
diff --git a/src/TensorSafe/Compile/Expr.hs b/src/TensorSafe/Compile/Expr.hs
new file mode 100644
--- /dev/null
+++ b/src/TensorSafe/Compile/Expr.hs
@@ -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
diff --git a/src/TensorSafe/Core.hs b/src/TensorSafe/Core.hs
new file mode 100644
--- /dev/null
+++ b/src/TensorSafe/Core.hs
@@ -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)
+
+
diff --git a/src/TensorSafe/Examples/Examples.hs b/src/TensorSafe/Examples/Examples.hs
new file mode 100644
--- /dev/null
+++ b/src/TensorSafe/Examples/Examples.hs
@@ -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)
+
diff --git a/src/TensorSafe/Examples/MnistExample.hs b/src/TensorSafe/Examples/MnistExample.hs
new file mode 100644
--- /dev/null
+++ b/src/TensorSafe/Examples/MnistExample.hs
@@ -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
diff --git a/src/TensorSafe/Examples/SimpleExample.hs b/src/TensorSafe/Examples/SimpleExample.hs
new file mode 100644
--- /dev/null
+++ b/src/TensorSafe/Examples/SimpleExample.hs
@@ -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
diff --git a/src/TensorSafe/Layer.hs b/src/TensorSafe/Layer.hs
new file mode 100644
--- /dev/null
+++ b/src/TensorSafe/Layer.hs
@@ -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 #-}
diff --git a/src/TensorSafe/Layers.hs b/src/TensorSafe/Layers.hs
new file mode 100644
--- /dev/null
+++ b/src/TensorSafe/Layers.hs
@@ -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
diff --git a/src/TensorSafe/Layers/Conv2D.hs b/src/TensorSafe/Layers/Conv2D.hs
new file mode 100644
--- /dev/null
+++ b/src/TensorSafe/Layers/Conv2D.hs
@@ -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
diff --git a/src/TensorSafe/Layers/Dense.hs b/src/TensorSafe/Layers/Dense.hs
new file mode 100644
--- /dev/null
+++ b/src/TensorSafe/Layers/Dense.hs
@@ -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)
+            ])
diff --git a/src/TensorSafe/Layers/Dropout.hs b/src/TensorSafe/Layers/Dropout.hs
new file mode 100644
--- /dev/null
+++ b/src/TensorSafe/Layers/Dropout.hs
@@ -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)
+            ])
diff --git a/src/TensorSafe/Layers/Flatten.hs b/src/TensorSafe/Layers/Flatten.hs
new file mode 100644
--- /dev/null
+++ b/src/TensorSafe/Layers/Flatten.hs
@@ -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
diff --git a/src/TensorSafe/Layers/LSTM.hs b/src/TensorSafe/Layers/LSTM.hs
new file mode 100644
--- /dev/null
+++ b/src/TensorSafe/Layers/LSTM.hs
@@ -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)
+            ])
+
diff --git a/src/TensorSafe/Layers/MaxPooling.hs b/src/TensorSafe/Layers/MaxPooling.hs
new file mode 100644
--- /dev/null
+++ b/src/TensorSafe/Layers/MaxPooling.hs
@@ -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])
+                ])
diff --git a/src/TensorSafe/Layers/Relu.hs b/src/TensorSafe/Layers/Relu.hs
new file mode 100644
--- /dev/null
+++ b/src/TensorSafe/Layers/Relu.hs
@@ -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
diff --git a/src/TensorSafe/Layers/Sigmoid.hs b/src/TensorSafe/Layers/Sigmoid.hs
new file mode 100644
--- /dev/null
+++ b/src/TensorSafe/Layers/Sigmoid.hs
@@ -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\"")])
diff --git a/src/TensorSafe/Network.hs b/src/TensorSafe/Network.hs
new file mode 100644
--- /dev/null
+++ b/src/TensorSafe/Network.hs
@@ -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
diff --git a/src/TensorSafe/Shape.hs b/src/TensorSafe/Shape.hs
new file mode 100644
--- /dev/null
+++ b/src/TensorSafe/Shape.hs
@@ -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)
diff --git a/tensor-safe.cabal b/tensor-safe.cabal
new file mode 100644
--- /dev/null
+++ b/tensor-safe.cabal
@@ -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