diff --git a/LambdaPrettyQuote.cabal b/LambdaPrettyQuote.cabal
--- a/LambdaPrettyQuote.cabal
+++ b/LambdaPrettyQuote.cabal
@@ -7,7 +7,7 @@
 -- The package version. See the Haskell package versioning policy
 -- (http://www.haskell.org/haskellwiki/Package_versioning_policy) for
 -- standards guiding when and how versions should be incremented.
-Version:             0.0.0.7
+Version:             0.0.0.8
 
 -- A short (one-line) description of the package.
 Synopsis:            Quasiquoter, and Arbitrary helpers for the lambda calculus.
@@ -51,7 +51,7 @@
 
 Library
   -- Modules exported by the library.
-  Exposed-modules: Language.Lambda.Untyped.Arbitrary, Language.Lambda.Untyped.Parser, Language.Lambda.Untyped.Pretty, Language.Lambda.Untyped.Quote, Language.Lambda.SimplyTyped.Arbitrary,  Language.Lambda.SimplyTyped.Pretty, Language.Lambda.SimplyTyped.TypeCheck 
+  Exposed-modules: Language.Lambda.Untyped.Arbitrary, Language.Lambda.Untyped.Parser, Language.Lambda.Untyped.Pretty, Language.Lambda.Untyped.Quote, Language.Lambda.SimplyTyped.Arbitrary,  Language.Lambda.SimplyTyped.Pretty, Language.Lambda.SimplyTyped.TypeCheck, Language.Lambda.SimplyTyped.Let.Arbitrary, Language.Lambda.SimplyTyped.Let.TypeCheck 
   Hs-Source-Dirs: src
   -- Packages needed in order to build this package.
   Build-depends: base >= 4.0 && <= 6.0,
diff --git a/src/Language/Lambda/SimplyTyped/Arbitrary.hs b/src/Language/Lambda/SimplyTyped/Arbitrary.hs
--- a/src/Language/Lambda/SimplyTyped/Arbitrary.hs
+++ b/src/Language/Lambda/SimplyTyped/Arbitrary.hs
@@ -3,7 +3,6 @@
     Env,
     gen_type,
     gen_expr,
-    --gen_env,
     gen_with_env,
     shrink_expr
 ) where
@@ -58,7 +57,7 @@
         1 -> Arrow <$> arb_type' (size - 1) <*> arb_type' (size - 1)
 
 arb_expr :: (Eq a, Eq s) => EnvGen a s c (Expr s a c)
-arb_expr = trace ("arb_expr") $ do
+arb_expr = do
     i <- get_size 
     input  <- arb_type
     output <- arb_type
@@ -89,7 +88,7 @@
      let f = Arrow output_type typ
      arb_app_typ i f output_type
 
-arb_app_typ i input_type output_type = trace ("arb_app_typ" ++ show i) $ do
+arb_app_typ i input_type output_type = do
     App <$> arb_expr' input_type (i - 1) <*> arb_expr' output_type (i - 1)
 
 
@@ -103,20 +102,19 @@
         Lam sym input <$> (arb_expr' output (i - 1))
 
 arb_expr' :: (Eq a, Eq s) => Type a -> Int -> EnvGen a s c (Expr s a c)
-arb_expr' typ i = trace ("arb_expr'" ++ show i) $ do
+arb_expr' typ i = do
     option <-lift $ choose (0, 10 :: Int)
     if option == 0
         then attemp_constant_expr typ i  
         else non_constant_expr typ i
         
 app_or_lam typ 0 = terminal_lambda typ 
-app_or_lam typ@(Arrow _ _) i = trace ("app_or_lam" ++ show i) $ do
+app_or_lam typ@(Arrow _ _) i = do
     option <- lift arbitrary
     if option
         then arb_app i typ
         else arb_lam i typ
-app_or_lam typ i = trace ("app_or_lam" ++ show i) $ do
-    arb_app i typ
+app_or_lam typ i = arb_app i typ
         
 terminal_lambda :: (Eq a, Eq s) => Type a -> EnvGen a s c (Expr s a c) 
 terminal_lambda typ@(Base _) = do 
@@ -129,7 +127,7 @@
      
 non_constant_expr :: (Eq a, Eq s) => Type a -> Int -> EnvGen a s c (Expr s a c)
 non_constant_expr typ@(Arrow _ _) 0 = arb_lam 0 typ
-non_constant_expr typ@(Arrow _ _) i = trace ("non_constant_expr" ++ show i) $ do
+non_constant_expr typ@(Arrow _ _) i = do
         option <- lift $ choose (0, 2 :: Int)
         case option of 
             0 -> do can_make_var <- var_type_exists typ
@@ -138,12 +136,12 @@
                         else app_or_lam typ i
             1 -> arb_app i typ
             2 -> arb_lam i typ
-non_constant_expr typ@(Base _) i = trace ("non_constant_expr" ++ show i) $ do
+non_constant_expr typ@(Base _) i = do
         c <- arb_constant typ
         return $ Constant $ fromJust c
 
 attemp_constant_expr :: (Eq a, Eq s) => Type a -> Int -> EnvGen a s c (Expr s a c)
-attemp_constant_expr typ i = trace ("attemp_constant_expr" ++ show i) $ do
+attemp_constant_expr typ i = do
     constant <- arb_constant typ
     case constant of
         Just x  -> return $ Constant x
@@ -165,7 +163,7 @@
 arb_base = lift =<< asks sel1
 
 get_size :: (Eq a, Eq s) => EnvGen a s c Int
-get_size = asks ((\x -> trace ("size " ++ show x) x) . sel3)
+get_size = asks sel3
 
 arb_constant :: (Eq a, Eq s) => (Type a) -> EnvGen a s c (Maybe c)
 arb_constant x = lift =<< asks (($ x) . sel4)
diff --git a/src/Language/Lambda/SimplyTyped/Let/Arbitrary.hs b/src/Language/Lambda/SimplyTyped/Let/Arbitrary.hs
new file mode 100644
--- /dev/null
+++ b/src/Language/Lambda/SimplyTyped/Let/Arbitrary.hs
@@ -0,0 +1,197 @@
+module Language.Lambda.SimplyTyped.Let.Arbitrary (
+    module Language.Lambda.Common.Arbitrary,
+    Env,
+    gen_type,
+    gen_expr,
+    gen_with_env,
+    shrink_expr
+) where
+import Test.QuickCheck
+import Control.Applicative ((<*>), (<$>))
+import Data.List
+import Language.Lambda.SimplyTyped.Let.Syntax
+import Control.Monad.RWS.Strict
+import Control.Applicative
+import Test.QuickCheck.Gen
+import Data.Tuple.Select
+import Language.Lambda.Common.Arbitrary
+import Data.Maybe
+import Debug.Trace.Helpers
+import Debug.Trace
+
+type Env a s = [(s, Type a)]
+
+null_const_gen = arbitrary :: Gen (Maybe ())
+
+gen_type :: (Eq a, Eq s) => Gen a -> Gen s -> Gen (Type a)
+gen_type x y = gen_with_env arb_type x y $ const null_const_gen
+
+gen_expr :: (Eq a, Eq s) => Gen a -> Gen s -> (Type a -> Gen (Maybe c)) -> Gen (Expr s a c)
+gen_expr = gen_with_env arb_expr
+
+shrink_expr :: Expr s a c -> [Expr s a c]
+shrink_expr x@(Constant _) = []
+shrink_expr x@(Var _)      = []
+shrink_expr (App x y)      = []
+shrink_expr (Lam s t e)    = []
+
+gen_with_env :: (Eq a, Eq s) => EnvGen a s c b -> Gen a -> Gen s -> (Type a -> Gen (Maybe c)) -> Gen b
+gen_with_env gen x y z = sized $ \i -> gen_with_env' gen (min i 5) x y z
+    
+gen_with_env' :: (Eq a, Eq s) => EnvGen a s c b -> Int -> Gen a -> Gen s -> (Type a -> Gen (Maybe c)) -> Gen b
+gen_with_env' gen size a_gen s_gen c_gen = do
+    (result, _) <- evalRWST gen (a_gen, s_gen, size, c_gen, []) ()
+    return result
+
+type EnvGen a s c = RWST (Gen a, Gen s, Int, Type a -> Gen (Maybe c), (Env a s)) () () Gen
+
+arb_type :: (Eq a, Eq s) => EnvGen a s c (Type a)
+arb_type = arb_type' =<< get_size 
+
+arb_type' :: (Eq a, Eq s) => Int -> EnvGen a s c (Type a)
+arb_type' 0    = Base <$> arb_base
+arb_type' size = do
+    option <- lift (choose (0, 1 :: Int))
+    case option of
+        0 -> Base  <$> arb_base
+        1 -> Arrow <$> arb_type' (size - 1) <*> arb_type' (size - 1)
+
+arb_expr :: (Eq a, Eq s) => EnvGen a s c (Expr s a c)
+arb_expr = do
+    i <- get_size 
+    input  <- arb_type
+    output <- arb_type
+    arb_lam i (Arrow input output)
+
+--This is good, but it is not useful for 
+arb_var typ = do
+    lookuped_value <- lookup_var_by_type typ
+    case lookuped_value of
+        (Just x) -> return $ Var $ fst x
+        _ -> error "bad symbol name"
+ 
+var_type_exists :: (Eq a, Eq s) => Type a -> EnvGen a s c (Bool)
+var_type_exists typ = isJust <$> lookup_var_by_type typ
+    
+lookup_var_by_type :: (Eq a, Eq s) => Type a -> EnvGen a s c (Maybe (s, Type a))
+lookup_var_by_type typ = do
+    vars <- gets_env (filter ((typ==) . snd))
+    if length vars > 0 
+        then do v <- lift $ elements vars
+                return $ Just v 
+        else return Nothing
+ 
+-- the right has to be it
+-- and the left has to be type -> whatever it was told to be  
+arb_app i typ = do
+     output_type <- arb_type
+     let f = Arrow output_type typ
+     arb_app_typ i f output_type
+
+arb_app_typ i input_type output_type = do
+    App <$> arb_expr' input_type (i - 1) <*> arb_expr' output_type (i - 1)
+
+
+fourth f (x, y, z, w, u) = (x, y, z, w, u)
+
+arb_lam :: (Eq a, Eq s) => Int -> Type a -> EnvGen a s c (Expr s a c) 
+arb_lam 0 x = terminal_lambda x
+arb_lam i (Arrow input output) = do
+    sym <- uniq_sym
+    local (fourth (extend sym input)) $ do 
+        Lam sym input <$> (arb_expr' output (i - 1))
+
+arb_expr' :: (Eq a, Eq s) => Type a -> Int -> EnvGen a s c (Expr s a c)
+arb_expr' typ i = do
+    option <-lift $ choose (0, 10 :: Int)
+    if option == 0
+        then attemp_constant_expr typ i  
+        else non_constant_expr typ i
+        
+app_or_lam typ 0 = terminal_lambda typ 
+app_or_lam typ@(Arrow _ _) i = do
+    option <- lift $ choose (0, 2 :: Int)
+    case option of
+        0 -> arb_app i typ
+        1 -> arb_lam i typ
+        2 -> arb_let i typ
+app_or_lam typ i = do
+    option <- lift arbitrary 
+    if option 
+        then arb_app i typ
+        else arb_let i typ
+        
+arb_let :: (Eq a, Eq s) => Int -> Type a -> EnvGen a s c (Expr s a c) 
+arb_let 0 typ =  error "let with depth zero"
+arb_let i typ = do
+    new_typ <- arb_type
+    sym <- uniq_sym
+    Let sym <$> arb_expr' new_typ (i - 1) <*> arb_expr' typ (i - 1)
+
+        
+terminal_lambda :: (Eq a, Eq s) => Type a -> EnvGen a s c (Expr s a c) 
+terminal_lambda typ@(Base _) = do 
+    c <- arb_constant typ
+    return $ Constant $ fromJust c
+terminal_lambda (Arrow input output) = do
+    sym <- uniq_sym
+    Lam sym input <$> terminal_lambda output
+
+     
+non_constant_expr :: (Eq a, Eq s) => Type a -> Int -> EnvGen a s c (Expr s a c)
+non_constant_expr typ@(Arrow _ _) 0 = arb_lam 0 typ
+non_constant_expr typ@(Arrow _ _) i = do
+        option <- lift $ choose (0, 3 :: Int)
+        case option of 
+            0 -> do can_make_var <- var_type_exists typ
+                    if can_make_var
+                        then arb_var typ
+                        else app_or_lam typ i
+            1 -> arb_app i typ
+            2 -> arb_lam i typ
+            3 -> arb_let i typ
+non_constant_expr typ@(Base _) 0 = do
+    c <- arb_constant typ
+    return $ Constant $ fromJust c
+non_constant_expr typ@(Base _) i = do
+        option <- lift $ arbitrary
+        if option
+            then do
+                    c <- arb_constant typ
+                    return $ Constant $ fromJust c
+            else do
+                    arb_let i typ
+
+attemp_constant_expr :: (Eq a, Eq s) => Type a -> Int -> EnvGen a s c (Expr s a c)
+attemp_constant_expr typ i = do
+    constant <- arb_constant typ
+    case constant of
+        Just x  -> return $ Constant x
+        Nothing -> non_constant_expr typ i
+            
+extend :: (Eq a, Eq s) => s -> Type a -> Env a s -> Env a s
+extend s t xs = (s, t):xs
+
+get_env :: (Eq a, Eq s) => EnvGen a s c (Env a s)
+get_env = asks sel5
+
+gets_env :: (Eq a, Eq s) => (Env a s -> d) ->  EnvGen a s c d
+gets_env f = asks (f . sel5)
+    
+arb_s :: (Eq a, Eq s) => EnvGen a s c s
+arb_s = lift =<< asks sel2
+    
+arb_base :: (Eq a, Eq s) => EnvGen a s c a
+arb_base = lift =<< asks sel1
+
+get_size :: (Eq a, Eq s) => EnvGen a s c Int
+get_size = asks sel3
+
+arb_constant :: (Eq a, Eq s) => (Type a) -> EnvGen a s c (Maybe c)
+arb_constant x = lift =<< asks (($ x) . sel4)
+
+uniq_sym :: (Eq a, Eq s) => EnvGen a s c s
+uniq_sym = do
+    s_gen <- asks sel2
+    env <- get_env
+    lift $ suchThat s_gen ( `notElem` (map fst env))
diff --git a/src/Language/Lambda/SimplyTyped/Let/TypeCheck.hs b/src/Language/Lambda/SimplyTyped/Let/TypeCheck.hs
new file mode 100644
--- /dev/null
+++ b/src/Language/Lambda/SimplyTyped/Let/TypeCheck.hs
@@ -0,0 +1,74 @@
+module Language.Lambda.SimplyTyped.Let.TypeCheck (type_check) where 
+import Language.Lambda.SimplyTyped.Let.Syntax
+import Control.Monad.Error
+import Control.Monad.Reader
+import Control.Monad.Identity
+import Data.Tuple.Select
+import Control.Arrow
+
+type M = Identity
+type TypeError = String
+
+type TypeCheckEnv a s c o = ErrorT TypeError (ReaderT ((c -> Type a), Env a s) M) o
+
+type_check :: (Show s, Eq s, Eq a, Show a) => (c -> Type a) -> Expr s a c -> Either TypeError (Type a)
+type_check const_to_type expr = runIdentity $ 
+    runReaderT (runErrorT (type_check' expr)) (const_to_type, [])
+
+------------------------------------------------------------------------------------------------------
+
+type Env a s = [(s, Type a)]
+
+extend :: s -> Type a -> Env a s -> Env a s
+extend sym typ xs = (sym, typ):xs
+
+find_var :: (Show s, Eq s) => s -> TypeCheckEnv a s c (Type a)
+find_var s = unmaybe ("could not find variable named " ++ show s) =<< (lift $ asks (lookup s . sel2))
+        
+type_check' :: (Show s, Eq s, Eq a, Show a) => Expr s a c -> TypeCheckEnv a s c (Type a)
+type_check' (Let sym expr in_expr) = do 
+    typ <- type_check' expr
+    local (second (extend sym typ)) $ type_check' in_expr
+type_check' (Var sym)      = find_var sym
+type_check' (App function argument) = do
+    function_type <- type_check'  function
+    --split the function type into its input and output
+    function_input_type  <- input_type  function_type 
+    function_output_type <- output_type function_type
+
+    --argument must match function input
+    argument_type <- type_check' argument
+    when (function_input_type /= argument_type) $ 
+        throwError $ ("Type Error: expected " ++ show function_input_type ++ " but got" 
+            ++ show argument_type)
+
+    return function_output_type
+type_check' (Lam sym input_typ expr) = do
+   local (second (extend sym input_typ)) $ do
+        output_typ <- type_check' expr
+        return $ Arrow input_typ output_typ
+type_check' (Constant c) = asks (($ c) . sel1)
+    
+    
+unmaybe :: String -> Maybe o -> TypeCheckEnv a s c o
+unmaybe error_string Nothing  = throwError error_string
+unmaybe error_string (Just x) = return x
+
+input_type (Arrow x _) = return x
+input_type _           = throwError "Not a function type"
+    
+output_type (Arrow _ y) = return y
+output_type _           = throwError "Not a function type"
+    
+    
+    
+    
+    
+    
+    
+    
+    
+    
+    
+    
+