Make the printer smarter, separate intermediate AST data type.

* The expression printer now knows how to use `let`, multi-argument lambdas and applications, and block arguments when appropriate.
* There is a separate type, AbstractSyntax, which separates parsing/printing logic from removing/reintroducing the more advanced syntax described above.
* Expression is now its own module because its 'show' depends on AbstractSyntax,
  and I don't want the ast2expr/expr2ast stuff to be in the same module as the real lambda calculus stuff.
master
James T. Martin 2020-11-03 13:29:59 -08:00
parent 05d5abec6d
commit 79e054700b
Signed by: james
GPG Key ID: 4B7F3DA9351E577C
10 changed files with 289 additions and 166 deletions

View File

@ -9,12 +9,12 @@ Exit the prompt with `Ctrl-c` (or equivalent).
### Example session
```
>> 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
>> 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')))
λy' z. y y'
>> ^C
```

View File

@ -4,7 +4,7 @@ module Main where
import Control.Monad (forever)
import Data.Text
import qualified Data.Text.IO as TIO
import LambdaCalculus.Expression (eagerEval)
import LambdaCalculus (eagerEval)
import LambdaCalculus.Parser (parseExpression)
import System.IO (hFlush, stdout)

View File

@ -13,7 +13,9 @@ extra-source-files:
- README.md
default-extensions:
- ImportQualifiedPost
- OverloadedStrings
- ViewPatterns
dependencies:
- base >= 4.13 && < 5

136
src/LambdaCalculus.hs Normal file
View File

@ -0,0 +1,136 @@
module LambdaCalculus
( module LambdaCalculus.Expression
, eagerEval, lazyEval
) where
import Data.List (elemIndex, find)
import Data.Maybe (fromJust)
import Data.HashSet (HashSet)
import Data.HashSet qualified as HS
import Data.Text (Text)
import Data.Text qualified as T
import LambdaCalculus.Expression (Expression (..))
-- | Free variables are variables which are present in an expression but not bound by any abstraction.
freeVariables :: Expression -> HashSet Text
freeVariables (Variable variable) = HS.singleton variable
freeVariables (Application ef ex) = freeVariables ef `HS.union` freeVariables ex
freeVariables (Abstraction variable body) = HS.delete variable $ freeVariables body
-- | Return True if the given variable is free in the given expression.
freeIn :: Text -> Expression -> Bool
freeIn var1 (Variable var2) = var1 == var2
freeIn var (Application ef ex) = var `freeIn` ef && var `freeIn` ex
freeIn var1 (Abstraction var2 body) = var1 == var2 || var1 `freeIn` body
-- | Bound variables are variables which are bound by any abstraction in an expression.
boundVariables :: Expression -> HashSet Text
boundVariables (Variable _) = HS.empty
boundVariables (Application ef ex) = boundVariables ef `HS.union` boundVariables ex
boundVariables (Abstraction variable body) = HS.insert variable $ boundVariables body
-- | A closed expression is an expression with no free variables.
-- Closed expressions are also known as combinators and are equivalent to terms in combinatory logic.
closed :: Expression -> Bool
closed = HS.null . freeVariables
-- | Alpha-equivalent terms differ only by the names of bound variables,
-- 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
-- | 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
| 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
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
betaRedex (Application (Abstraction _ _) _) = True
betaRedex _ = False
-- | Returns True if the top-level expression is reducible by eta-reduction.
etaRedex :: Expression -> Bool
etaRedex (Abstraction var1 (Application ef (Variable var2)))
= var1 /= var2 || var1 `freeIn` ef
etaRedex _ = False
-- | In an expression in normal form, all reductions that can be applied have been applied.
-- This is the result of applying eager evaluation.
normal :: Expression -> Bool
-- The expression is beta-reducible.
normal (Application (Abstraction _ _) _) = False
-- The expression is eta-reducible.
normal (Abstraction var1 (Application fe (Variable var2)))
= var1 /= var2 || var1 `freeIn` fe
normal (Application ef ex) = normal ef && normal ex
normal _ = True
-- | In an expression in weak head normal form, reductions to the function have been applied,
-- but not all reductions to the parameter have been applied.
-- This is the result of applying lazy evaluation.
whnf :: Expression -> Bool
whnf (Application (Abstraction _ _) _) = False
whnf (Abstraction var1 (Application fe (Variable var2)))
= var1 /= var2 || var1 `freeIn` fe
whnf (Application ef _) = whnf ef
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
-- | Reduce an expression to normal form.
eagerEval :: Expression -> Expression
eagerEval = eval eagerEval
-- | Reduce an expression to weak head normal form.
lazyEval :: Expression -> Expression
lazyEval = eval id

View File

@ -1,149 +1,73 @@
{-# LANGUAGE DeriveGeneric #-}
module LambdaCalculus.Expression where
import Data.List (elemIndex, find)
import Data.Maybe (fromJust)
import Data.HashSet (HashSet)
import qualified Data.HashSet as HS
-- The definition of Expression is in its own file because:
-- * Expression and AbstractSyntax should not be in the same file
-- * Expression's `show` definition depends on AbstractSyntax's show definition,
-- which means that `ast2expr` and `expr2ast` can't be in AbstractSyntax
-- because of mutually recursive modules
-- * 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.Text (Text)
import qualified Data.Text as T
import Data.Text qualified as T
import GHC.Generics (Generic)
import LambdaCalculus.Parser.AbstractSyntax (AbstractSyntax)
import LambdaCalculus.Parser.AbstractSyntax qualified as AST
import TextShow
data Expression
= Variable Text
| Application Expression Expression
| Abstraction Text Expression
deriving (Eq, Generic)
= Variable Text
| Application Expression Expression
| 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.
basicShow :: Expression -> Builder
basicShow (Variable var) = fromText var
basicShow (Application ef ex) = "(" <> showb ef <> " " <> showb ex <> ")"
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.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
-- | View nested applications of abstractions as a list.
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.
viewAbstraction :: Expression -> ([Text], Expression)
viewAbstraction (Abstraction name body) = first (name :) (viewAbstraction body)
viewAbstraction x = ([], x)
-- | View left-nested applications as a list.
viewApplication :: Expression -> [Expression]
viewApplication (Application ef ex) = ex : viewApplication ef
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 (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 (Variable name) = AST.Variable name
instance TextShow Expression where
showb (Variable var) = fromText var
showb (Application ef ex) = "(" <> showb ef <> " " <> showb ex <> ")"
showb (Abstraction var body) = "" <> fromText var <> ". " <> showb body <> ")"
showb = showb . expr2ast
instance Show Expression where
show = T.unpack . showt
-- | Free variables are variables which are present in an expression but not bound by any abstraction.
freeVariables :: Expression -> HashSet Text
freeVariables (Variable variable) = HS.singleton variable
freeVariables (Application ef ex) = freeVariables ef `HS.union` freeVariables ex
freeVariables (Abstraction variable body) = HS.delete variable $ freeVariables body
-- | Return True if the given variable is free in the given expression.
freeIn :: Text -> Expression -> Bool
freeIn var1 (Variable var2) = var1 == var2
freeIn var (Application ef ex) = var `freeIn` ef && var `freeIn` ex
freeIn var1 (Abstraction var2 body) = var1 == var2 || var1 `freeIn` body
-- | Bound variables are variables which are bound by any abstraction in an expression.
boundVariables :: Expression -> HashSet Text
boundVariables (Variable _) = HS.empty
boundVariables (Application ef ex) = boundVariables ef `HS.union` boundVariables ex
boundVariables (Abstraction variable body) = HS.insert variable $ boundVariables body
-- | A closed expression is an expression with no free variables.
-- Closed expressions are also known as combinators and are equivalent to terms in combinatory logic.
closed :: Expression -> Bool
closed = HS.null . freeVariables
-- | Alpha-equivalent terms differ only by the names of bound variables,
-- 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
-- | 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
| 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
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
betaRedex (Application (Abstraction _ _) _) = True
betaRedex _ = False
-- | Returns True if the top-level expression is reducible by eta-reduction.
etaRedex :: Expression -> Bool
etaRedex (Abstraction var1 (Application ef (Variable var2)))
= var1 /= var2 || var1 `freeIn` ef
etaRedex _ = False
-- | In an expression in normal form, all reductions that can be applied have been applied.
-- This is the result of applying eager evaluation.
normal :: Expression -> Bool
-- The expression is beta-reducible.
normal (Application (Abstraction _ _) _) = False
-- The expression is eta-reducible.
normal (Abstraction var1 (Application fe (Variable var2)))
= var1 /= var2 || var1 `freeIn` fe
normal (Application ef ex) = normal ef && normal ex
normal _ = True
-- | In an expression in weak head normal form, reductions to the function have been applied,
-- but not all reductions to the parameter have been applied.
-- This is the result of applying lazy evaluation.
whnf :: Expression -> Bool
whnf (Application (Abstraction _ _) _) = False
whnf (Abstraction var1 (Application fe (Variable var2)))
= var1 /= var2 || var1 `freeIn` fe
whnf (Application ef _) = whnf ef
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
-- | Reduce an expression to normal form.
eagerEval :: Expression -> Expression
eagerEval = eval eagerEval
-- | Reduce an expression to weak head normal form.
lazyEval :: Expression -> Expression
lazyEval = eval id

View File

@ -1,12 +1,17 @@
module LambdaCalculus.Parser (parseExpression) where
module LambdaCalculus.Parser
( parseAST, parseExpression
) where
import Control.Applicative ((*>))
import Control.Monad (void)
import Data.Text (Text)
import qualified Data.Text as T
import LambdaCalculus.Expression
import LambdaCalculus.Expression (Expression, ast2expr)
import qualified LambdaCalculus.Expression as Expr
import LambdaCalculus.Parser.AbstractSyntax
import Text.Parsec hiding (spaces)
import Text.Parsec.Text
import TextShow
keywords :: [Text]
keywords = ["let", "in"]
@ -18,51 +23,50 @@ keyword kwd = do
notFollowedBy letter
-- | An identifier is a sequence of letters which is not a keyword.
identifier :: Parser Text
identifier :: Parser Identifier
identifier = do
notFollowedBy anyKeyword
T.pack <$> many1 letter
where anyKeyword = choice $ map (try . keyword) keywords
variable :: Parser Expression
variable :: Parser AbstractSyntax
variable = Variable <$> identifier
spaces :: Parser ()
spaces = skipMany1 space
application :: Parser Expression
application = foldl1 Application <$> sepEndBy1 applicationTerm spaces
where applicationTerm :: Parser Expression
application :: Parser AbstractSyntax
application = Application <$> sepEndBy1 applicationTerm spaces
where applicationTerm :: Parser AbstractSyntax
applicationTerm = abstraction <|> grouping <|> let_ <|> variable
where grouping :: Parser Expression
where grouping :: Parser AbstractSyntax
grouping = between (char '(') (char ')') expression
abstraction :: Parser Expression
abstraction :: Parser AbstractSyntax
abstraction = do
char '\\' <|> char 'λ' ; optional spaces
names <- sepEndBy1 identifier spaces
char '.'
body <- expression
pure $ foldr Abstraction body names
Abstraction names <$> expression
let_ :: Parser Expression
let_ :: Parser AbstractSyntax
let_ = do
try (keyword "let") ; spaces
defs <- sepBy1 definition (char ';' *> optional spaces)
keyword "in"
body <- expression
pure $ foldr (uncurry letExpr) body defs
where definition :: Parser (Text, Expression)
Let defs <$> expression
where definition :: Parser Definition
definition = do
name <- identifier ; optional spaces
char '='
value <- expression
pure (name, value)
letExpr :: Text -> Expression -> Expression -> Expression
letExpr name value body = Application (Abstraction name body) value
expression :: Parser Expression
expression :: Parser AbstractSyntax
expression = optional spaces *> (abstraction <|> let_ <|> application <|> variable) <* optional spaces
parseAST :: Text -> Either ParseError AbstractSyntax
parseAST = parse (expression <* eof) "input"
parseExpression :: Text -> Either ParseError Expression
parseExpression = parse (expression <* eof) "input"
parseExpression = fmap ast2expr . parseAST

View File

@ -0,0 +1,55 @@
module LambdaCalculus.Parser.AbstractSyntax
( AbstractSyntax (..), Definition, Identifier
) where
import Data.Bifunctor (first)
import Data.Text (Text)
import Data.Text qualified as T
import TextShow
-- | The abstract syntax tree reflects the structure of the externally-visible syntax.
--
-- This contains a lot of syntactic sugar when compared with 'LambdaCalculus.Expression'.
-- If this syntactic sugar were used in Expression, then operations like evaluation
-- 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
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)
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
-- | 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 <> ")"
instance Show AbstractSyntax where
show = T.unpack . showt

View File

@ -1,3 +1,5 @@
resolver: lts-16.20
# 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
packages:
- .

View File

@ -6,7 +6,7 @@
packages: []
snapshots:
- completed:
size: 532177
url: https://raw.githubusercontent.com/commercialhaskell/stackage-snapshots/master/lts/16/20.yaml
sha256: 0e14ba5603f01e8496e8984fd84b545a012ca723f51a098c6c9d3694e404dc6d
original: lts-16.20
size: 544004
url: https://raw.githubusercontent.com/commercialhaskell/stackage-snapshots/master/nightly/2020/11/3.yaml
sha256: f6988e9a2c92219dc8ff0ebd2d420ede3425fa08cb6613ba47f1bc97c9925aa8
original: nightly-2020-11-03

View File

@ -1,7 +1,7 @@
import Data.Char (isAlpha)
import qualified Data.Text as T
import Generic.Random (genericArbitraryRec, uniform)
import LambdaCalculus.Expression
import LambdaCalculus
import LambdaCalculus.Parser
import Test.QuickCheck
import Test.Tasty