From 4541f30f463a60fb915375a3d60e654dec06bad9 Mon Sep 17 00:00:00 2001 From: James Martin Date: Mon, 15 Mar 2021 23:56:52 -0700 Subject: [PATCH] Lots of refactors using recursion-schemes, plus hacky code cleanup. A side-effect of this refactoring was that I got `traceEval` for free! --- app/Main.hs | 4 +- package.yaml | 9 + src/Data/Stream.hs | 26 +++ src/LambdaCalculus.hs | 200 ++++++++++++-------- src/LambdaCalculus/Expression.hs | 60 +++--- src/LambdaCalculus/Parser/AbstractSyntax.hs | 81 +++++--- 6 files changed, 238 insertions(+), 142 deletions(-) create mode 100644 src/Data/Stream.hs diff --git a/app/Main.hs b/app/Main.hs index 66b7c95..e2ffc04 100644 --- a/app/Main.hs +++ b/app/Main.hs @@ -1,8 +1,8 @@ -module Main where +module Main (main) where import Control.Monad (forever) import Data.Text -import qualified Data.Text.IO as TIO +import Data.Text.IO qualified as TIO import LambdaCalculus (eval) import LambdaCalculus.Parser (parseExpression) import System.IO (hFlush, stdout) diff --git a/package.yaml b/package.yaml index 16a0e84..f83cd1d 100644 --- a/package.yaml +++ b/package.yaml @@ -14,16 +14,24 @@ extra-source-files: default-extensions: - BlockArguments +- FlexibleContexts - ImportQualifiedPost - LambdaCase - OverloadedStrings - PatternSynonyms - ViewPatterns +# Required for use of recursion-schemes +- DeriveFoldable +- DeriveFunctor +- DeriveTraversable +- TemplateHaskell +- TypeFamilies dependencies: - base >= 4.14 && < 5 - mtl >= 2.2 && < 3 - parsec >= 3.1 && < 4 +- recursion-schemes >= 5.2 && < 6 - text >= 1.2 && < 2 - text-show >= 3.9 && < 4 - unordered-containers >= 0.2.13 && < 0.3 @@ -42,6 +50,7 @@ library: # Less stupid warnings, but I still don't care - -Wno-unused-do-bind - -Wno-all-missed-specialisations + - -Wno-missing-local-signatures # Explicit import lists are generally a good thing, but I don't want them # in certain cases (e.g. importing my own modules, task-specific modules like the parser). - -Wno-missing-import-lists diff --git a/src/Data/Stream.hs b/src/Data/Stream.hs new file mode 100644 index 0000000..df585e1 --- /dev/null +++ b/src/Data/Stream.hs @@ -0,0 +1,26 @@ +module Data.Stream (Stream (Cons), filter, fromList) where + +import Data.Functor.Foldable (Base, Corecursive, Recursive, embed, project, ana) +import Prelude hiding (filter, head, tail) + +data Stream a = Cons a (Stream a) + +type instance Base (Stream a) = (,) a + +instance Recursive (Stream a) where + project (Cons x xs) = (x, xs) + +instance Corecursive (Stream a) where + embed (x, xs) = Cons x xs + +filter :: (a -> Bool) -> Stream a -> Stream a +filter p = ana \case + Cons x xs + | p x -> (x, xs) + | otherwise -> project xs + +fromList :: [a] -> Stream a +fromList = ana coalg + where + coalg (x : xs) = (x, xs) + coalg [] = error "Attempted to turn finite list into stream" diff --git a/src/LambdaCalculus.hs b/src/LambdaCalculus.hs index 4f01dae..1b22300 100644 --- a/src/LambdaCalculus.hs +++ b/src/LambdaCalculus.hs @@ -1,106 +1,156 @@ module LambdaCalculus ( module LambdaCalculus.Expression - , eval + , eval, traceEval ) where -import Control.Monad.State (State, evalState, modify', state, put, gets) -import Data.List (find) -import Data.Maybe (fromJust) +import Control.Monad.Except (MonadError, ExceptT, throwError, runExceptT) +import Control.Monad.State (MonadState, State, evalState, modify', state, put, gets) +import Control.Monad.Writer (runWriterT, tell) +import Data.Functor.Foldable (cata, para, project, embed) import Data.HashSet (HashSet) import Data.HashSet qualified as HS +import Data.Stream (Stream) +import Data.Stream qualified as S import Data.Text (Text) import Data.Text qualified as T +import Data.Void (Void, absurd) import LambdaCalculus.Continuation -import LambdaCalculus.Expression (Expression (..), foldExpr) +import LambdaCalculus.Expression (Expression (..), ExpressionF (..)) -- | Free variables are variables which are present in an expression but not bound by any abstraction. freeVariables :: Expression -> HashSet Text -freeVariables = foldExpr HS.singleton HS.union HS.delete +freeVariables = cata \case + VariableF name -> HS.singleton name + ApplicationF e1 e2 -> HS.union e1 e2 + AbstractionF n e -> HS.delete n e + ContinuationF e -> HS.delete "!" e --- FIXME -quickHack :: Expression -> Expression -quickHack (Continuation name body) = Abstraction name body -quickHack e = e +-- | Bound variables are variables which are bound by any form of abstraction in an expression. +boundVariables :: Expression -> HashSet Text +boundVariables = cata \case + VariableF _ -> HS.empty + ApplicationF e1 e2 -> HS.union e1 e2 + AbstractionF n e -> HS.insert n e + ContinuationF e -> HS.insert "!" e + +-- | Variables that occur anywhere in an experession, bound or free. +usedVariables :: Expression -> HashSet Text +usedVariables x = HS.union (freeVariables x) (boundVariables x) + +-- | Generate a stream of new variables which are not in the set of provided variables. +freshVariables :: HashSet Text -> Stream Text +freshVariables ctx = S.filter (not . flip HS.member ctx) $ S.fromList $ fmap T.pack $ (:) <$> ['a'..'z'] <*> map show [0 :: Int ..] + +-- | Create a new variable which is not used anywhere else. +fresh :: State (Stream Text) Text +fresh = state project -- | Substitution is the process of replacing all free occurrences of a variable in one expression with another expression. substitute :: Text -> Expression -> Expression -> Expression -substitute var1 value unmodified@(Variable var2) - | var1 == var2 = value - | otherwise = unmodified -substitute var value (Application ef ex) - = Application (substitute var value ef) (substitute var value ex) -substitute var1 value unmodified@(quickHack -> Abstraction var2 body) - | var1 == var2 = unmodified - | otherwise = constructor var2' $ substitute var1 value $ alphaConvert var2 var2' body +substitute var val = unsafeSubstitute var val . alphaConvert (usedVariables val) + +-- | Rename the bound variables in `e` so they do not overlap any variables used in `ctx`. +-- +-- This is used as part of substitution when substituting `val` with free variables `ctx` into `e`, +-- because it prevents any of the binders in `e` from accidentally capturing a free variable in `ctx`. +alphaConvert :: HashSet Text -> Expression -> Expression +alphaConvert ctx e_ = evalState (rename e_) $ freshVariables $ HS.union (usedVariables e_) ctx where - constructor = case unmodified of - Abstraction _ _ -> Abstraction - Continuation _ _ -> Continuation - _ -> error "impossible" + rename :: Expression -> State (Stream Text) Expression + rename = cata \case + VariableF var -> pure $ Variable var + ApplicationF ef ex -> Application <$> ef <*> ex + ContinuationF e -> Continuation <$> e + AbstractionF n e + | HS.member n ctx -> do + n' <- fresh + Abstraction n' . unsafeSubstitute n (Variable n') <$> e + | otherwise -> Abstraction n <$> e - var2' :: Text - var2' = escapeName (freeVariables value) var2 - - alphaConvert :: Text -> Text -> Expression -> Expression - alphaConvert oldName newName expr = substitute oldName (Variable newName) expr - -- | Generate a new name which isn't present in the set, based on the old name. - escapeName :: HashSet Text -> Text -> Text - escapeName env name = fromJust $ find (not . free) names - where names :: [Text] - names = name : map (`T.snoc` '\'') names - - free :: Text -> Bool - free = (`HS.member` env) -substitute _ _ _ = error "impossible" - -type EvaluatorM a = State Continuation a -type Evaluator = Expression -> EvaluatorM Expression +-- | Substitution with the assumption that no free variables in the value are bound in the expression. +unsafeSubstitute :: Text -> Expression -> Expression -> Expression +unsafeSubstitute var val = para \case + e' + | VariableF var2 <- e', var == var2 -> val + | ApplicationF (_, ef) (_, ex) <- e' -> Application ef ex + | ContinuationF (_, e) <- e', var /= "!" -> Continuation e + | AbstractionF var2 (_, e) <- e', var /= var2 -> Abstraction var2 e + | otherwise -> embed $ fmap fst e' isReducible :: Expression -> Bool -isReducible (Application (quickHack -> (Abstraction _ _)) _) = True -isReducible (Application (Variable "callcc") _) = True -isReducible (Application ef ex) = isReducible ef || isReducible ex -isReducible _ = False +isReducible = snd . cata \case + ApplicationF ctr args -> eliminator ctr [args] + VariableF "callcc" -> constructor + AbstractionF _ _ -> constructor + ContinuationF _ -> constructor + VariableF _ -> constant + where + -- | Constants are irreducible in any context. + constant = (False, False) + -- | Constructors are reducible if an eliminator is applied to them. + constructor = (True, False) + -- | Eliminators are reducible if they are applied to a constructor or their arguments are reducible. + eliminator ctr args = (False, fst ctr || snd ctr || any snd args) -push :: ContinuationCrumb -> EvaluatorM () +push :: MonadState Continuation m => ContinuationCrumb -> m () push c = modify' (c :) -pop :: EvaluatorM (Maybe ContinuationCrumb) +pop :: MonadState Continuation m => m (Maybe ContinuationCrumb) pop = state \case [] -> (Nothing, []) (crumb:k) -> (Just crumb, k) -ret :: Expression -> EvaluatorM Expression -ret e = pop >>= maybe (pure e) (evaluator . continue1 e) +ret :: (MonadError Expression m, MonadState Continuation m) => Expression -> m Expression +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 + +-- | Iteratively call an action until it 'throws' a return value. +loop :: Monad m => (a -> ExceptT b m a) -> a -> m b +loop f = fmap fromLeft . runExceptT . iterateM_ f -- | A call-by-value expression evaluator. -evaluator :: Evaluator -evaluator unmodified@(Application ef ex) - -- First reduce the argument... - | isReducible ex = do - push (AppliedTo ef) - evaluator ex - -- then reduce the function... - | isReducible ef = do - push (ApplyTo ex) - evaluator ef - | otherwise = case ef of - -- perform beta reduction if possible... - Abstraction name body -> - evaluator $ substitute name ex body - -- perform continuation calls if possible... - Continuation name body -> do - put [] - evaluator $ substitute name ex body - -- capture the current continuation if requested... - Variable "callcc" -> do - -- Don't worry about variable capture here for now. - k <- gets $ continue (Variable "!") - evaluator (Application ex (Continuation "!" k)) - -- otherwise the value is irreducible and we can continue evaluation. - _ -> ret unmodified --- Neither abstractions nor variables are reducible. -evaluator e = ret e +evaluatorStep :: (MonadError Expression m, MonadState Continuation m) => Expression -> m Expression +evaluatorStep = \case + unmodified@(Application ef ex) + -- First reduce the argument... + | isReducible ex -> do + push (AppliedTo ef) + pure ex + -- then reduce the function... + | isReducible ef -> do + push (ApplyTo ex) + pure ef + | otherwise -> case ef of + -- perform beta reduction if possible... + Abstraction name body -> + pure $ substitute name ex body + -- perform continuation calls if possible... + Continuation body -> do + put [] + pure $ substitute "!" ex body + -- capture the current continuation if requested... + Variable "callcc" -> do + -- Don't worry about variable capture here for now. + k <- gets $ continue (Variable "!") + pure $ Application ex (Continuation k) + -- otherwise the value is irreducible and we can continue evaluation. + _ -> ret unmodified + -- Neither abstractions nor variables are reducible. + e -> ret e eval :: Expression -> Expression -eval = flip evalState [] . evaluator +eval = flip evalState [] . loop evaluatorStep + +traceEval :: Expression -> (Expression, [Expression]) +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. + tell [e] + evaluatorStep e diff --git a/src/LambdaCalculus/Expression.hs b/src/LambdaCalculus/Expression.hs index 9a68318..2b30d64 100644 --- a/src/LambdaCalculus/Expression.hs +++ b/src/LambdaCalculus/Expression.hs @@ -1,9 +1,8 @@ module LambdaCalculus.Expression - ( Expression (..), foldExpr + ( Expression (..), ExpressionF (..) , ast2expr, expr2ast , pattern Lets, pattern Abstractions, pattern Applications , viewLet, viewAbstraction, viewApplication - , basicShow ) where -- The definition of Expression is in its own file because: @@ -14,13 +13,16 @@ module LambdaCalculus.Expression -- * I don't want to clutter the module focusing on the actual evaluation -- with all of these irrelevant conversion operators. -import Data.Bifunctor (first, second) +import Data.Bifunctor (first) +import Data.Functor.Foldable (ana, cata) +import Data.Functor.Foldable.TH (makeBaseFunctor) +import Data.List (foldl1') import Data.List.NonEmpty (NonEmpty ((:|)), fromList, toList) import Data.Text (Text) import Data.Text qualified as T import LambdaCalculus.Parser.AbstractSyntax (AbstractSyntax) import LambdaCalculus.Parser.AbstractSyntax qualified as AST -import TextShow (Builder, fromText, TextShow, showb, showt) +import TextShow (TextShow, showb, showt) data Expression = Variable Text @@ -33,37 +35,22 @@ data Expression -- deleting the current continuation. -- -- Continuations do not have any corresponding surface-level syntax. - | Continuation Text Expression + | Continuation Expression deriving Eq -foldExpr :: (Text -> a) -> (a -> a -> a) -> (Text -> a -> a) -> Expression -> a -foldExpr varf appf absf = foldExpr' - where - foldExpr' (Variable name) = varf name - foldExpr' (Application ef ex) = appf (foldExpr' ef) (foldExpr' ex) - foldExpr' (Abstraction name body) = absf name (foldExpr' body) - -- This isn't technically correct, but it's good enough for every place I use this. - -- I'll figure out a proper solution later, or possibly just rip out this function. - foldExpr' (Continuation name body) = absf name (foldExpr' body) - --- | A naive implementation of 'show', which does not take advantage of any syntactic sugar --- and always emits optional parentheses. -basicShow :: Expression -> Builder -basicShow (Variable var) = fromText var -basicShow (Application ef ex) = "(" <> showb ef <> " " <> showb ex <> ")" -basicShow (Abstraction var body) = "(λ" <> fromText var <> ". " <> showb body <> ")" -basicShow (Continuation var body) = "(Λ" <> fromText var <> ". " <> showb body <> ")" +makeBaseFunctor ''Expression -- | Convert from an abstract syntax tree to an expression. ast2expr :: AbstractSyntax -> Expression -ast2expr (AST.Variable name) = Variable name -ast2expr (AST.Application (x :| [])) = ast2expr x -ast2expr (AST.Application xs) = foldl1 Application $ map ast2expr (toList xs) -ast2expr (AST.Abstraction names body) = foldr Abstraction (ast2expr body) names -ast2expr (AST.Let defs body) = foldr (uncurry letExpr . second ast2expr) (ast2expr body) defs - where - letExpr :: Text -> Expression -> Expression -> Expression - letExpr name val body' = Application (Abstraction name body') val +ast2expr = cata \case + AST.VariableF name -> Variable name + AST.ApplicationF es -> case es of + x :| [] -> x + xs -> foldl1' Application (toList xs) + AST.AbstractionF names body -> foldr Abstraction body (toList names) + AST.LetF defs body -> + let letExpr name val body' = Application (Abstraction name body') val + in foldr (uncurry letExpr) body defs -- | View nested applications of abstractions as a list. pattern Lets :: [(Text, Expression)] -> Expression -> Expression @@ -88,18 +75,19 @@ pattern Applications exprs <- (viewApplication -> exprs@(_:_:_)) {-# COMPLETE Abstractions, Applications, Continuation, Variable :: Expression #-} viewApplication :: Expression -> [Expression] -viewApplication (Application ef ex) = ex : viewApplication ef +viewApplication (Application ef ex) = viewApplication ef ++ [ex] viewApplication x = [x] -- | Convert from an expression to an abstract syntax tree. -- -- This function will use let, and applications and abstractions of multiple values when possible. expr2ast :: Expression -> AbstractSyntax -expr2ast (Lets defs body) = AST.Let (fromList $ map (second expr2ast) defs) $ expr2ast body -expr2ast (Abstractions names body) = AST.Abstraction (fromList names) $ expr2ast body -expr2ast (Applications exprs) = AST.Application $ fromList $ map expr2ast $ reverse exprs -expr2ast (Variable name) = AST.Variable name -expr2ast (Continuation _ body) = AST.Abstraction ("!" :| []) (expr2ast body) +expr2ast = ana \case + Lets defs body -> AST.LetF (fromList defs) body + Abstractions names body -> AST.AbstractionF (fromList names) body + Applications exprs -> AST.ApplicationF $ fromList exprs + Continuation body -> AST.AbstractionF ("!" :| []) body + Variable name -> AST.VariableF name instance TextShow Expression where showb = showb . expr2ast diff --git a/src/LambdaCalculus/Parser/AbstractSyntax.hs b/src/LambdaCalculus/Parser/AbstractSyntax.hs index ba52e9e..0b6edb3 100644 --- a/src/LambdaCalculus/Parser/AbstractSyntax.hs +++ b/src/LambdaCalculus/Parser/AbstractSyntax.hs @@ -1,9 +1,11 @@ module LambdaCalculus.Parser.AbstractSyntax - ( AbstractSyntax (..), Definition, Identifier + ( AbstractSyntax (..), AbstractSyntaxF (..), Definition, Identifier ) where -import Data.Bifunctor (first) -import Data.List.NonEmpty (NonEmpty ((:|)), fromList, toList) +import Data.Functor.Base (NonEmptyF (NonEmptyF)) +import Data.Functor.Foldable (cata) +import Data.Functor.Foldable.TH (makeBaseFunctor) +import Data.List.NonEmpty (NonEmpty, toList) import Data.Text (Text) import Data.Text qualified as T import TextShow (Builder, TextShow, showb, showt, toText, fromText) @@ -38,36 +40,57 @@ data AbstractSyntax type Definition = (Identifier, AbstractSyntax) type Identifier = Text +makeBaseFunctor ''AbstractSyntax + -- I'm surprised this isn't in base somewhere. unsnoc :: NonEmpty a -> ([a], a) -unsnoc (x :| []) = ([], x) -unsnoc (x :| xs) = first (x :) (unsnoc (fromList xs)) +unsnoc = cata \case + NonEmptyF x' Nothing -> ([], x') + NonEmptyF x (Just (xs, x')) -> (x : xs, x') + +data SyntaxType + -- | Ambiguous syntax is not necessarily finite and not guaranteed to consume any input. + = Ambiguous + -- | Block syntax is not necessarily finite but is guaranteed to consume input. + | Block + -- | Unambiguous syntax is finite and guaranteed to consume input. + | Finite +type Tagged a = (SyntaxType, a) + +tag :: SyntaxType -> a -> Tagged a +tag = (,) + +group :: Builder -> Builder +group x = "(" <> x <> ")" + +-- | An unambiguous context has a marked beginning and end. +unambiguous :: Tagged Builder -> Builder +unambiguous (_, t) = t + +-- | A final context has a marked end but no marked beginning, +-- so we provide a grouper when a beginning marker is necessary. +final :: Tagged Builder -> Builder +final (Ambiguous, t) = group t +final (_, t) = t + +-- | An ambiguous context has neither a marked end nor marked beginning, +-- so we provide a grouper when an ending marker is necessary. +ambiguous :: Tagged Builder -> Builder +ambiguous (Finite, t) = t +ambiguous (_, t) = group t instance TextShow AbstractSyntax where - showb = unambiguous - where - -- Parentheses are often optional to the parser, but not in every context. - -- The `unambigous` printer is used in contexts where parentheses are optional, and does not include them; - -- the `ambiguous` printer is used when omitting parentheses could result in an incorrect parse. - unambiguous, ambiguous :: AbstractSyntax -> Builder - unambiguous (Variable name) = fromText name - unambiguous (Application (unsnoc -> (es, final))) = foldr (\e es' -> ambiguous e <> " " <> es') final' es - where - final' = case final of - Application _ -> ambiguous final - _ -> unambiguous final - unambiguous (Abstraction names body) = "λ" <> names' <> ". " <> unambiguous body - where names' = fromText (T.intercalate " " $ toList names) - unambiguous (Let defs body) = "let " <> defs' <> " in " <> unambiguous body - where - defs' = fromText (T.intercalate "; " $ map (toText . showDef) $ toList defs) - - showDef :: Definition -> Builder - showDef (name, val) = fromText name <> " = " <> unambiguous val - - -- | Adds a grouper if omitting it could result in ambiguous syntax.) - ambiguous e@(Variable _) = unambiguous e - ambiguous e = "(" <> unambiguous e <> ")" + showb = snd . cata \case + VariableF name -> tag Finite $ fromText name + ApplicationF (unsnoc -> (es, efinal)) -> tag Ambiguous $ foldr (\e es' -> ambiguous e <> " " <> es') (final efinal) es + AbstractionF names body -> tag Block $ + let names' = fromText (T.intercalate " " $ toList names) + in "λ" <> names' <> ". " <> unambiguous body + LetF defs body -> tag Block $ + let + showDef (name, val) = fromText name <> " = " <> unambiguous val + defs' = fromText (T.intercalate "; " $ map (toText . showDef) $ toList defs) + in "let " <> defs' <> " in " <> unambiguous body instance Show AbstractSyntax where show = T.unpack . showt