Cleanup: fix warnings, fix indentation, upgrade dependencies.

master
James T. Martin 2021-03-05 19:04:06 -08:00
parent 59a55acdc6
commit f73e78fcdb
Signed by: james
GPG Key ID: 4B7F3DA9351E577C
11 changed files with 195 additions and 140 deletions

View File

@ -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

View File

@ -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

View File

@ -1,4 +1,3 @@
{-# LANGUAGE LambdaCase #-}
module Main where
import Control.Monad (forever)

View File

@ -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

View File

@ -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

View File

@ -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

View File

@ -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

View File

@ -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

View File

@ -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:
- .

View File

@ -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

View File

@ -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")