diff options
author | Yann Herklotz <git@yannherklotz.com> | 2022-03-13 11:07:40 +0000 |
---|---|---|
committer | Yann Herklotz <git@yannherklotz.com> | 2022-03-13 11:07:40 +0000 |
commit | cf44e166a956bb7a00f9185291f02c54d213be0f (patch) | |
tree | 87617eab467af8d5a27145f75c9e1145f2423be6 /src | |
parent | 425e96636c1311b52a9e72c004cd1e74deb37bf0 (diff) | |
download | choc-cf44e166a956bb7a00f9185291f02c54d213be0f.tar.gz choc-cf44e166a956bb7a00f9185291f02c54d213be0f.zip |
Adding simply typed lambda calculus
Diffstat (limited to 'src')
-rw-r--r-- | src/Choc/Parser.hs | 41 | ||||
-rw-r--r-- | src/Choc/SimplyTyped.hs | 108 |
2 files changed, 149 insertions, 0 deletions
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." |