Add a small typechecker

lambda-calculator.cabal

@@ -24,8 +24,10 @@ library
 
                        Language.SystemF,
                        Language.SystemF.Expression,
-                       Language.SystemF.Parser
+                       Language.SystemF.Parser,
+                       Language.SystemF.TypeCheck
   build-depends:       base <= 5,
+                       containers,
                        parsec
   default-language:    Haskell2010
 
@@ -58,9 +60,11 @@ test-suite lambda-calculus-test
 
                        Language.SystemFSpec,
                        Language.SystemF.ExpressionSpec,
-                       Language.SystemF.ParserSpec
+                       Language.SystemF.ParserSpec,
+                       Language.SystemF.TypeCheckSpec
   build-depends:       base <= 5,
                        lambda-calculator,
+                       containers,
                        hspec,
                        HUnit
   ghc-options:         -threaded -rtsopts -with-rtsopts=-N

src/Language/SystemF/Expression.hs

-{-# LANGUAGE FlexibleInstances #-}
 module Language.SystemF.Expression where
 
 import Data.Monoid

src/Language/SystemF/TypeCheck.hs

+module Language.SystemF.TypeCheck where
+
+import Data.Map
+import Prelude hiding (lookup)
+
+import Language.SystemF.Expression
+
+type UniqueSupply n = [n]
+type Context n t = Map n t
+
+typecheck :: (Ord n, Eq t)
+          => UniqueSupply t 
+          -> Context n (Ty t)
+          -> SystemFExpr n t 
+          -> Either String (Ty t)
+typecheck uniqs ctx (Var v)        = tcVar uniqs ctx v
+typecheck uniqs ctx (Abs n t body) = tcAbs uniqs ctx n t body
+typecheck _     _   _       = undefined
+
+tcVar :: (Ord n, Eq t)
+      => UniqueSupply t
+      -> Context n (Ty t)
+      -> n
+      -> Either String (Ty t)
+tcVar uniqs ctx var = maybe (TyVar <$> unique uniqs) return (lookup var ctx)
+
+tcAbs :: (Ord n, Eq t)
+      => UniqueSupply t
+      -> Context n (Ty t)
+      -> n
+      -> Ty t
+      -> SystemFExpr n t
+      -> Either String (Ty t)
+tcAbs uniqs ctx name ty body = TyArrow ty <$> typecheck uniqs ctx' body
+  where ctx' = insert name ty ctx
+
+-- Utilities
+unique :: UniqueSupply t
+       -> Either String t
+unique (u:_) = return u
+unique _     = fail "Unique supply ran out"

test/Language/SystemF/TypeCheckSpec.hs

+module Language.SystemF.TypeCheckSpec (spec) where
+
+import Data.Map
+
+import Test.Hspec
+
+import Language.SystemF.Expression
+import Language.SystemF.TypeCheck
+
+tc uniqs ctx = typecheck uniqs (fromList ctx)
+
+spec :: Spec
+spec = describe "typecheck" $ do
+  it "typechecks simple variables in context" $
+    tc [] [("x", TyVar "X")] (Var "x") `shouldBe` Right (TyVar "X")
+
+  it "typechecks simple variables not in context" $ 
+    tc ["A"] [] (Var "x") `shouldBe` Right (TyVar "A")
+
+  it "typechecks simple abstractions" $
+    tc [] [] (Abs "x" (TyVar "A") (Var "x")) 
+      `shouldBe` Right (TyArrow (TyVar "A") (TyVar "A"))