slight edits

haskell/TypeCheckerAtkey.hs

@@ -11,12 +11,19 @@ data Typ
 data Term
   = Var Int
   | App Term Term
-  | Abs Typ Term
+  | Lam Typ Term
 
 -- Context here keeps track of the type of variables.
 -- Not their values.
 type Ctxt = [Typ] 
 
+-- λ> [] !! 0
+-- *** Exception: Prelude.!!: index too large
+-- CallStack (from HasCallStack):
+--   error, called at libraries/base/GHC/List.hs:1368:14 in base:GHC.List
+--   tooLarge, called at libraries/base/GHC/List.hs:1378:50 in base:GHC.List
+--   !!, called at <interactive>:140:4 in interactive:Ghci1
+
 typecheck :: Term -> Ctxt -> Maybe Typ  
 typecheck tm ctxt = case tm of
   Var i -> Just $ ctxt !! i
@@ -29,18 +36,18 @@ typecheck tm ctxt = case tm of
             if typ1 == typ1' then Just typ2
             else Nothing
       _ -> Nothing
-  Abs ty1 tm ->
+  Lam ty1 tm ->
     case typecheck tm (ty1:ctxt) of
       Just ty2 -> Just $ Arrow ty1 ty2
       _ -> Nothing
 
 
-eg1 = Abs Boolean (Var 0)  
+eg1 = Lam Boolean (Var 0)  
 
 -- Open terms possible too
-eg2 = Abs Boolean (Var 2)  
+eg2 = Lam Boolean (Var 2)  
 
-eg3 = App (Abs Boolean (Var 2)) (Var 0)
+eg3 = App (Lam Boolean (Var 2)) (Var 0)
 
 -- λ> typecheck eg1 [Boolean, Nat, Arrow Nat Boolean]
 -- Just (Arrow Boolean Boolean)
@@ -51,3 +58,49 @@ eg3 = App (Abs Boolean (Var 2)) (Var 0)
 
 
 type TypeChecker = Ctxt -> Maybe Typ
+
+typecheck2 :: Term -> TypeChecker
+typecheck2 tm ctxt = case tm of
+  Var i -> var i ctxt
+  App tm1 tm2 -> app tm1 tm2 ctxt
+  Lam t tm -> lam t tm ctxt
+
+var :: Int -> TypeChecker
+var i ctxt = Just $ ctxt !! i
+
+app :: Term -> Term -> TypeChecker
+app tm1 tm2 ctxt = case typecheck2 tm1 ctxt of
+    Just (Arrow ty1 ty2) ->
+        (case typecheck2 tm2 ctxt of
+        Just ty' -> if ty2 == ty' then Just ty2 else Nothing
+        _ -> Nothing)
+    Nothing -> Nothing                 
+
+lam :: Typ -> Term -> TypeChecker
+lam t tm ctxt = case typecheck2 tm (t:ctxt) of  -- TODO: Attention. Probably wrong
+    Just ty -> Just $ Arrow t ty
+    _ -> Nothing
+                             
+-- Typechecker whose i-th element in context has type ty
+have :: Int -> Typ -> TypeChecker -> TypeChecker
+have i ty tc = \ctxt ->
+  if ctxt!!i == ty then tc ctxt
+  else Nothing
+
+-- Typechecker that always fail
+failure :: TypeChecker
+failure = \ctxt -> Nothing
+
+-- Typecheck that evaluates to a particular type
+hasType :: Typ -> TypeChecker -> TypeChecker
+hasType ty tc = \ctxt -> case tc ctxt of
+  Just ty' -> if ty == ty' then Just ty else Nothing
+  _ -> Nothing
+
+
+-- λf:B -> N. λa:B. f a
+eg4 :: Term
+eg4 = Lam (Arrow Boolean Nat) $ Lam Boolean $ App (Var 1) (Var 0)
+
+tc1 = lam (Arrow Boolean Nat)
+-- $ lam Boolean $ app (var 1) (var 0)