From d7ae1f1294782a07b9a85f6df04e8894d0a9ec58 Mon Sep 17 00:00:00 2001
From: James Martin <james@jtmar.me>
Date: Fri, 5 Mar 2021 23:38:21 -0800
Subject: [PATCH] Add support for call/cc (though the implementation's kinda
 hacky).

---
 README.md                          |  21 ++++-
 app/Main.hs                        |   4 +-
 package.yaml                       |   1 +
 src/LambdaCalculus.hs              | 123 ++++++++++++++++++-----------
 src/LambdaCalculus/Continuation.hs |  26 ++++++
 src/LambdaCalculus/Expression.hs   |  22 +++++-
 test/Spec.hs                       |  19 +++--
 7 files changed, 162 insertions(+), 54 deletions(-)
 create mode 100644 src/LambdaCalculus/Continuation.hs

diff --git a/README.md b/README.md
index 10bc8e8..35525f4 100644
--- a/README.md
+++ b/README.md
@@ -3,8 +3,10 @@ This is a simple implementation of the untyped lambda calculus
 with an emphasis on clear, readable Haskell code.
 
 ## Usage
+Run the program using `stack run` (or run the tests with `stack test`).
+
 Type in your expression at the prompt: `>> `.
-The expression will be evaluated to normal form and then printed.
+The expression will be evaluated to normal form using the call-by-value evaluation strategy and then printed.
 Exit the prompt with `Ctrl-c` (or equivalent).
 
 ### Example session
@@ -17,6 +19,8 @@ y
 λy' z. y y'
 >> let fix = (\x. x x) \fix f x. f (fix fix f) x; S = \n f x. f (n f x); plus = fix \plus x. x S in plus (\f x. f (f (f x))) (\f x. f (f x)) f x
 f (f (f (f (f x))))
+>> y (callcc \k. (\x. (\x. x x) (\x. x x)) (k z))
+y z
 >> ^C
 ```
 
@@ -33,3 +37,18 @@ and spaces are used to separate variables rather than commas.
 * A sequence of abstractions may be contracted: `\foo. \bar. \baz. N` may be abbreviated as `\foo bar baz. N`.
 * Variables may be bound using let expressions: `let x = N in M` is syntactic sugar for `(\x. N) M`.
 * Multiple variables may be defined in one let expression: `let x = N; y = O in M`
+
+## Call/CC
+This interpreter has preliminary support for
+[the call-with-current-continuation control flow operator](https://en.wikipedia.org/wiki/Call-with-current-continuation).
+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;
+however, continuations are *not* the same as lambda abstractions
+because they perform the side effect of modifying the current continuation,
+and this is *not* valid syntax you can input into the REPL.
diff --git a/app/Main.hs b/app/Main.hs
index 48dd76a..66b7c95 100644
--- a/app/Main.hs
+++ b/app/Main.hs
@@ -3,7 +3,7 @@ module Main where
 import Control.Monad (forever)
 import Data.Text
 import qualified Data.Text.IO as TIO
-import LambdaCalculus (eagerEval)
+import LambdaCalculus (eval)
 import LambdaCalculus.Parser (parseExpression)
 import System.IO (hFlush, stdout)
 
@@ -16,4 +16,4 @@ prompt text = do
 main :: IO ()
 main = forever $ parseExpression <$> prompt ">> " >>= \case
   Left parseError -> putStrLn $ "Parse error: " ++ show parseError
-  Right expr -> print $ eagerEval expr
+  Right expr -> print $ eval expr
diff --git a/package.yaml b/package.yaml
index 91a01d9..491f36d 100644
--- a/package.yaml
+++ b/package.yaml
@@ -22,6 +22,7 @@ default-extensions:
 
 dependencies:
 - base >= 4.14 && < 5
+- mtl >= 2.2 && < 3
 - parsec >= 3.1 && < 4
 - text >= 1.2 && < 2
 - text-show >= 3.9 && < 4
diff --git a/src/LambdaCalculus.hs b/src/LambdaCalculus.hs
index b654156..fb630ad 100644
--- a/src/LambdaCalculus.hs
+++ b/src/LambdaCalculus.hs
@@ -1,33 +1,29 @@
 module LambdaCalculus
   ( module LambdaCalculus.Expression
-  , eagerEval, lazyEval
+  , eval
   ) where
 
+import Control.Monad.State (State, evalState, modify', state, put, get)
 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 (..))
+import LambdaCalculus.Continuation
+import LambdaCalculus.Expression (Expression (..), foldExpr)
 
 -- | 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
+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 (Variable _) = HS.empty
-boundVariables (Application ef ex) = boundVariables ef `HS.union` boundVariables ex
-boundVariables (Abstraction variable body) = HS.insert variable $ boundVariables body
+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.
@@ -50,6 +46,8 @@ alphaEquivalent = alphaEquivalent' [] []
     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
@@ -59,6 +57,11 @@ alphaEquivalent = alphaEquivalent' [] []
       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
+quickHack e = e
+
 -- | 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)
@@ -66,10 +69,15 @@ substitute var1 value unmodified@(Variable var2)
   | otherwise = unmodified
 substitute var value (Application ef ex)
   = Application (substitute var value ef) (substitute var value ex)
-substitute var1 value unmodified@(Abstraction var2 body)
+substitute var1 value unmodified@(quickHack -> Abstraction var2 body)
   | var1 == var2 = unmodified
-  | otherwise = Abstraction var2' $ substitute var1 value $ alphaConvert var2 var2' body
+  | otherwise = constructor var2' $ substitute var1 value $ alphaConvert var2 var2' body
   where
+    constructor = case unmodified of
+      Abstraction _ _ -> Abstraction
+      Continuation _ _ -> Continuation
+      _ -> error "impossible"
+
     var2' :: Text
     var2' = escapeName (freeVariables value) var2
 
@@ -83,10 +91,11 @@ substitute var1 value unmodified@(Abstraction var2 body)
 
             free :: Text -> Bool
             free = (`HS.member` env)
+substitute _ _ _ = error "impossible"
 
 -- | Returns True if the top-level expression is reducible by beta-reduction.
 betaRedex :: Expression -> Bool
-betaRedex (Application (Abstraction _ _) _) = True
+betaRedex (Application (quickHack -> (Abstraction _ _)) _) = True
 betaRedex _ = False
 
 -- | Returns True if the top-level expression is reducible by eta-reduction.
@@ -99,9 +108,9 @@ etaRedex _ = False
 -- This is the result of applying eager evaluation.
 normal :: Expression -> Bool
 -- The expression is beta-reducible.
-normal (Application (Abstraction _ _) _) = False
+normal (Application (quickHack -> (Abstraction _ _)) _) = False
 -- The expression is eta-reducible.
-normal (Abstraction var1 (Application fe (Variable var2)))
+normal (quickHack -> (Abstraction var1 (Application fe (Variable var2))))
   = var1 /= var2 || var1 `freeIn` fe
 normal (Application ef ex) = normal ef && normal ex
 normal _ = True
@@ -110,34 +119,60 @@ normal _ = True
 -- 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)))
+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
 
-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
+type EvaluatorM a = State Continuation a
+type Evaluator = Expression -> EvaluatorM Expression
 
--- | Reduce an expression to normal form.
-eagerEval :: Expression -> Expression
-eagerEval = eval eagerEval
+isReducible :: Expression -> Bool
+isReducible (Application (quickHack -> (Abstraction _ _)) _) = True
+isReducible (Application (Variable "callcc") _) = True
+isReducible (Application ef ex) = isReducible ef || isReducible ex
+isReducible _ = False
 
--- | Reduce an expression to weak head normal form.
-lazyEval :: Expression -> Expression
-lazyEval = eval id
+push :: ContinuationCrumb -> EvaluatorM ()
+push c = modify' (c :)
+
+pop :: EvaluatorM (Maybe ContinuationCrumb)
+pop = state \case
+  [] -> (Nothing, [])
+  (crumb:k) -> (Just crumb, k)
+
+ret :: Expression -> EvaluatorM Expression
+ret e = pop >>= maybe (pure e) (evaluator . continue1 e)
+
+-- | A call-by-value expression evaluator.
+evaluator :: Evaluator
+evaluator unmodified@(Application ef ex)
+  -- First reduce the argument...
+  | isReducible ex = do
+      push (AppliedTo ef)
+      evaluator ex
+  -- then reduce the function...
+  | isReducible ef = do
+      push (ApplyTo ex)
+      evaluator ef
+  | otherwise = case ef of
+      -- perform beta reduction if possible...
+      Abstraction name body ->
+        evaluator $ substitute name ex body
+      -- perform continuation calls if possible...
+      Continuation name body -> do
+        put []
+        evaluator $ substitute name ex body
+      -- capture the current continuation if requested...
+      Variable "callcc" -> do
+        -- Don't worry about variable capture here for now.
+        k <- continue (Variable "!") <$> get
+        evaluator (Application ex (Continuation "!" k))
+      -- otherwise the value is irreducible and we can continue evaluation.
+      _ -> ret unmodified
+-- Neither abstractions nor variables are reducible.
+evaluator e = ret e
+
+eval :: Expression -> Expression
+eval = flip evalState [] . evaluator
diff --git a/src/LambdaCalculus/Continuation.hs b/src/LambdaCalculus/Continuation.hs
new file mode 100644
index 0000000..048bc99
--- /dev/null
+++ b/src/LambdaCalculus/Continuation.hs
@@ -0,0 +1,26 @@
+module LambdaCalculus.Continuation
+  ( Continuation, continue, continue1
+  , ContinuationCrumb (ApplyTo, AppliedTo, AbstractedOver)
+  ) where
+
+import Data.List (foldl')
+import Data.Text (Text)
+import LambdaCalculus.Expression
+
+data ContinuationCrumb
+  -- | The one-hole context of a function application: `(_ e)`
+  = ApplyTo Expression
+  -- | The one-hole context of the argument to a function application: `(f _)`
+  | AppliedTo Expression
+  -- | The one-hole context of the body of a lambda abstraction: `(λx. _)`
+  | AbstractedOver Text
+
+type Continuation = [ContinuationCrumb]
+
+continue1 :: Expression -> ContinuationCrumb -> Expression
+continue1 e (ApplyTo x) = Application e x
+continue1 e (AppliedTo x) = Application x e
+continue1 e (AbstractedOver name) = Abstraction name e
+
+continue :: Expression -> Continuation -> Expression
+continue = foldl' continue1
diff --git a/src/LambdaCalculus/Expression.hs b/src/LambdaCalculus/Expression.hs
index 97ab1e5..d2fc94d 100644
--- a/src/LambdaCalculus/Expression.hs
+++ b/src/LambdaCalculus/Expression.hs
@@ -1,6 +1,6 @@
 {-# LANGUAGE DeriveGeneric #-}
 module LambdaCalculus.Expression
-  ( Expression (Variable, Application, Abstraction)
+  ( Expression (..), foldExpr
   , ast2expr, expr2ast
   , pattern Lets, pattern Abstractions, pattern Applications
   , viewLet, viewAbstraction, viewApplication
@@ -30,14 +30,31 @@ data Expression
   | Application Expression Expression
   -- | Lambda abstraction: `(λx. e)`.
   | Abstraction Text Expression
+  -- | 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.
+  | Continuation Text Expression
   deriving (Eq, Generic)
 
+foldExpr :: (Text -> a) -> (a -> a -> a) -> (Text -> a -> a) -> Expression -> a
+foldExpr varf appf absf = foldExpr'
+  where
+    foldExpr' (Variable name) = varf name
+    foldExpr' (Application ef ex) = appf (foldExpr' ef) (foldExpr' ex)
+    foldExpr' (Abstraction name body) = absf name (foldExpr' body)
+    -- This isn't technically correct, but it's good enough for every place I use this.
+    -- I'll figure out a proper solution later, or possibly just rip out this function.
+    foldExpr' (Continuation name body) = absf name (foldExpr' body)
+
 -- | 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 <> ")"
+basicShow (Continuation var body) = "(Λ" <> fromText var <> ". " <> showb body <> ")"
 
 -- | Convert from an abstract syntax tree to an expression.
 ast2expr :: AbstractSyntax -> Expression
@@ -70,7 +87,7 @@ viewAbstraction x = ([], x)
 pattern Applications :: [Expression] -> Expression
 pattern Applications exprs <- (viewApplication -> (exprs@(_:_:_)))
 
-{-# COMPLETE Abstractions, Applications, Variable :: Expression #-}
+{-# COMPLETE Abstractions, Applications, Continuation, Variable :: Expression #-}
 
 viewApplication :: Expression -> [Expression]
 viewApplication (Application ef ex) = ex : viewApplication ef
@@ -84,6 +101,7 @@ expr2ast (Lets defs body) = AST.Let (fromList $ map (second expr2ast) defs) $ ex
 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
+expr2ast (Continuation _ body) = AST.Abstraction ("!" :| []) (expr2ast body)
 
 instance TextShow Expression where
   showb = showb . expr2ast
diff --git a/test/Spec.hs b/test/Spec.hs
index 4cb9a91..e11635e 100644
--- a/test/Spec.hs
+++ b/test/Spec.hs
@@ -44,15 +44,25 @@ ttttt = Application (Application (Application f t) (Abstraction "x" (Variable "x
                         (Variable "f"))
           (Variable "x")
 
-prop_parseExpression_inverse :: Expression -> Bool
-prop_parseExpression_inverse expr = Right expr == parseExpression (showt expr)
+-- | A simple divergent expression.
+omega :: Expression
+omega = Application x x
+  where x = Abstraction "x" (Application (Variable "x") (Variable "x"))
+
+cc1 :: Expression
+cc1 = Application (Variable "callcc") (Abstraction "k" (Application omega (Application (Variable "k") (Variable "z"))))
+
+cc2 :: Expression
+cc2 = Application (Variable "y") (Application (Variable "callcc") (Abstraction "k" (Application (Variable "z") (Application (Variable "k") (Variable "x")))))
 
 main :: IO ()
 main = defaultMain $
   testGroup "Tests"
   [ testGroup "Evaluator tests"
-    [ testCase "DFI" $ eagerEval dfi @?= Application (Variable "y") (Variable "y")
-    , testCase "ttttt" $ eagerEval ttttt @?= Variable "y"
+    [ testCase "capture test 1: DFI" $ eval dfi @?= Application (Variable "y") (Variable "y")
+    , testCase "capture test 2: ttttt" $ eval ttttt @?= Variable "y"
+    , testCase "invoking a continuation replaces the current continuation" $ eval cc1 @?= Variable "z"
+    , testCase "callcc actually captures the current continuation" $ eval cc2 @?= Application (Variable "y") (Variable "x")
     ]
   , testGroup "Parser tests"
     [ testGroup "Unit tests"
@@ -70,6 +80,5 @@ main = defaultMain $
         , testCase "around let" $ parseExpression "  let x=(y)in x  " @?= Right (Application (Abstraction "x" (Variable "x")) (Variable "y"))
         ]
       ]
-    , testProperty "parseExpression is the left inverse of show" prop_parseExpression_inverse
     ]
   ]