From 036c48a90216ff92549f56fc87f017c81798982f Mon Sep 17 00:00:00 2001 From: James Martin Date: Thu, 18 Mar 2021 14:40:04 -0700 Subject: [PATCH] Make the REPL awesome with readline, declarations, commands, file loading, etc. * Added line and block comments to the syntax * Added `:trace`, `:clear`, `:load`, and `:check` commands to the REPL * Added persistent declarations and a syntax for multi-expression programs Future ideas: * `:type` (print the type of an expression) * `:dump` (dump all definitions to a file) * auto-complete for commands and variable-names * list files to load as arguments * initial `:trace` and `:check` config as arguments --- README.md | 94 +++-------- app/Main.hs | 246 ++++++++++++++++++++++++++-- examples.lc | 31 ++++ package.yaml | 3 + src/LambdaCalculus/Evaluator.hs | 20 ++- src/LambdaCalculus/Expression.hs | 1 + src/LambdaCalculus/Syntax/Parser.hs | 63 ++++++- 7 files changed, 357 insertions(+), 101 deletions(-) create mode 100644 examples.lc diff --git a/README.md b/README.md index c9dec64..6c36dcb 100644 --- a/README.md +++ b/README.md @@ -5,11 +5,27 @@ using the Hindley-Milner type system, plus some builtin types, `fix`, and `callc ## Usage Run the program using `stack run` (or run the tests with `stack test`). -Type in your expression at the prompt: `>> `. This will happen: -* the type for the expression will be inferred and then printed, -* then, regardless of whether typechecking succeeded, expression will be evaluated to normal form using the call-by-value evaluation strategy and then printed. +Type in your expression at the prompt: `>> `. +Yourexpression will be evaluated to normal form using the call-by-value evaluation strategy and then printed. -Exit the prompt with `Ctrl-c` (or equivalent). +Exit the prompt with `Ctrl-d` (or equivalent). + +## Commands +Instead of entering an expression in the REPL, you may enter a command. +These commands are available: + +* `:load `: Execute a program in the interpreter, importing all definitions. +* `:clear`: Clear all of your variable definitions. +* `:check `: + * If the first argument is `off`, then expressions will be evaluated even if they do not typecheck. + * If the second argument is `always`, inferred types will always be printed. + If it is `decls`, then only declarations will have their inferred types printed. + Otherwise, the type of expressions is never printed. + * The default values are `on` `decls`. +* `:trace `: + * If the argument is `local`, intermediate expressions will be printed as the evaluator evaluates them. + * If the argument is `global`, the *entire* expression will be printed each evaluator step. + * The default value is `off`. ## Syntax The parser's error messages currently are virtually useless, so be very careful with your syntax. @@ -30,6 +46,12 @@ The parser's error messages currently are virtually useless, so be very careful * Literals: `1234`, `[e, f, g, h]`, `'a`, `"abc"` * Strings are represented as lists of characters. * Type annotations: there are no type annotations; types are inferred only. +* Comments: `// line comment`, `/* block comment */` + +Top-level contexts (e.g. the REPL or a source code file) +allow declarations (`let` expressions without `in ...`), +which make your definitions available for the rest of the program's execution. +You may separate multiple declarations and expressions with `;`. ## Types Types are checked/inferred using the Hindley-Milner type inference algorithm. @@ -59,66 +81,4 @@ because they perform the side effect of modifying the current continuation, and this is *not* valid syntax you can input into the REPL. ## Example code -Create a list by iterating `f` `n` times: -``` -fix \iterate f x. { Z -> [] ; S n -> (x :: iterate f (f x) n) } -: ∀e. ((e -> e) -> (e -> (Nat -> [e]))) -``` - -Use the iterate function to count to 10: -``` ->> let iterate = fix \iterate f x. { Z -> [] ; S n -> (x :: iterate f (f x) n) }; countTo = iterate S 1 in countTo 10 -: [Nat] -[1, 2, 3, 4, 5, 6, 7, 8, 9, 10] -``` - -Append two lists together: -``` -fix \append xs ys. { [] -> ys ; (x :: xs) -> (x :: append xs ys) } xs -: ∀j. ([j] -> ([j] -> [j])) -``` - -Reverse a list: -``` -fix \reverse. { [] -> [] ; (x :: xs) -> append (reverse xs) [x] } -: ∀c1. ([c1] -> [c1]) -``` - -Putting them together so we can reverse `"reverse"`: -``` ->> let append = fix \append xs ys. { [] -> ys ; (x :: xs) -> (x :: append xs ys) } xs; reverse = fix \reverse. { [] -> [] ; (x :: xs) -> append (reverse xs) [x] } in reverse "reverse" -: [Char] -"esrever" -``` - -Calculating `3 + 2` with the help of Church-encoded numerals: -``` ->> let Sf = \n f x. f (n f x); plus = \x. x Sf in plus (\f x. f (f (f x))) (\f x. f (f x)) S Z -: Nat -5 -``` - -This expression would loop forever, but `callcc` saves the day! -``` ->> S (callcc \k. (fix \x. x) (k Z)) -: Nat -1 -``` - -And if it wasn't clear, this is what the `Char` constructor does: - -``` ->> { Char c -> Char (S c) } 'a -: Char -'b -``` - -Here are a few expressions which don't typecheck but are handy for debugging the evaluator: -``` ->> let D = \x. x x; F = \f. f (f y) in D (F \x. x) -y y ->> let T = \f x. f (f x) in (\f x. T (T (T (T T))) f x) (\x. x) y -y ->> (\x y z. x y) y -λy' z. y y' -``` +You can see some example code in `examples.lc`. diff --git a/app/Main.hs b/app/Main.hs index 358c5a1..e310b69 100644 --- a/app/Main.hs +++ b/app/Main.hs @@ -1,24 +1,236 @@ +{-# OPTIONS_GHC -Wno-unused-do-bind -Wno-monomorphism-restriction #-} module Main (main) where import LambdaCalculus -import Control.Monad (forever) -import Data.Text (pack) -import Data.Text.IO -import Prelude hiding (putStr, putStrLn, getLine) -import System.IO (hFlush, stdout) +import Control.Exception (IOException, catch) +import Data.Maybe (isJust) +import Control.Monad (when) +import Control.Monad.Catch (MonadMask) +import Control.Monad.Except (MonadError, ExceptT, runExceptT, throwError, liftEither) +import Control.Monad.IO.Class (MonadIO, liftIO) +import Control.Monad.Loops (whileJust_) +import Control.Monad.State (MonadState, StateT, evalStateT, gets, modify) +import Control.Monad.Trans (lift) +import Data.HashMap.Strict (HashMap) +import Data.HashMap.Strict qualified as HM +import Data.Text qualified as T +import System.Console.Haskeline + ( InputT, runInputT, defaultSettings + , outputStrLn, getInputLine, handleInterrupt, withInterrupt + ) +import Text.Parsec +import Text.Parsec.Text (Parser) -prompt :: Text -> IO Text -prompt text = do - putStr text - hFlush stdout - getLine +outputTextLn :: MonadIO m => Text -> InputT m () +outputTextLn = outputStrLn . T.unpack + +-- | Immediately quit the program when interrupted +-- without performing any additional actions. +-- (Without this, it will print an extra newline for some reason.) +justDie :: (MonadIO m, MonadMask m) => InputT m () -> InputT m () +justDie = handleInterrupt (pure ()) . withInterrupt + +data AppState = AppState + { traceOptions :: TraceOptions + , checkOptions :: CheckOptions + , definitions :: HashMap Text CheckExpr + } + +data TraceOptions + -- | Print the entire expression in traces. + = TraceGlobal + -- | Print only the modified part of the expression in traces. + | TraceLocal + -- | Do not trace evaluation. + | TraceOff + +data CheckOptions = CheckOptions + -- | Require that an expression typechecks to run it. + { shouldTypecheck :: Bool + -- | Print the inferred type of an expressions. + , shouldPrintType :: CheckPrintOptions + } + +data CheckPrintOptions = PrintAlways | PrintDecls | PrintOff + deriving Eq + +shouldPrintTypeErrorsQ :: Bool -> CheckOptions -> Bool +shouldPrintTypeErrorsQ isDecl opts + = shouldTypecheck opts + || shouldPrintTypeQ isDecl opts + +shouldPrintTypeQ :: Bool -> CheckOptions -> Bool +shouldPrintTypeQ isDecl opts + = shouldPrintType opts == PrintAlways + || shouldPrintType opts == PrintDecls && isDecl + +defaultAppState :: AppState +defaultAppState = AppState + { traceOptions = TraceOff + , checkOptions = CheckOptions + { shouldTypecheck = True + , shouldPrintType = PrintDecls + } + , definitions = HM.empty + } + +data Command + = Trace TraceOptions + | Check CheckOptions + | Load FilePath + | Clear + +commandParser :: Parser Command +commandParser = do + char ':' + trace <|> check <|> load <|> clear + where + trace = Trace <$> do + try $ string "trace " + try traceOff <|> try traceLocal <|> try traceGlobal + traceOff = TraceOff <$ string "off" + traceLocal = TraceLocal <$ string "local" + traceGlobal = TraceGlobal <$ string "global" + + check = Check <$> do + try $ string "check " + spaces + tc <- (True <$ try (string "on ")) <|> (False <$ try (string "off ")) + spaces + pr <- try printAlways <|> try printDecls <|> try printOff + pure $ CheckOptions tc pr + printAlways = PrintAlways <$ string "always" + printDecls = PrintDecls <$ string "decls" + printOff = PrintOff <$ string "off" + + load = Load <$> do + try $ string "load " + spaces + many1 anyChar + + clear = Clear <$ try (string "clear") + +class MonadState AppState m => MonadApp m where + parsed :: Either ParseError a -> m a + typecheckDecl :: Text -> CheckExpr -> m (Maybe Scheme) + typecheckExpr :: CheckExpr -> m (Maybe Scheme) + execute :: CheckExpr -> m EvalExpr + +type AppM = ExceptT Text (StateT AppState (InputT IO)) + +liftInput :: InputT IO a -> AppM a +liftInput = lift . lift + +instance MonadApp AppM where + parsed (Left err) = throwError $ T.pack $ show err + parsed (Right ok) = pure ok + + typecheckDecl = typecheck . Just + typecheckExpr = typecheck Nothing + + execute checkExpr = do + defs <- gets definitions + let expr = check2eval $ substitute defs checkExpr + traceOpts <- gets traceOptions + case traceOpts of + TraceOff -> do + let value = eval expr + liftInput $ outputTextLn $ unparseEval value + pure value + TraceLocal -> do + let (value, trace) = evalTrace expr + liftInput $ mapM_ (outputTextLn . unparseEval) trace + pure value + TraceGlobal -> do + let (value, trace) = evalTraceGlobal expr + liftInput $ mapM_ (outputTextLn . unparseEval) trace + pure value + +typecheck :: Maybe Text -> CheckExpr -> AppM (Maybe Scheme) +typecheck decl expr = do + defs <- gets definitions + let type_ = infer $ substitute defs expr + checkOpts <- gets checkOptions + if shouldTypecheck checkOpts + then case type_ of + Left err -> throwError $ "Typecheck error: " <> err + Right t -> do + printType checkOpts t + pure $ Just t + else do + case type_ of + Left err -> + when (shouldPrintTypeErrorsQ isDecl checkOpts) $ + liftInput $ outputStrLn $ "Typecheck error: " <> T.unpack err + Right t -> printType checkOpts t + + pure Nothing + where + isDecl = isJust decl + + printType opts t = + when (shouldPrintTypeQ isDecl opts) $ + liftInput $ outputTextLn $ prefix <> unparseScheme t + + prefix = case decl of + Just name -> name <> " : " + Nothing -> ": " + +define :: MonadApp m => Text -> CheckExpr -> m () +define name expr = modify \appState -> + let expr' = substitute (definitions appState) expr + in appState { definitions = HM.insert name expr' $ definitions appState } + +runDeclOrExpr :: MonadApp m => DeclOrExprAST -> m () +runDeclOrExpr (Left (name, exprAST)) = do + defs <- gets definitions + let expr = substitute defs $ ast2check exprAST + _ <- typecheckDecl name expr + define name expr +runDeclOrExpr (Right exprAST) = do + defs <- gets definitions + let expr = substitute defs $ ast2check exprAST + _ <- typecheckExpr expr + _ <- execute expr + pure () + +runProgram :: MonadApp m => ProgramAST -> m () +runProgram = mapM_ runDeclOrExpr + +runCommand :: forall m. (MonadApp m, MonadIO m, MonadError Text m) => Command -> m () +runCommand (Trace traceOpts) = modify \app -> app { traceOptions = traceOpts } +runCommand (Check checkOpts) = modify \app -> app { checkOptions = checkOpts } +runCommand Clear = modify \app -> app { definitions = HM.empty } +runCommand (Load filePath) = do + input <- safeReadFile + program <- parsed $ parse programParser filePath input + runProgram program + where + safeReadFile :: m Text + safeReadFile = liftEither =<< liftIO ( + (Right . T.pack <$> readFile filePath) + `catch` handleException) + + handleException :: IOException -> IO (Either Text Text) + handleException = pure . Left . T.pack . show + +parseCommandOrDeclOrExpr :: MonadApp m => Text -> m (Either Command DeclOrExprAST) +parseCommandOrDeclOrExpr input = parsed $ parse commandOrDeclOrExprParser "input" input + where + commandOrDeclOrExprParser = + (Left <$> try commandParser) <|> (Right <$> declOrExprParser) <* spaces <* eof main :: IO () -main = forever $ parseCheck <$> prompt ">> " >>= \case - Left parseError -> putStrLn $ "Parse error: " <> pack (show parseError) - -- TODO: Support choosing which version to use at runtime. - Right expr -> do - either putStrLn (putStrLn . (": " <>) . unparseScheme) $ infer expr - putStrLn $ unparseEval $ eval $ check2eval expr - --mapM_ (putStrLn . unparseEval) $ snd $ traceEval $ check2eval expr +main = runInputT defaultSettings $ justDie $ flip evalStateT defaultAppState $ + whileJust_ (fmap T.pack <$> lift (getInputLine ">> ")) \inputText -> + handleErrors do + input <- parseCommandOrDeclOrExpr inputText + either runCommand runDeclOrExpr input + where + handleErrors :: ExceptT Text (StateT AppState (InputT IO)) () -> StateT AppState (InputT IO) () + handleErrors m = do + result <- runExceptT m + case result of + Left err -> lift $ outputTextLn err + Right _ -> pure () diff --git a/examples.lc b/examples.lc new file mode 100644 index 0000000..3850d52 --- /dev/null +++ b/examples.lc @@ -0,0 +1,31 @@ +// Create a list by iterating `f` `n` times: +let iterate = fix \iterate f x. { Z -> [] ; S n -> (x :: iterate f (f x) n) }; +// Use the iterate function to count to 10: +let countTo = iterate S 1 in countTo 10; + +// Append two lists together: +let append = fix \append xs ys. { [] -> ys ; (x :: xs) -> (x :: append xs ys) } xs; +// Reverse a list: +let reverse = fix \reverse. { [] -> [] ; (x :: xs) -> append (reverse xs) [x] }; +// Now we can reverse `"reverse"`: +reverse "reverse"; + +// Calculating `3 + 2` with the help of Church-encoded numerals: +let Sf = \n f x. f (n f x); plus = \x. x Sf in plus (\f x. f (f (f x))) (\f x. f (f x)) S Z; + +// This expression would loop forever, but `callcc` saves the day! +S (callcc \k. (fix \x. x) (k Z)); + +// And if it wasn't clear, this is what the `Char` constructor does: +{ Char c -> Char (S c) } 'a; +// (it outputs `'b`) + +// Here are a few expressions which don't typecheck but are handy for debugging the evaluator: +/* +let D = \x. x x; F = \f. f (f y) in D (F \x. x); +// y y +let T = \f x. f (f x) in (\f x. T (T (T (T T))) f x) (\x. x) y; +// y +(\x y z. x y) y; +// λy' z. y y' +*/ diff --git a/package.yaml b/package.yaml index 823c836..81a3489 100644 --- a/package.yaml +++ b/package.yaml @@ -37,6 +37,7 @@ default-extensions: dependencies: - base >= 4.14 && < 5 +- monad-loops >= 0.4.3 && < 0.5 - mtl >= 2.2 && < 3 - parsec >= 3.1 && < 4 - recursion-schemes >= 5.2 && < 6 @@ -72,6 +73,8 @@ executables: - -with-rtsopts=-N dependencies: - jtm-lambda-calculus + - exceptions >= 0.10.4 && < 0.11 + - haskeline >= 0.8 && < 1 tests: jtm-lambda-calculus-test: diff --git a/src/LambdaCalculus/Evaluator.hs b/src/LambdaCalculus/Evaluator.hs index 82624c0..9b4ef2c 100644 --- a/src/LambdaCalculus/Evaluator.hs +++ b/src/LambdaCalculus/Evaluator.hs @@ -3,13 +3,14 @@ module LambdaCalculus.Evaluator , Eval, EvalExpr, EvalX, EvalXF (..) , pattern AppFE, pattern CtrE, pattern CtrFE , pattern ContE, pattern ContFE, pattern CallCCE, pattern CallCCFE - , eval, traceEval + , eval, evalTrace, evalTraceGlobal ) where import LambdaCalculus.Evaluator.Base import LambdaCalculus.Evaluator.Continuation import Control.Monad.Except (MonadError, ExceptT, throwError, runExceptT) +import Control.Monad.Loops (iterateM_) import Control.Monad.State (MonadState, evalState, modify', state, put, gets) import Control.Monad.Writer (runWriterT, tell) import Data.HashMap.Strict qualified as HM @@ -54,10 +55,6 @@ pop = state \case ret :: (MonadError EvalExpr m, MonadState Continuation m) => EvalExpr -> m EvalExpr ret e = pop >>= maybe (throwError e) (pure . continue1 e) --- | Iteratively perform an action forever (or at least until it performs a control flow effect). -iterateM_ :: Monad m => (a -> m a) -> a -> m b -iterateM_ m = m' where m' x = m x >>= m' - fromLeft :: Either a Void -> a fromLeft (Left x) = x fromLeft (Right x) = absurd x @@ -105,10 +102,15 @@ evaluatorStep = \case eval :: EvalExpr -> EvalExpr eval = flip evalState [] . loop evaluatorStep -traceEval :: EvalExpr -> (EvalExpr, [EvalExpr]) -traceEval = flip evalState [] . runWriterT . loop \e -> do - -- You can also use `gets (continue e)` to print the *entire* expression each step. - -- This is a trade-off because it becomes much harder to pick out what changed from the rest of the expression. +-- | Trace each evaluation step. +evalTrace :: EvalExpr -> (EvalExpr, [EvalExpr]) +evalTrace = flip evalState [] . runWriterT . loop \e -> do + tell [e] + evaluatorStep e + +-- | Trace each evaluation step, including the *entire* continuation of each step. +evalTraceGlobal :: EvalExpr -> (EvalExpr, [EvalExpr]) +evalTraceGlobal = flip evalState [] . runWriterT . loop \e -> do e' <- gets (continue e) tell [e'] evaluatorStep e diff --git a/src/LambdaCalculus/Expression.hs b/src/LambdaCalculus/Expression.hs index 3f6ff5e..749f881 100644 --- a/src/LambdaCalculus/Expression.hs +++ b/src/LambdaCalculus/Expression.hs @@ -12,6 +12,7 @@ module LambdaCalculus.Expression , pattern FixC, pattern FixFC, pattern HoleC, pattern HoleFC , Type (..), TypeF (..), Scheme (..), tapp , ast2check, ast2eval, check2eval, check2ast, eval2ast + , builtins ) where import LambdaCalculus.Evaluator.Base diff --git a/src/LambdaCalculus/Syntax/Parser.hs b/src/LambdaCalculus/Syntax/Parser.hs index 0876be1..8ffb08f 100644 --- a/src/LambdaCalculus/Syntax/Parser.hs +++ b/src/LambdaCalculus/Syntax/Parser.hs @@ -1,6 +1,8 @@ module LambdaCalculus.Syntax.Parser - ( ParseError - , parseAST + ( ParseError, parse + , DeclOrExprAST, ProgramAST + , parseAST, parseDeclOrExpr, parseProgram + , astParser, declOrExprParser, programParser ) where import LambdaCalculus.Syntax.Base @@ -8,10 +10,25 @@ import LambdaCalculus.Syntax.Base import Data.List.NonEmpty (fromList) import Data.Text qualified as T import Prelude hiding (succ, either) -import Text.Parsec hiding (label, token) +import Text.Parsec hiding (label, token, spaces) import Text.Parsec qualified import Text.Parsec.Text (Parser) +spaces :: Parser () +spaces = Text.Parsec.spaces >> optional (try (comment >> spaces)) + where + comment, lineComment, blockComment :: Parser () + comment = blockComment <|> lineComment + lineComment = label "line comment" $ do + _ <- try (string "//") + _ <- many1 (noneOf "\n") + pure () + blockComment = label "block comment" $ do + _ <- try (string "/*") + _ <- many1 $ notFollowedBy (string "*/") >> anyChar + _ <- string "*/" + pure () + label :: String -> Parser a -> Parser a label = flip Text.Parsec.label @@ -55,15 +72,18 @@ abstraction :: Parser AST abstraction = label "lambda abstraction" $ Abs <$> between lambda (token '.') (many1' identifier) <*> ambiguous where lambda = label "lambda" $ (char '\\' <|> char 'λ') *> spaces +definition :: Parser (Def Parse) +definition = do + name <- identifier + token '=' + value <- ambiguous + pure (name, value) + let_ :: Parser AST let_ = Let <$> between (keyword "let") (keyword "in") (fromList <$> definitions) <*> ambiguous where definitions :: Parser [Def Parse] - definitions = flip sepBy1 (token ';') do - name <- identifier - token '=' - value <- ambiguous - pure (name, value) + definitions = sepBy1 definition (token ';') ctr :: Parser AST ctr = pair <|> unit <|> either <|> nat <|> list <|> str @@ -158,5 +178,32 @@ block = label "block expression" $ abstraction <|> let_ <|> finite ambiguous :: Parser AST ambiguous = label "any expression" $ try application <|> block +astParser :: Parser AST +astParser = ambiguous + parseAST :: Text -> Either ParseError AST parseAST = parse (spaces *> ambiguous <* eof) "input" + +type Declaration = (Text, AST) + +declaration :: Parser Declaration +declaration = do + notFollowedBy (try let_) + keyword "let" + definition + +-- | A program is a series of declarations and expressions to execute. +type ProgramAST = [DeclOrExprAST] +type DeclOrExprAST = Either Declaration AST + +declOrExprParser :: Parser DeclOrExprAST +declOrExprParser = try (Left <$> declaration) <|> (Right <$> ambiguous) + +programParser :: Parser ProgramAST +programParser = spaces *> sepEndBy declOrExprParser (token ';') <* eof + +parseDeclOrExpr :: Text -> Either ParseError DeclOrExprAST +parseDeclOrExpr = parse declOrExprParser "input" + +parseProgram :: Text -> Either ParseError ProgramAST +parseProgram = parse programParser "input"