diff --git a/package.yaml b/package.yaml index 491f36d..16a0e84 100644 --- a/package.yaml +++ b/package.yaml @@ -45,15 +45,13 @@ library: # 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: main: Main.hs source-dirs: app ghc-options: + - -Wall - -threaded - -rtsopts - -with-rtsopts=-N @@ -65,13 +63,11 @@ tests: main: Spec.hs source-dirs: test ghc-options: + - -Wall - -threaded - -rtsopts - -with-rtsopts=-N dependencies: - jtm-lambda-calculus - - generic-random >= 1.2 && < 2 - - 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 fb630ad..4f01dae 100644 --- a/src/LambdaCalculus.hs +++ b/src/LambdaCalculus.hs @@ -3,8 +3,8 @@ module LambdaCalculus , eval ) where -import Control.Monad.State (State, evalState, modify', state, put, get) -import Data.List (elemIndex, find) +import Control.Monad.State (State, evalState, modify', state, put, gets) +import Data.List (find) import Data.Maybe (fromJust) import Data.HashSet (HashSet) import Data.HashSet qualified as HS @@ -17,46 +17,6 @@ import LambdaCalculus.Expression (Expression (..), foldExpr) freeVariables :: Expression -> HashSet Text freeVariables = foldExpr HS.singleton HS.union HS.delete --- | Bound variables are variables which are bound by any abstraction in an expression. -boundVariables :: Expression -> HashSet Text -boundVariables = foldExpr (const HS.empty) HS.union HS.insert - --- | Return True if the given variable is free in the given expression. -freeIn :: Text -> Expression -> Bool -freeIn var = foldExpr (== var) (&&) (\name body -> (name == var) || 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 - alphaEquivalent' ctx1 ctx2 (Continuation v1 b1) (Continuation v2 b2) - = 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 - -- FIXME quickHack :: Expression -> Expression quickHack (Continuation name body) = Abstraction name body @@ -93,38 +53,6 @@ substitute var1 value unmodified@(quickHack -> Abstraction var2 body) free = (`HS.member` env) substitute _ _ _ = error "impossible" --- | Returns True if the top-level expression is reducible by beta-reduction. -betaRedex :: Expression -> Bool -betaRedex (Application (quickHack -> (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 (quickHack -> (Abstraction _ _)) _) = False --- The expression is eta-reducible. -normal (quickHack -> (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 (quickHack -> (Abstraction _ _)) _) = False -whnf (quickHack -> (Abstraction var1 (Application fe (Variable var2)))) - = var1 /= var2 || var1 `freeIn` fe -whnf (Application ef _) = whnf ef -whnf _ = True - type EvaluatorM a = State Continuation a type Evaluator = Expression -> EvaluatorM Expression @@ -167,7 +95,7 @@ evaluator unmodified@(Application ef ex) -- capture the current continuation if requested... Variable "callcc" -> do -- Don't worry about variable capture here for now. - k <- continue (Variable "!") <$> get + k <- gets $ continue (Variable "!") evaluator (Application ex (Continuation "!" k)) -- otherwise the value is irreducible and we can continue evaluation. _ -> ret unmodified diff --git a/src/LambdaCalculus/Expression.hs b/src/LambdaCalculus/Expression.hs index d2fc94d..9a68318 100644 --- a/src/LambdaCalculus/Expression.hs +++ b/src/LambdaCalculus/Expression.hs @@ -1,4 +1,3 @@ -{-# LANGUAGE DeriveGeneric #-} module LambdaCalculus.Expression ( Expression (..), foldExpr , ast2expr, expr2ast @@ -19,7 +18,6 @@ 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 (Builder, fromText, TextShow, showb, showt) @@ -36,7 +34,7 @@ data Expression -- -- Continuations do not have any corresponding surface-level syntax. | Continuation Text Expression - deriving (Eq, Generic) + deriving Eq foldExpr :: (Text -> a) -> (a -> a -> a) -> (Text -> a -> a) -> Expression -> a foldExpr varf appf absf = foldExpr' @@ -85,7 +83,7 @@ viewAbstraction x = ([], x) -- | View left-nested applications as a list. pattern Applications :: [Expression] -> Expression -pattern Applications exprs <- (viewApplication -> (exprs@(_:_:_))) +pattern Applications exprs <- (viewApplication -> exprs@(_:_:_)) {-# COMPLETE Abstractions, Applications, Continuation, Variable :: Expression #-} diff --git a/test/Spec.hs b/test/Spec.hs index e11635e..ba5638e 100644 --- a/test/Spec.hs +++ b/test/Spec.hs @@ -1,19 +1,7 @@ -import Data.Char (isAlpha) -import qualified Data.Text as T -import Generic.Random (genericArbitraryRec, uniform) import LambdaCalculus import LambdaCalculus.Parser -import Test.QuickCheck import Test.Tasty import Test.Tasty.HUnit -import Test.Tasty.QuickCheck -import TextShow (showt) - -instance Arbitrary Expression where - arbitrary = genericArbitraryRec uniform - -instance Arbitrary T.Text where - arbitrary = T.pack <$> listOf1 (elements $ ['A'..'Z'] ++ ['a'..'z']) -- These are terms which have complex reduction steps and -- are likely to catch bugs in the substitution function, if there are any.