diff --git a/README.md b/README.md index 35525f4..5cb5f17 100644 --- a/README.md +++ b/README.md @@ -44,8 +44,6 @@ This interpreter has preliminary support for However, it has not been thoroughly tested. To use it, simply apply the variable `callcc` like you would a function, e.g. `(callcc (\k. ...))`. -`callcc` is not a normal variable and cannot be shadowed; -`\callcc. callcc` is *not* the identity function, it *ignores* its argument and then returns the *operator* `callcc`. Continuations are printed as `λ!. ... ! ...`, like a lambda abstraction with an argument named `!` which is used exactly once; diff --git a/package.yaml b/package.yaml index 60a2efd..15b1ed4 100644 --- a/package.yaml +++ b/package.yaml @@ -56,8 +56,6 @@ library: # Less stupid warnings, but I still don't care - -Wno-all-missed-specialisations - -Wno-missing-local-signatures - # This is a good warning, but often polymorphism isn't actually needed. - - -Wno-monomorphism-restriction # 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/LambdaCalculus/Evaluator.hs b/src/LambdaCalculus/Evaluator.hs index e56edca..954347c 100644 --- a/src/LambdaCalculus/Evaluator.hs +++ b/src/LambdaCalculus/Evaluator.hs @@ -1,8 +1,8 @@ module LambdaCalculus.Evaluator ( Expr (..), ExprF (..), VoidF, Text , Eval, EvalExpr, EvalX, EvalXF (..) - , pattern AppFE, pattern Cont, pattern ContF - , eval, traceEval + , pattern AppFE, pattern Cont, pattern ContF, pattern CallCC, pattern CallCCF + , eval, traceEval, substitute, alphaConvert ) where import LambdaCalculus.Evaluator.Base @@ -21,18 +21,17 @@ import Data.Void (Void, absurd) -- | Free variables are variables which are present in an expression but not bound by any abstraction. freeVars :: EvalExpr -> HashSet Text freeVars = cata \case - VarF name -> HS.singleton name - AppFE e1 e2 -> HS.union e1 e2 - AbsF n e -> HS.delete n e - ContF e -> HS.delete "!" e + AbsF n e -> HS.delete n e + ContF e -> HS.delete "!" e + VarF n -> HS.singleton n + e -> foldr HS.union HS.empty e -- | Bound variables are variables which are bound by any form of abstraction in an expression. boundVars :: EvalExpr -> HashSet Text boundVars = cata \case - VarF _ -> HS.empty - AppFE e1 e2 -> HS.union e1 e2 - AbsF n e -> HS.insert n e - ContF e -> HS.insert "!" e + AbsF n e -> HS.insert n e + ContF e -> HS.insert "!" e + e -> foldr HS.union HS.empty e -- | Vars that occur anywhere in an experession, bound or free. usedVars :: EvalExpr -> HashSet Text @@ -88,16 +87,17 @@ unsafeSubstitute var val = para \case | ContF _ <- e', var == "!" -> unmodified e' | otherwise -> substituted e' where + substituted, unmodified :: EvalExprF (EvalExpr, EvalExpr) -> EvalExpr substituted = embed . fmap snd unmodified = embed . fmap fst isReducible :: EvalExpr -> Bool isReducible = snd . cata \case - AppF ctr (Identity args) -> eliminator ctr [args] - VarF "callcc" -> constructor - AbsF _ _ -> constructor - ContF _ -> constructor - VarF _ -> constant + AppFE ctr args -> eliminator ctr [args] + CallCCF -> constructor + AbsF _ _ -> constructor + ContF _ -> constructor + VarF _ -> constant where -- | Constants are irreducible in any context. constant = (False, False) @@ -150,8 +150,7 @@ evaluatorStep = \case put [] pure $ substitute "!" ex body -- capture the current continuation if requested... - Var "callcc" -> do - -- Don't worry about variable capture here for now. + CallCC -> do k <- gets $ continue (Var "!") pure $ App ex (Cont k) -- otherwise the value is irreducible and we can continue evaluation. diff --git a/src/LambdaCalculus/Evaluator/Base.hs b/src/LambdaCalculus/Evaluator/Base.hs index c9a22f4..418d722 100644 --- a/src/LambdaCalculus/Evaluator/Base.hs +++ b/src/LambdaCalculus/Evaluator/Base.hs @@ -2,7 +2,7 @@ module LambdaCalculus.Evaluator.Base ( Identity (..) , Expr (..), ExprF (..), VoidF, Text , Eval, EvalExpr, EvalExprF, EvalX, EvalXF (..) - , pattern AppFE, pattern Cont, pattern ContF + , pattern AppFE, pattern Cont, pattern ContF, pattern CallCC, pattern CallCCF ) where import LambdaCalculus.Expression.Base @@ -23,14 +23,16 @@ type instance AppArgsF Eval = Identity type instance LetArgsF Eval = VoidF type instance XExprF Eval = EvalXF -newtype EvalXF r +data EvalXF r -- | A continuation. This is identical to a lambda abstraction, -- with the exception that it performs the side-effect of -- deleting the current continuation. -- -- Continuations do not have any corresponding surface-level syntax, -- but may be printed like a lambda with the illegal variable `!`. - = Cont_ r + = Cont_ !r + -- | Call-with-current-continuation, an evaluator built-in function. + | CallCC_ deriving (Eq, Functor, Foldable, Traversable, Show) instance RecursivePhase Eval where @@ -40,13 +42,19 @@ instance RecursivePhase Eval where pattern Cont :: EvalExpr -> EvalExpr pattern Cont e = ExprX (Cont_ e) +pattern CallCC :: EvalExpr +pattern CallCC = ExprX CallCC_ + pattern ContF :: r -> EvalExprF r pattern ContF e = ExprXF (Cont_ e) +pattern CallCCF :: EvalExprF r +pattern CallCCF = ExprXF CallCC_ + pattern AppFE :: r -> r -> EvalExprF r pattern AppFE ef ex = AppF ef (Identity ex) -{-# COMPLETE Var, App, Abs, Let, Cont #-} -{-# COMPLETE VarF, AppF, AbsF, LetF, ContF #-} -{-# COMPLETE VarF, AppFE, AbsF, LetF, ExprXF #-} -{-# COMPLETE VarF, AppFE, AbsF, LetF, ContF #-} +{-# COMPLETE Var, App, Abs, Let, Cont, CallCC #-} +{-# COMPLETE VarF, AppF, AbsF, LetF, ContF, CallCCF #-} +{-# COMPLETE VarF, AppFE, AbsF, LetF, ExprXF #-} +{-# COMPLETE VarF, AppFE, AbsF, LetF, ContF, CallCCF #-} diff --git a/src/LambdaCalculus/Expression.hs b/src/LambdaCalculus/Expression.hs index 88629c9..6de24af 100644 --- a/src/LambdaCalculus/Expression.hs +++ b/src/LambdaCalculus/Expression.hs @@ -1,22 +1,24 @@ module LambdaCalculus.Expression ( Expr (..), ExprF (..), DefF (..), VoidF, Text , Eval, EvalExpr, EvalX, EvalXF (..), Identity (..) - , pattern AppFE, pattern Cont, pattern ContF + , pattern AppFE, pattern Cont, pattern ContF, pattern CallCC, pattern CallCCF , Parse, AST, ASTF, NonEmptyDefFs (..), NonEmpty (..), simplify , pattern LetFP , ast2eval, eval2ast ) where import LambdaCalculus.Evaluator.Base +import LambdaCalculus.Evaluator import LambdaCalculus.Syntax.Base import Data.Functor.Foldable (cata, hoist) +import Data.HashSet qualified as HS import Data.List (foldl') import Data.List.NonEmpty (toList) -- | Convert from an abstract syntax tree to an evaluator expression. ast2eval :: AST -> EvalExpr -ast2eval = cata \case +ast2eval = substitute "callcc" CallCC . cata \case VarF name -> Var name AppF ef exs -> foldl' App ef $ toList exs AbsF ns e -> foldr Abs e $ toList ns @@ -26,8 +28,16 @@ ast2eval = cata \case -- | Convert from an evaluator expression to an abstract syntax tree. eval2ast :: EvalExpr -> AST -eval2ast = hoist \case - VarF name -> VarF name - AppFE ef ex -> AppF ef (ex :| []) - AbsF n e -> AbsF (n :| []) e - ContF e -> AbsF ("!" :| []) e +-- Because all `ast2eval` replaces all free instances of `callcc`, +-- all instances of `callcc` must be bound; +-- therefore, we are free to alpha convert them, +-- freeing the name `callcc` for us to use for the built-in again. +eval2ast = hoist go . alphaConvert (HS.singleton "callcc") + where + go :: EvalExprF r -> ASTF r + go = \case + VarF name -> VarF name + CallCCF -> VarF "callcc" + AppFE ef ex -> AppF ef (ex :| []) + AbsF n e -> AbsF (n :| []) e + ContF e -> AbsF ("!" :| []) e diff --git a/test/Spec.hs b/test/Spec.hs index 59ae7be..444409f 100644 --- a/test/Spec.hs +++ b/test/Spec.hs @@ -39,10 +39,10 @@ omega = App x x where x = Abs "x" (App (Var "x") (Var "x")) cc1 :: EvalExpr -cc1 = App (Var "callcc") (Abs "k" (App omega (App (Var "k") (Var "z")))) +cc1 = App CallCC (Abs "k" (App omega (App (Var "k") (Var "z")))) cc2 :: EvalExpr -cc2 = App (Var "y") (App (Var "callcc") (Abs "k" (App (Var "z") (App (Var "k") (Var "x"))))) +cc2 = App (Var "y") (App CallCC (Abs "k" (App (Var "z") (App (Var "k") (Var "x"))))) main :: IO () main = defaultMain $