Last active
June 2, 2020 02:17
-
-
Save rcythr/9cc4a275056cb92f8b9b4163bc98d83e to your computer and use it in GitHub Desktop.
A Lambda Calculus Interpreter implemented in Haskell. The only dependency is the readline library because without it, the REPL is pure pain and suffering.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| {- | |
| This program is free software: you can redistribute it and/or modify | |
| it under the terms of the GNU General Public License as published by | |
| the Free Software Foundation, either version 3 of the License, or | |
| (at your option) any later version. | |
| This program is distributed in the hope that it will be useful, | |
| but WITHOUT ANY WARRANTY; without even the implied warranty of | |
| MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the | |
| GNU General Public License for more details. | |
| You should have received a copy of the GNU General Public License | |
| along with this program. If not, see <https://www.gnu.org/licenses/>. | |
| -} | |
| module Main where | |
| import Prelude hiding (lex) | |
| import Control.Monad.State | |
| import Data.Char (isAlpha, isDigit, isSpace) | |
| import System.Environment | |
| import System.Exit | |
| import System.IO | |
| import System.Console.Readline | |
| import qualified Data.Map as Map | |
| import qualified Data.Set as Set | |
| import qualified Text.PrettyPrint as PP | |
| -------------------------------------------------------------------------------- | |
| -- Datatypes | |
| -------------------------------------------------------------------------------- | |
| data Token = | |
| TkLam | |
| | TkLParen | |
| | TkRParen | |
| | TkDot | |
| | TkId String | |
| deriving (Eq, Show) | |
| type Parser a = [Token] -> [(a, [Token])] | |
| data Expr = | |
| EId String | |
| | EApp Expr Expr | |
| | ELam String Expr | |
| type Eval a = State Int a | |
| type Env = Map.Map String Expr | |
| -------------------------------------------------------------------------------- | |
| -- Main & Helpers | |
| -------------------------------------------------------------------------------- | |
| unwrapEither :: Either a a -> a | |
| unwrapEither (Left x) = x | |
| unwrapEither (Right x) = x | |
| runPrompt :: (Expr -> Expr) -> IO () | |
| runPrompt f = do | |
| maybeLine <- readline "λ >> " | |
| case maybeLine of | |
| Nothing -> return () | |
| Just ":quit" -> return () | |
| Just line -> do | |
| addHistory line | |
| putStrLn . unwrapEither $ show . evaluate f <$> parse line | |
| runPrompt f | |
| main :: IO () | |
| main = do | |
| args <- getArgs | |
| case args of | |
| ["strict"] -> runPrompt strict | |
| ["naiveLazy"] -> runPrompt naiveLazy | |
| _ -> do | |
| putStrLn "Usage: EVALUATION_STRATEGY" | |
| putStrLn " EVALUATION_STRATEGY is one of {strict, naiveLazy}" | |
| exitFailure | |
| -------------------------------------------------------------------------------- | |
| -- Lexing | |
| -------------------------------------------------------------------------------- | |
| lex :: String -> [Token] | |
| lex [] = [] | |
| lex cs@(c:cs') | isSpace c = lex cs' | |
| | isAlpha c = let (xs, cs'') = span isAlpha cs in TkId xs : lex cs'' | |
| | c == '.' = TkDot : lex cs' | |
| | c == '(' = TkLParen : lex cs' | |
| | c == ')' = TkRParen : lex cs' | |
| | c == '\\' = TkLam : lex cs' | |
| | otherwise = TkId [c] : lex cs' | |
| -------------------------------------------------------------------------------- | |
| -- Parsing | |
| -------------------------------------------------------------------------------- | |
| pEmpty :: a -> Parser a | |
| pEmpty a toks = [(a, toks)] | |
| pAlt :: Parser a -> Parser a -> Parser a | |
| pAlt pA pB tokens = | |
| case pA tokens of | |
| [] -> pB tokens | |
| xs -> xs | |
| pZeroOrMore :: Parser a -> Parser [a] | |
| pZeroOrMore p = pOneOrMore p `pAlt` pEmpty [] | |
| pOneOrMore :: Parser a -> Parser [a] | |
| pOneOrMore p = pThen (:) p (pZeroOrMore p) | |
| pThen :: (a -> b -> c) -> Parser a -> Parser b -> Parser c | |
| pThen f pA pB toks = do | |
| (a, toksA) <- pA toks | |
| (b, toksB) <- pB toksA | |
| return (f a b, toksB) | |
| pThen3 :: (a -> b -> c -> d) -> Parser a -> Parser b -> Parser c -> Parser d | |
| pThen3 f pA pB pC toks = do | |
| (f', toksB) <- pThen f pA pB toks | |
| (c, toksC) <- pC toksB | |
| return (f' c, toksC) | |
| pThen4 :: (a -> b -> c -> d -> e) -> Parser a -> Parser b -> Parser c -> Parser d -> Parser e | |
| pThen4 f pA pB pC pD toks = do | |
| (f', toksC) <- pThen3 f pA pB pC toks | |
| (d, toksD) <- pD toksC | |
| return (f' d, toksD) | |
| pApply :: Parser a -> (a -> b) -> Parser b | |
| pApply pA f tokens = do | |
| (a, tokens') <- pA tokens | |
| return (f a, tokens') | |
| pTk :: Token -> Parser Token | |
| pTk tkn [] = [] | |
| pTk tkn (tok:toks) | tok == tkn = [(tkn, toks)] | |
| | otherwise = [] | |
| pId :: Parser String | |
| pId ((TkId s):toks) = [(s, toks)] | |
| pId _ = [] | |
| pExpr :: Parser Expr | |
| pExpr = pOneOrMore pExpr' `pApply` foldl1 EApp | |
| where | |
| pEId = pId `pApply` EId | |
| pELam = pThen4 (\_ y _ w -> ELam y w) (pTk TkLam) pId (pTk TkDot) pExpr | |
| pEParen = pThen3 (\_ y _ -> y) (pTk TkLParen) pExpr (pTk TkRParen) | |
| pExpr' = pEId `pAlt` pELam `pAlt` pEParen | |
| parse :: String -> Either String Expr | |
| parse input = | |
| case map fst . filter (null . snd) $ pExpr (lex input) of | |
| [] -> Left "No valid parse found." | |
| [e] -> Right e | |
| xs -> Left $ PP.render $ PP.text "Multiple parses found:\n" <> foldl1 (<>) (map (\x -> PP.text " " <> pprExpr x <> PP.text "\n") xs) | |
| -------------------------------------------------------------------------------- | |
| -- Pretty Printing Functions | |
| -------------------------------------------------------------------------------- | |
| instance Show Expr where | |
| show = PP.render . pprExpr | |
| -- | Pretty print an expression. Multi-item objects are not necessarily parenthesized. | |
| pprExpr :: Expr -> PP.Doc | |
| pprExpr (EId n) = PP.text n | |
| pprExpr (EApp f e) = pprExpr f PP.<+> pprExpr' e | |
| pprExpr e@(ELam _ _) = pprExpr' e | |
| -- | Pretty print an expression. Multi-item objects are parenthesized. | |
| pprExpr' :: Expr -> PP.Doc | |
| pprExpr' (ELam n e) = PP.text "(λ" <> PP.text n <> PP.text ". " <> pprExpr' e <> PP.text ")" | |
| pprExpr' e@(EApp _ _) = PP.text "(" <> pprExpr e <> PP.text ")" | |
| pprExpr' x = pprExpr x | |
| -------------------------------------------------------------------------------- | |
| -- Evaluation Functions | |
| -------------------------------------------------------------------------------- | |
| -- | Avoid unintentional lambda capture by renaming all lambda-bound variables | |
| -- to globally unused variables. Free variables are left untouched. | |
| alphaConvert :: Expr -> Eval Expr | |
| alphaConvert e = fst <$> alphaConvert' Map.empty e | |
| where | |
| avoidVars = varNames e | |
| freshVar :: Eval String | |
| freshVar = do | |
| s <- get | |
| put (s+1) | |
| let x = reverse (toVar s) | |
| if Set.member x avoidVars then | |
| freshVar | |
| else | |
| return x | |
| alphaConvert' :: Map.Map String String -> Expr -> Eval (Expr, Map.Map String String) | |
| alphaConvert' env (EApp f a) = do | |
| (f', env') <- alphaConvert' env f | |
| (a', env'') <- alphaConvert' env' a | |
| return (EApp f' a', env'') | |
| alphaConvert' env (ELam x b) = | |
| case Map.lookup x env of | |
| Nothing -> do | |
| v <- freshVar | |
| (b', env') <- alphaConvert' (Map.insert x v env) b | |
| return (ELam v b', Map.delete x env') | |
| Just v -> do | |
| v' <- freshVar | |
| (b', env') <- alphaConvert' (Map.insert x v' env) b | |
| return (ELam v' b', Map.insert x v env') | |
| alphaConvert' env (EId x) = | |
| case Map.lookup x env of | |
| Just v -> return (EId v, env) | |
| Nothing -> return (EId x, env) | |
| -- | Uses the given evaluation strategy and alphaConvert to compute the result | |
| -- of the given expression. | |
| evaluate :: (Expr -> Expr) -> Expr -> Expr | |
| evaluate f e = f (evalState (alphaConvert e) 0) | |
| -- | Evaluates the given expression using Call-By-Need, without sharing. | |
| naiveLazy :: Expr -> Expr | |
| naiveLazy (EApp f a) = | |
| case f' of | |
| (ELam x e) -> naiveLazy $ subst (x, a) e | |
| e -> EApp f' a | |
| where f' = naiveLazy f | |
| naiveLazy e = e | |
| -- | Evaluates the given expression using Call-By-Value. | |
| strict :: Expr -> Expr | |
| strict (EApp f a) = | |
| case f' of | |
| (ELam x e) -> strict $ subst (x, a') e | |
| e -> EApp f' a' | |
| where f' = strict f | |
| a' = strict a | |
| strict (ELam x b) = ELam x (strict b) | |
| strict e = e | |
| -- | Replace all variables, n, with the expression v in the given expression. | |
| subst :: (String, Expr) -> Expr -> Expr | |
| subst r@(n, v) e@(EId x) = if x == n then v else e | |
| subst r@(n, v) (EApp f a) = EApp (subst r f) (subst r a) | |
| subst r@(n, v) e@(ELam x b) = if x /= n then ELam x (subst r b) else e | |
| -- | Given an int, returns a unique string corresponding to that int. | |
| -- 0 is a, 1 is b, ... 27 is aa, etc. | |
| toVar :: Int -> String | |
| toVar c | c < 26 = [toEnum (97+c)] | |
| | otherwise = let (n, r) = c `divMod` 26 | |
| in toEnum (97+r) : toVar (n-1) | |
| -- | Returns the set of all used variable names in the given expression. | |
| -- this will be used during alpha conversion to avoid used variables. | |
| varNames :: Expr -> Set.Set String | |
| varNames (EId x) = Set.singleton x | |
| varNames (EApp f a) = varNames f `Set.union` varNames a | |
| varNames (ELam x b) = Set.insert x (varNames b) |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment