From 8c8539415b1a31f7bba6da4f0795a1fe4e92360f Mon Sep 17 00:00:00 2001
From: Sean Gillespie <sean@mistersg.net>
Date: Fri, 6 Jan 2017 21:44:08 -0500
Subject: [PATCH] Add a small typechecker
---
lambda-calculator.cabal | 8 +++--
src/Language/SystemF/Expression.hs | 1 -
src/Language/SystemF/TypeCheck.hs | 41 ++++++++++++++++++++++++++
test/Language/SystemF/TypeCheckSpec.hs | 22 ++++++++++++++
4 files changed, 69 insertions(+), 3 deletions(-)
create mode 100644 src/Language/SystemF/TypeCheck.hs
create mode 100644 test/Language/SystemF/TypeCheckSpec.hs
diff --git a/lambda-calculator.cabal b/lambda-calculator.cabal
index d0071b0..9fd17c5 100644
--- a/lambda-calculator.cabal
+++ b/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
diff --git a/src/Language/SystemF/Expression.hs b/src/Language/SystemF/Expression.hs
index ece7e15..0bfa167 100644
--- a/src/Language/SystemF/Expression.hs
+++ b/src/Language/SystemF/Expression.hs
@@ -1,4 +1,3 @@
-{-# LANGUAGE FlexibleInstances #-}
module Language.SystemF.Expression where
import Data.Monoid
diff --git a/src/Language/SystemF/TypeCheck.hs b/src/Language/SystemF/TypeCheck.hs
new file mode 100644
index 0000000..76616f9
--- /dev/null
+++ b/src/Language/SystemF/TypeCheck.hs
@@ -0,0 +1,41 @@
+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"
diff --git a/test/Language/SystemF/TypeCheckSpec.hs b/test/Language/SystemF/TypeCheckSpec.hs
new file mode 100644
index 0000000..2776892
--- /dev/null
+++ b/test/Language/SystemF/TypeCheckSpec.hs
@@ -0,0 +1,22 @@
+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"))
--
GitLab