From 70b3b7e0512ed591461dd1088514adf74407548b Mon Sep 17 00:00:00 2001 From: James Martin Date: Thu, 15 Aug 2019 13:11:17 -0700 Subject: [PATCH] I fixed it! Also deleted some unused code, and refactored a little. --- README.md | 3 +- app/Main.hs | 5 +- src/UntypedLambdaCalculus.hs | 146 ++++++++++++++++------------ src/UntypedLambdaCalculus/Parser.hs | 20 +++- 4 files changed, 105 insertions(+), 69 deletions(-) diff --git a/README.md b/README.md index 9e4b45b..78be6f7 100644 --- a/README.md +++ b/README.md @@ -19,9 +19,10 @@ This is not guaranteed not to capture free variables. ``` >> (\D F I. D (F I)) (\x. x x) (\f. f (f y)) (\x. x) y y +>> (\T f x. T (T (T (T T))) f x) (\f x. f (f x)) (\x. x) y +y >> \x. \y. y x \x. \y. y:0 x:1 ->> ``` ## Syntax diff --git a/app/Main.hs b/app/Main.hs index 7fed360..b4a077f 100644 --- a/app/Main.hs +++ b/app/Main.hs @@ -12,12 +12,9 @@ prompt text = do hFlush stdout getLine --- (\D F I. D (F I)) (\x. x x) (\f. f (f y)) (\x. x) main :: IO () main = forever $ do expr <- parse expr "stdin" <$> prompt ">> " case expr of Left parseError -> putStrLn $ "Parse error: " ++ show parseError - Right expr -> do - print $ eval [] $ canonym expr - + Right expr -> print $ eval $ canonym expr diff --git a/src/UntypedLambdaCalculus.hs b/src/UntypedLambdaCalculus.hs index f9f070d..9adb32e 100644 --- a/src/UntypedLambdaCalculus.hs +++ b/src/UntypedLambdaCalculus.hs @@ -1,17 +1,20 @@ {-# LANGUAGE TemplateHaskell, TypeFamilies, DeriveFunctor, DeriveFoldable, DeriveTraversable #-} -module UntypedLambdaCalculus where +module UntypedLambdaCalculus (Expr (Free, Var, Lam, App), canonym, eval, normal, whnf) where import Control.Applicative (liftA2) import Control.Monad.Reader (Reader, runReader, ask, local, reader) import Data.Function (fix) -import Data.Functor.Foldable (Base, Recursive, cata, embed) +import Data.Functor.Foldable (Base, Recursive, cata, embed, project) import Data.Functor.Foldable.TH (makeBaseFunctor) -import Data.HashSet (HashSet, empty, singleton, union, member, delete) import Data.List (findIndex) import UntypedLambdaCalculus.Parser (Ast (AstVar, AstLam, AstApp), AstF (AstVarF, AstLamF, AstAppF)) +-- | Look up a recursion-schemes tutorial if you don't know what an Algebra means. +-- | I use recursion-schemes in this project a lot. type Algebra f a = f a -> a +-- | A lambda calculus expression where variables are identified +-- | by their distance from their binding site (De Bruijn indices). data Expr = Free String | Var Int | Lam String Expr @@ -19,7 +22,21 @@ data Expr = Free String makeBaseFunctor ''Expr +instance Show Expr where + show = cataReader alg [] + where alg :: Algebra ExprF (Reader [String] String) + alg (FreeF v) = return v + alg (VarF v) = reader (\vars -> vars !! v ++ ':' : show v) + alg (LamF v e) = do + body <- local (v :) e + return $ "(\\" ++ v ++ ". " ++ body ++ ")" + alg (AppF f' x') = do + f <- f' + x <- x' + return $ "(" ++ f ++ " " ++ x ++ ")" + -- | Recursively reduce a `t` into an `a` when inner reductions are dependent on outer context. +-- | In other words, data flows outside-in, reductions flow inside-out. cataReader :: Recursive t => Algebra (Base t) (Reader s a) -> s -> t -> a cataReader alg s x = runReader (cata alg x) s @@ -33,74 +50,81 @@ unbound = cataReader alg 0 alg (AppF f x) = (&&) <$> f <*> x alg (LamF _ e) = local (+ 1) e -eval :: [Expr] -> Expr -> Expr -eval env (Var v) = env !! v -eval env (App f' x') = case f of - Lam _ e -> eval (x : env) e - _ -> App f x - where f = eval env f' - x = eval env x' -eval env o@(Lam _ (App f (Var 0))) - | unbound f = eval (undefined : env) f - | otherwise = o -eval env x = runReader (substExpr x) env - -free :: Ast -> HashSet String -free = cata alg - where alg :: Algebra AstF (HashSet String) - alg (AstVarF x) = singleton x - alg (AstLamF x m) = delete x m - alg (AstAppF m n) = m `union` n - +-- | Convert an Ast into an Expression where all variables have canonical, unique names. +-- | Namely, bound variables are identified according to their distance from their binding site +-- | (i.e. De Bruijn indices). canonym :: Ast -> Expr canonym = cataReader alg [] where alg :: Algebra AstF (Reader [String] Expr) - alg (AstVarF v) = maybe (Free v) Var <$> findIndex (== v) <$> ask - alg (AstLamF v e') = Lam v <$> local (v :) e' - alg (AstAppF n m) = App <$> n <*> m + alg (AstVarF v) = maybe (Free v) Var <$> findIndex (== v) <$> ask + alg (AstLamF v e) = Lam v <$> local (v :) e + alg (AstAppF n m) = App <$> n <*> m -rename :: String -> HashSet String -> String -rename var free - -- Continue prepending `_` until the name is free. - | var `member` free = rename newVar free - | otherwise = var - where newVar = '_' : var -subst :: String -> Ast -> Ast -> Ast -subst var n o@(AstVar var') - | var == var' = n - | otherwise = o -subst var n (AstApp m1 m2) = AstApp (subst var n m1) (subst var n m2) -subst var n o@(AstLam var' m) - | var == var' = o - -- Alpha-convert as necessary, and then substitute into the body. - | otherwise = AstLam newVar $ subst var n $ subst var' (AstVar newVar) m - where newVar = rename var' $ free n -instance Show Expr where - show = cataReader alg [] - where alg :: Algebra ExprF (Reader [String] String) - alg (FreeF v) = return v - alg (VarF v) = reader (\vars -> vars !! v ++ show v) - alg (LamF v e) = do - body <- local (v :) e - return $ "(\\" ++ v ++ ". " ++ body ++ ")" - alg (AppF f' x') = do - f <- f' - x <- x' - return $ "(" ++ f ++ " " ++ x ++ ")" +-- | When we bind a new variable, we enter a new scope. +-- | Since variables are identified by their distance from their binder, +-- | we must increment them to account for the incremented distance. +{-introduceBindingInExpr :: Expr -> Expr +introduceBindingInExpr = cataReader alg 0 + where alg :: Algebra ExprF (Reader Int Expr) + alg (VarF v) = reader $ \x -> + if v > x then Var $ v + 1 else Var v + alg (LamF v e) = Lam v <$> local (+ 1) e + alg (AppF f x) = App <$> f <*> x + alg (FreeF v) = return $ Free v-} +introduceBindingInExpr :: Expr -> Expr +introduceBindingInExpr (Var v) = Var $ v + 1 +introduceBindingInExpr o@(Lam _ _) = o +introduceBindingInExpr x = embed $ fmap introduceBindingInExpr $ project x -type Eval' = Expr -> Reader [Expr] Expr +introduceBinding :: Expr -> Reader [Expr] a -> Reader [Expr] a +introduceBinding x = local (\exprs -> x : map introduceBindingInExpr exprs) -incrementVars :: Expr -> Expr -incrementVars = cata alg - where alg (VarF x) = Var $ x + 1 - alg x = embed x +intoBinding :: Reader [Expr] a -> Reader [Expr] a +intoBinding = introduceBinding (Var 0) -substExpr :: Eval' -substExpr = cata alg +intoEta :: Reader [Expr] a -> Reader [Expr] a +intoEta = introduceBinding undefined + +-- | Substitute all bound variables in an expression for their values, +-- | without performing any further evaluation. +subst :: Expr -> Reader [Expr] Expr +subst = cata alg where alg :: Algebra ExprF (Reader [Expr] Expr) alg (VarF v) = reader (!! v) alg (AppF f x) = App <$> f <*> x alg (FreeF x) = return $ Free x - alg (LamF v e) = Lam v <$> local (\exprs -> Var 0 : map incrementVars exprs) e + -- In a lambda expression, we substitute the parameter with itself. + -- The rest of the substitutions may reference variables outside this binding, + -- so that (Var 0) would refer not to this lambda, but the lambda outside it. + -- Thus, we must increment all variables in the expression to be substituted in. + alg (LamF v e) = Lam v <$> intoBinding e + +-- | Evaluate a variable to normal form. +eval :: Expr -> Expr +eval expr = runReader (eval' expr) [] + where eval' (App f' x') = do + f <- eval' f' + x <- eval' x' + case f of + Lam _ e -> introduceBinding x $ eval' e + _ -> return $ App f x + eval' o@(Lam _ (App f (Var 0))) + | unbound f = intoEta $ eval' f + | otherwise = subst o + eval' x = subst x + +-- | Is an expression in normal form? +normal :: Expr -> Bool +normal (App (Lam _ _) _) = False +normal (Lam _ (App f (Var 0))) = unbound f +normal (App f x) = normal f && normal x +normal _ = True + +-- | Is an expression in weak head normal form? +whnf :: Expr -> Bool +whnf (App (Lam _ _) _) = False +whnf (Lam _ (App f (Var 0))) = unbound f +whnf (App f _) = whnf f +whnf _ = True diff --git a/src/UntypedLambdaCalculus/Parser.hs b/src/UntypedLambdaCalculus/Parser.hs index f6c065f..217ead9 100644 --- a/src/UntypedLambdaCalculus/Parser.hs +++ b/src/UntypedLambdaCalculus/Parser.hs @@ -10,6 +10,7 @@ import Data.List (foldl1') import Text.Parsec import Text.Parsec.String +-- | The abstract syntax tree of lambda calculus. data Ast = AstVar String | AstLam String Ast | AstApp Ast Ast @@ -22,18 +23,22 @@ instance Show Ast where alg (AstLamF v e) = "(\\" ++ v ++ ". " ++ e ++ ")" alg (AstAppF f x) = "(" ++ f ++ " " ++ x ++ ")" +-- | A variable name. name :: Parser String name = do c <- letter cs <- many alphaNum return $ c : cs +-- | A variable expression. var :: Parser Ast var = AstVar <$> name +-- | Run parser between parentheses. parens :: Parser a -> Parser a parens = between (char '(') (char ')') +-- | A lambda expression. lam :: Parser Ast lam = do char '\\' @@ -43,8 +48,17 @@ lam = do body <- expr return $ foldr AstLam body vars -safeExpr :: Parser Ast -safeExpr = var <|> parens (lam <|> expr) +-- | An application expression. +app :: Parser Ast +app = foldl1' AstApp <$> sepBy1 safeExpr spaces +-- | An expression, but where applications must be surrounded by parentheses, +-- | to avoid ambiguity (infinite recursion on `app` in the case where the first +-- | expression in the application is also an `app`, consuming no input). +safeExpr :: Parser Ast +safeExpr = var <|> lam <|> parens (lam <|> app) + +-- | Since applications do not require parentheses and can contain only a single item, +-- | the `app` parser is sufficient to parse any expression at all. expr :: Parser Ast -expr = foldl1' AstApp <$> sepBy1 safeExpr spaces +expr = app