diff --git a/.editorconfig b/.editorconfig index e2139a6..0043c7c 100644 --- a/.editorconfig +++ b/.editorconfig @@ -3,9 +3,6 @@ root = true [*] charset = utf-8 indent_style = space -indent_size = 4 +indent_size = 2 trim_trailing_whitespace = true insert_final_newline = true - -[*.yml] -indent_size = 2 diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index f1f858c..86de72e 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -10,8 +10,8 @@ jobs: - name: Checkout sources uses: actions/checkout@v2 - - name: Install latest Haskell Stack - uses: actions/setup-haskell@v1.1 + - name: Install Haskell toolchain + uses: haskell/actions/setup@v1 with: enable-stack: true diff --git a/app/Main.hs b/app/Main.hs index 9aec129..48dd76a 100644 --- a/app/Main.hs +++ b/app/Main.hs @@ -1,4 +1,3 @@ -{-# LANGUAGE LambdaCase #-} module Main where import Control.Monad (forever) diff --git a/package.yaml b/package.yaml index 2b5bd45..91a01d9 100644 --- a/package.yaml +++ b/package.yaml @@ -15,18 +15,38 @@ extra-source-files: default-extensions: - BlockArguments - ImportQualifiedPost +- LambdaCase - OverloadedStrings +- PatternSynonyms - ViewPatterns dependencies: -- base >= 4.13 && < 5 +- base >= 4.14 && < 5 - parsec >= 3.1 && < 4 - text >= 1.2 && < 2 -- text-show >= 3.8 && < 4 -- unordered-containers >= 0.2.10 && < 0.3 +- text-show >= 3.9 && < 4 +- unordered-containers >= 0.2.13 && < 0.3 library: source-dirs: src + ghc-options: + - -Weverything + # Useless Safe Haskell warnings + - -Wno-missing-safe-haskell-mode + - -Wno-unsafe + - -Wno-safe + # Other stupid warnings + - -Wno-implicit-prelude + - -Wno-missing-deriving-strategies + # Less stupid warnings, but I still don't care + - -Wno-unused-do-bind + - -Wno-all-missed-specialisations + # 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 + # I intentionally include unused top-level bindings + # as a way of documenting and explaining concepts. + - -Wno-unused-top-binds executables: jtm-lambda-calculus: @@ -50,7 +70,7 @@ tests: dependencies: - jtm-lambda-calculus - generic-random >= 1.2 && < 2 - - QuickCheck >= 2.13 && < 3 + - QuickCheck >= 2.14 && < 3 - tasty >= 1.2 && < 2 - tasty-hunit >= 0.10 && < 0.11 - tasty-quickcheck >= 0.10.1 && < 0.11 diff --git a/src/LambdaCalculus.hs b/src/LambdaCalculus.hs index 5947bea..b654156 100644 --- a/src/LambdaCalculus.hs +++ b/src/LambdaCalculus.hs @@ -1,7 +1,7 @@ module LambdaCalculus - ( module LambdaCalculus.Expression - , eagerEval, lazyEval - ) where + ( module LambdaCalculus.Expression + , eagerEval, lazyEval + ) where import Data.List (elemIndex, find) import Data.Maybe (fromJust) @@ -38,47 +38,51 @@ closed = HS.null . freeVariables -- i.e. one can be converted to the other using only alpha-conversion. alphaEquivalent :: Expression -> Expression -> Bool alphaEquivalent = alphaEquivalent' [] [] - where alphaEquivalent' :: [Text] -> [Text] -> Expression -> Expression -> Bool - alphaEquivalent' ctx1 ctx2 (Variable v1) (Variable v2) - -- Two variables are alpha-equivalent if they are bound in the same location. - = bindingSite ctx1 v1 == bindingSite ctx2 v2 - alphaEquivalent' ctx1 ctx2 (Application ef1 ex1) (Application ef2 ex2) - -- Two applications are alpha-equivalent if their components are alpha-equivalent. - = alphaEquivalent' ctx1 ctx2 ef1 ef2 - && alphaEquivalent' ctx1 ctx2 ex1 ex2 - alphaEquivalent' ctx1 ctx2 (Abstraction v1 b1) (Abstraction v2 b2) - -- Two abstractions are alpha-equivalent if their bodies are alpha-equivalent. - = alphaEquivalent' (v1 : ctx1) (v2 : ctx2) b1 b2 + where + alphaEquivalent' :: [Text] -> [Text] -> Expression -> Expression -> Bool + alphaEquivalent' ctx1 ctx2 (Variable v1) (Variable v2) + -- Two variables are alpha-equivalent if they are bound in the same location. + = bindingSite ctx1 v1 == bindingSite ctx2 v2 + alphaEquivalent' ctx1 ctx2 (Application ef1 ex1) (Application ef2 ex2) + -- Two applications are alpha-equivalent if their components are alpha-equivalent. + = alphaEquivalent' ctx1 ctx2 ef1 ef2 + && alphaEquivalent' ctx1 ctx2 ex1 ex2 + alphaEquivalent' ctx1 ctx2 (Abstraction v1 b1) (Abstraction v2 b2) + -- Two abstractions are alpha-equivalent if their bodies are alpha-equivalent. + = alphaEquivalent' (v1 : ctx1) (v2 : ctx2) b1 b2 + alphaEquivalent' _ _ _ _ = False - -- | The binding site of a variable is either the index of its binder - -- or, if it is unbound, the name of the free variable. - bindingSite :: [Text] -> Text -> Either Text Int - bindingSite ctx var = maybeToRight var $ var `elemIndex` ctx - where maybeToRight :: b -> Maybe a -> Either b a - maybeToRight default_ = maybe (Left default_) Right + -- | The binding site of a variable is either the index of its binder + -- or, if it is unbound, the name of the free variable. + bindingSite :: [Text] -> Text -> Either Text Int + bindingSite ctx var = maybeToRight var $ var `elemIndex` ctx + where maybeToRight :: b -> Maybe a -> Either b a + maybeToRight default_ = maybe (Left default_) Right -- | 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 + | var1 == var2 = value | otherwise = unmodified substitute var value (Application ef ex) = Application (substitute var value ef) (substitute var value ex) substitute var1 value unmodified@(Abstraction var2 body) | var1 == var2 = unmodified | otherwise = Abstraction var2' $ substitute var1 value $ alphaConvert var2 var2' body - where var2' :: Text - var2' = escapeName (freeVariables value) var2 + where + 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) + 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) -- | Returns True if the top-level expression is reducible by beta-reduction. betaRedex :: Expression -> Bool @@ -110,22 +114,25 @@ whnf (Application (Abstraction _ _) _) = False whnf (Abstraction var1 (Application fe (Variable var2))) = var1 /= var2 || var1 `freeIn` fe whnf (Application ef _) = whnf ef +whnf _ = True eval :: (Expression -> Expression) -> Expression -> Expression eval strategy = eval' - where eval' :: Expression -> Expression - eval' (Application ef ex) = - case ef' of - -- Beta-reduction - Abstraction var body -> eval' $ substitute var ex' body - _ -> Application ef' ex' - where ef' = eval' ef - ex' = strategy ex - eval' unmodified@(Abstraction var1 (Application ef (Variable var2))) - -- Eta-reduction - | var1 == var2 && not (var1 `freeIn` ef) = eval' ef - | otherwise = unmodified - eval' x = x + where + eval' :: Expression -> Expression + eval' (Application ef ex) = + case ef' of + -- Beta-reduction + Abstraction var body -> eval' $ substitute var ex' body + _ -> Application ef' ex' + where + ef' = eval' ef + ex' = strategy ex + eval' unmodified@(Abstraction var1 (Application ef (Variable var2))) + -- Eta-reduction + | var1 == var2 && not (var1 `freeIn` ef) = eval' ef + | otherwise = unmodified + eval' x = x -- | Reduce an expression to normal form. eagerEval :: Expression -> Expression diff --git a/src/LambdaCalculus/Expression.hs b/src/LambdaCalculus/Expression.hs index 12640ce..97ab1e5 100644 --- a/src/LambdaCalculus/Expression.hs +++ b/src/LambdaCalculus/Expression.hs @@ -1,5 +1,11 @@ {-# LANGUAGE DeriveGeneric #-} -module LambdaCalculus.Expression where +module LambdaCalculus.Expression + ( Expression (Variable, Application, Abstraction) + , ast2expr, expr2ast + , pattern Lets, pattern Abstractions, pattern Applications + , viewLet, viewAbstraction, viewApplication + , basicShow + ) where -- The definition of Expression is in its own file because: -- * Expression and AbstractSyntax should not be in the same file @@ -10,18 +16,21 @@ module LambdaCalculus.Expression where -- with all of these irrelevant conversion operators. import Data.Bifunctor (first, second) +import Data.List.NonEmpty (NonEmpty ((:|)), fromList, toList) import Data.Text (Text) import Data.Text qualified as T import GHC.Generics (Generic) import LambdaCalculus.Parser.AbstractSyntax (AbstractSyntax) import LambdaCalculus.Parser.AbstractSyntax qualified as AST -import TextShow +import TextShow (Builder, fromText, TextShow, showb, showt) data Expression - = Variable Text - | Application Expression Expression - | Abstraction Text Expression - deriving (Eq, Generic) + = Variable Text + -- | Function application: `(f x)`. + | Application Expression Expression + -- | Lambda abstraction: `(λx. e)`. + | Abstraction Text Expression + deriving (Eq, Generic) -- | A naive implementation of 'show', which does not take advantage of any syntactic sugar -- and always emits optional parentheses. @@ -33,26 +42,36 @@ basicShow (Abstraction var body) = "(λ" <> fromText var <> ". " <> showb body < -- | Convert from an abstract syntax tree to an expression. ast2expr :: AbstractSyntax -> Expression ast2expr (AST.Variable name) = Variable name -ast2expr (AST.Application []) = Abstraction "x" (Variable "x") -ast2expr (AST.Application [x]) = ast2expr x -ast2expr (AST.Application xs) = foldl1 Application $ map ast2expr xs -ast2expr (AST.Abstraction [] body) = ast2expr body +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 + where + letExpr :: Text -> Expression -> Expression -> Expression + letExpr name val body' = Application (Abstraction name body') val -- | View nested applications of abstractions as a list. +pattern Lets :: [(Text, Expression)] -> Expression -> Expression +pattern Lets defs body <- (viewLet -> (defs@(_:_), body)) + viewLet :: Expression -> ([(Text, Expression)], Expression) viewLet (Application (Abstraction var body) x) = first ((var, x) :) (viewLet body) viewLet x = ([], x) -- | View nested abstractions as a list. +pattern Abstractions :: [Text] -> Expression -> Expression +pattern Abstractions names body <- (viewAbstraction -> (names@(_:_), body)) + viewAbstraction :: Expression -> ([Text], Expression) viewAbstraction (Abstraction name body) = first (name :) (viewAbstraction body) viewAbstraction x = ([], x) -- | View left-nested applications as a list. +pattern Applications :: [Expression] -> Expression +pattern Applications exprs <- (viewApplication -> (exprs@(_:_:_))) + +{-# COMPLETE Abstractions, Applications, Variable :: Expression #-} + viewApplication :: Expression -> [Expression] viewApplication (Application ef ex) = ex : viewApplication ef viewApplication x = [x] @@ -61,9 +80,9 @@ viewApplication x = [x] -- -- This function will use let, and applications and abstractions of multiple values when possible. expr2ast :: Expression -> AbstractSyntax -expr2ast (viewLet -> (defs@(_:_), body)) = AST.Let (map (second expr2ast) defs) $ expr2ast body -expr2ast (viewAbstraction -> (names@(_:_), body)) = AST.Abstraction names $ expr2ast body -expr2ast (viewApplication -> es@(_:_:_)) = AST.Application $ map expr2ast $ reverse es +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 instance TextShow Expression where diff --git a/src/LambdaCalculus/Parser.hs b/src/LambdaCalculus/Parser.hs index 0b29b06..7e76aaf 100644 --- a/src/LambdaCalculus/Parser.hs +++ b/src/LambdaCalculus/Parser.hs @@ -1,18 +1,13 @@ -module LambdaCalculus.Parser - ( parseAST, parseExpression - ) where +module LambdaCalculus.Parser (parseAST, parseExpression) where -import Control.Applicative ((*>)) -import Control.Monad (void) +import Data.List.NonEmpty (fromList) import Data.Text (Text) -import qualified Data.Text as T +import Data.Text qualified as T import LambdaCalculus.Expression (Expression, ast2expr) -import qualified LambdaCalculus.Expression as Expr import LambdaCalculus.Parser.AbstractSyntax import Text.Parsec hiding (label, token) import Text.Parsec qualified import Text.Parsec.Text (Parser) -import TextShow label :: String -> Parser a -> Parser a label = flip Text.Parsec.label @@ -26,10 +21,10 @@ keywords = ["let", "in"] -- | A keyword is an exact string which is not part of an identifier. keyword :: Text -> Parser () keyword kwd = label (T.unpack kwd) $ do - try do - string $ T.unpack kwd - notFollowedBy letter - spaces + try do + string $ T.unpack kwd + notFollowedBy letter + spaces -- | An identifier is a sequence of letters which is not a keyword. identifier :: Parser Identifier @@ -48,22 +43,22 @@ grouping :: Parser AbstractSyntax grouping = label "grouping" $ between (token '(') (token ')') expression application :: Parser AbstractSyntax -application = Application <$> many2 applicationTerm - where applicationTerm :: Parser AbstractSyntax - applicationTerm = abstraction <|> let_ <|> grouping <|> variable +application = Application . fromList <$> many2 applicationTerm + where applicationTerm = abstraction <|> let_ <|> grouping <|> variable abstraction :: Parser AbstractSyntax -abstraction = label "lambda abstraction" $ Abstraction <$> between lambda (token '.') (many1 identifier) <*> expression - where lambda = label "lambda" $ (char '\\' <|> char 'λ') *> spaces +abstraction = label "lambda abstraction" $ Abstraction <$> between lambda (token '.') (fromList <$> many1 identifier) <*> expression + where lambda = label "lambda" $ (char '\\' <|> char 'λ') *> spaces let_ :: Parser AbstractSyntax -let_ = Let <$> between (keyword "let") (keyword "in") definitions <*> expression - where definitions :: Parser [Definition] - definitions = flip sepBy1 (token ';') do - name <- identifier - token '=' - value <- expression - pure (name, value) +let_ = Let <$> between (keyword "let") (keyword "in") (fromList <$> definitions) <*> expression + where + definitions :: Parser [Definition] + definitions = flip sepBy1 (token ';') do + name <- identifier + token '=' + value <- expression + pure (name, value) expression :: Parser AbstractSyntax expression = label "expression" $ abstraction <|> let_ <|> try application <|> grouping <|> variable diff --git a/src/LambdaCalculus/Parser/AbstractSyntax.hs b/src/LambdaCalculus/Parser/AbstractSyntax.hs index 8c84e85..ba52e9e 100644 --- a/src/LambdaCalculus/Parser/AbstractSyntax.hs +++ b/src/LambdaCalculus/Parser/AbstractSyntax.hs @@ -1,11 +1,12 @@ module LambdaCalculus.Parser.AbstractSyntax - ( AbstractSyntax (..), Definition, Identifier - ) where + ( AbstractSyntax (..), Definition, Identifier + ) where import Data.Bifunctor (first) +import Data.List.NonEmpty (NonEmpty ((:|)), fromList, toList) import Data.Text (Text) import Data.Text qualified as T -import TextShow +import TextShow (Builder, TextShow, showb, showt, toText, fromText) -- | The abstract syntax tree reflects the structure of the externally-visible syntax. -- @@ -14,42 +15,59 @@ import TextShow -- would become unnecessarily complicated, because the same expression -- can be represented in terms of multiple abstract syntax trees. data AbstractSyntax - = Variable Identifier - | Application [AbstractSyntax] - | Abstraction [Identifier] AbstractSyntax - | Let [Definition] AbstractSyntax + = Variable Identifier + -- There is no technical reason for the AST to forbid nullary applications and so forth. + -- However the parser rejects them to avoid confusing edge cases like `let x=in`, + -- so they're forbidden here too so that the syntax tree can't contain data + -- that the parser would refuse to accept. + -- + -- As a matter of curiosity, here's why `let x=in` was syntactically valid: + -- 1. Parentheses in `let` statements are optional, infer them: `let x=()in()`. + -- 2. Insert optional whitespace: `let x = () in ()`. + -- 3. Nullary application expands to the identity function because + -- the identity function is the left identity of function application: + -- `let x=(\x.x) in \x.x`. + -- + -- | n-ary function application: `(f x_1 x_2 ... x_n)`. + | Application (NonEmpty AbstractSyntax) + -- | Lambda abstraction over n variables: `(λx_1 x_2 ... x_n. e)` + | Abstraction (NonEmpty Identifier) AbstractSyntax + -- | Let expressions (syntactic sugar) binding `n` variables: + -- `let x_1 = e_1; x_2 = e_2; ... x_n = e_n`. + | Let (NonEmpty Definition) AbstractSyntax type Definition = (Identifier, AbstractSyntax) type Identifier = Text -- I'm surprised this isn't in base somewhere. -unsnoc :: [a] -> ([a], a) -unsnoc [x] = ([], x) -unsnoc (x : xs) = first (x :) (unsnoc xs) +unsnoc :: NonEmpty a -> ([a], a) +unsnoc (x :| []) = ([], x) +unsnoc (x :| xs) = first (x :) (unsnoc (fromList xs)) instance TextShow AbstractSyntax where - showb = unambiguous - where - unambiguous, ambiguous :: AbstractSyntax -> Builder - unambiguous (Variable name) = fromText name - -- There's no technical reason for the AST to forbid nullary applications and so forth. - -- However the parser rejects them to avoid confusing edge cases like `let x=in`, - -- so they're forbidden here too so that `show` will never print anything the parser would refuse to accept. - unambiguous (Application []) = error "Empty applications are currently disallowed." - 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 [] _) = error "Empty lambdas are currently disallowed." - unambiguous (Abstraction names body) = "λ" <> fromText (T.intercalate " " names) <> ". " <> unambiguous body - unambiguous (Let [] body) = error "Empty lets are currently disallowed." - unambiguous (Let defs body) = "let " <> fromText (T.intercalate "; " $ map (toText . showDef) defs) <> " in " <> unambiguous body - where showDef :: Definition -> Builder - showDef (name, val) = fromText name <> " = " <> unambiguous val + 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) - -- | Adds a grouper if omitting it could result in ambiguous syntax. - -- (Which is to say, the parser would parse it wrong because a different parse has a higher priority.) - ambiguous e@(Variable _) = unambiguous e - ambiguous e = "(" <> unambiguous e <> ")" + 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 <> ")" instance Show AbstractSyntax where - show = T.unpack . showt + show = T.unpack . showt diff --git a/stack.yaml b/stack.yaml index 95e6234..4d3fc11 100644 --- a/stack.yaml +++ b/stack.yaml @@ -1,5 +1,3 @@ -# Nightly is required for the ImportQualifiedPost extension from GHC 8.10. -# An LTS resolver will be used once GHC 8.10 is in an LTS. -resolver: nightly-2020-11-03 +resolver: lts-17.5 packages: - . diff --git a/stack.yaml.lock b/stack.yaml.lock index eef3c43..fa953b3 100644 --- a/stack.yaml.lock +++ b/stack.yaml.lock @@ -6,7 +6,7 @@ packages: [] snapshots: - completed: - size: 544004 - url: https://raw.githubusercontent.com/commercialhaskell/stackage-snapshots/master/nightly/2020/11/3.yaml - sha256: f6988e9a2c92219dc8ff0ebd2d420ede3425fa08cb6613ba47f1bc97c9925aa8 - original: nightly-2020-11-03 + size: 565266 + url: https://raw.githubusercontent.com/commercialhaskell/stackage-snapshots/master/lts/17/5.yaml + sha256: 78e8ebabf11406261abbc95b44f240acf71802630b368888f6d758de7fc3a2f7 + original: lts-17.5 diff --git a/test/Spec.hs b/test/Spec.hs index 87a0fb9..4cb9a91 100644 --- a/test/Spec.hs +++ b/test/Spec.hs @@ -23,16 +23,18 @@ instance Arbitrary T.Text where -- This should evaluate to `y y`. dfi :: Expression dfi = Application d (Application f i) - where d = Abstraction "x" $ Application (Variable "x") (Variable "x") - f = Abstraction "f" $ Application (Variable "f") (Application (Variable "f") (Variable "y")) - i = Abstraction "x" $ Variable "x" + where + d = Abstraction "x" $ Application (Variable "x") (Variable "x") + f = Abstraction "f" $ Application (Variable "f") (Application (Variable "f") (Variable "y")) + i = Abstraction "x" $ Variable "x" -- This should evalaute to `y`. ttttt :: Expression ttttt = Application (Application (Application f t) (Abstraction "x" (Variable "x"))) (Variable "y") - where t = Abstraction "f" $ Abstraction "x" $ + where + t = Abstraction "f" $ Abstraction "x" $ Application (Variable "f") (Application (Variable "f") (Variable "x")) - f = Abstraction "T" $ Abstraction "f" $ Abstraction "x" $ + f = Abstraction "T" $ Abstraction "f" $ Abstraction "x" $ Application (Application (Application (Variable "T") (Application (Variable "T")