Adding simply typed lambda calculus

4 files changed, 159 insertions, 2 deletions

diff --git a/package.yaml b/package.yaml
index 23a31a7..1c8e6b2 100644
--- a/package.yaml
+++ b/package.yaml
@@ -1,6 +1,7 @@
 name:                choc
 version:             0.1.0.0
-git:                 "https://sr.ht/~ymherklotz/choc"
+git:                 "https://git.sr.ht/~ymherklotz/choc"
+homepage:            "https://sr.ht/~ymherklotz/choc"
 license:             BSD3
 author:              "Yann Herklotz"
 maintainer:          "git@yannherklotz.com"
@@ -16,6 +17,7 @@ description:         Please see the README at <https://sr.ht/~ymherklotz/choc>
 
 dependencies:
 - base >= 4.7 && < 5
+- parsec >= 3 && < 4
 
 library:
   source-dirs: src
@@ -41,3 +43,4 @@ tests:
     - -with-rtsopts=-N
     dependencies:
     - choc
+    - hspec
diff --git a/src/Choc/Parser.hs b/src/Choc/Parser.hs
new file mode 100644
index 0000000..24e4004
--- /dev/null
+++ b/src/Choc/Parser.hs
@@ -0,0 +1,41 @@
+module Choc.Parser (
+  module Text.Parsec,
+  Parser,
+  lexeme,
+  reservedOp,
+  reserved,
+  symbol,
+  parens,
+  integer) where
+
+import Text.Parsec
+import qualified Text.Parsec.Token as T
+import Text.Parsec.Language (emptyDef)
+import Data.Functor.Identity (Identity)
+
+type Parser a = Parsec String () a
+
+lexer :: T.GenTokenParser String u Identity
+lexer = T.makeTokenParser (emptyDef {
+                              T.commentLine = ";",
+                              T.reservedNames = ["L", "B", "C"],
+                              T.reservedOpNames = ["->"]
+                           })
+
+lexeme :: Parser a -> Parser a
+lexeme = T.lexeme lexer
+
+reservedOp :: String -> Parser ()
+reservedOp = T.reservedOp lexer
+
+reserved :: String -> ParsecT String u Identity ()
+reserved = T.reserved lexer
+
+symbol :: String -> Parser String
+symbol = T.symbol lexer
+
+parens :: Parser a -> Parser a
+parens a = lexeme $ between (symbol "(") (symbol ")") a
+
+integer :: Parser Integer
+integer = T.integer lexer
diff --git a/src/Choc/SimplyTyped.hs b/src/Choc/SimplyTyped.hs
new file mode 100644
index 0000000..3481ec6
--- /dev/null
+++ b/src/Choc/SimplyTyped.hs
@@ -0,0 +1,108 @@
+module Choc.SimplyTyped where
+
+import Data.Functor (($>))
+import Control.Monad (guard)
+
+import Choc.Parser
+
+----------------------
+-- Type Definitions --
+----------------------
+
+data Type = Bass
+          | Arrow Type Type
+          deriving (Eq)
+
+data Term = Lambda Type Term
+          | App Term Term
+          | Var Integer
+          | Const
+          deriving (Eq)
+
+instance Show Type where
+  show Bass = "B"
+  show (Arrow b1 b2) = "(-> " <> show b1 <> " " <> show b2 <> ")"
+
+instance Show Term where
+  show Const = "C"
+  show (Var i) = show i
+  show (App t1 t2) = "(" <> show t1 <> " " <> show t2 <> ")"
+  show (Lambda ty te) = "(L " <> show ty <> " " <> show te <> ")"
+
+------------------
+-- Type Checker --
+------------------
+
+check :: [Type] -> Term -> Maybe Type
+check _ Const = return Bass
+check env (Var v)
+  | fromInteger v < length env = Just (env !! fromInteger v)
+  | otherwise = Nothing
+check env (Lambda tp te) = Arrow tp <$> check (tp : env) te
+check env (App tm tm') = do
+  Arrow i o <- check env tm
+  i' <- check env tm'
+  guard (i == i')
+  return o
+
+-------------------------------
+-- Evaluation of Expressions --
+-------------------------------
+
+eval :: Term -> Term
+eval (App t1 t2) =
+  case eval t1 of
+    Lambda _ body -> eval (subst 0 t2 body)
+    _ -> error "Cannot apply non function."
+eval v = v
+
+subst :: Integer -> Term -> Term -> Term
+subst _ _ Const = Const
+subst n tm (Var m) =
+  case compare m n of
+    LT -> Var m
+    EQ -> tm
+    GT -> Var (m - 1)
+subst n tm (Lambda t body) = Lambda t (subst (n + 1) tm body)
+subst n tm (App tm' tm'') = App (subst n tm tm') (subst n tm tm'')
+
+evalMay :: Term -> Maybe Term
+evalMay t = eval t <$ check [] t
+
+------------
+-- Parser --
+------------
+
+parseLambda :: Parser Term
+parseLambda = parens $ do
+  _ <- reserved "L"
+  t <- parseType
+  b <- parseTerm
+  return $ Lambda t b
+
+parseApp :: Parser Term
+parseApp = parens $ do
+  t1 <- parseTerm
+  t2 <- parseTerm
+  return $ App t1 t2
+
+parseVar :: Parser Term
+parseVar = Var <$> integer
+
+parseType :: Parser Type
+parseType =
+  (reserved "B" $> Bass) <|>
+  (parens $ do
+      _ <- reservedOp "->"
+      t1 <- parseType
+      t2 <- parseType
+      return (Arrow t1 t2))
+
+parseTerm :: Parser Term
+parseTerm = try parseLambda <|> parseApp <|> parseVar <|> (reserved "C" $> Const)
+
+parseL :: String -> Term
+parseL a =
+  case runParser parseTerm () "" a of
+    Right b -> b
+    Left _ -> error "Could not parse expression."
diff --git a/test/Spec.hs b/test/Spec.hs
index cd4753f..12eed81 100644
--- a/test/Spec.hs
+++ b/test/Spec.hs
@@ -1,2 +1,7 @@
+import Test.Hspec
+
 main :: IO ()
-main = putStrLn "Test suite not yet implemented"
+main = hspec $ do
+  describe "Prelude.head" $ do
+    it "returns the first element of a list" $ do
+      head [23 ..] `shouldBe` (23 :: Int)