From d74f17007a7987c40de6ccb16f02439745014e9f Mon Sep 17 00:00:00 2001 From: James Martin Date: Fri, 16 Aug 2019 18:37:55 -0700 Subject: [PATCH] Made variables indexed by `Fin n` instead of Int. --- src/Data/Fin.hs | 60 ++++++++++ src/Data/Injection.hs | 11 ++ src/Data/Type/Nat.hs | 28 +++++ src/Data/Vec.hs | 24 ++++ src/UntypedLambdaCalculus.hs | 165 +++++++++++++--------------- src/UntypedLambdaCalculus/Parser.hs | 18 +++ 6 files changed, 215 insertions(+), 91 deletions(-) create mode 100644 src/Data/Fin.hs create mode 100644 src/Data/Injection.hs create mode 100644 src/Data/Type/Nat.hs create mode 100644 src/Data/Vec.hs diff --git a/src/Data/Fin.hs b/src/Data/Fin.hs new file mode 100644 index 0000000..4ba2371 --- /dev/null +++ b/src/Data/Fin.hs @@ -0,0 +1,60 @@ +{-# LANGUAGE TypeFamilies, GADTs, MultiParamTypeClasses #-} +module Data.Fin (Fin (Zero, Succ), finUp, toInt, pred, finRemove) where + +import Data.Functor.Foldable (Base, Recursive, project, cata) +import Data.Injection (Injection, inject) +import Data.Type.Nat (Nat, Zero, Succ, GTorEQ) +import Prelude hiding (pred) +import Unsafe.Coerce (unsafeCoerce) + +data Fin n where + -- Fin Zero is uninhabited. Fin (Succ Zero) has one inhabitant. + Zero :: Nat n => Fin (Succ n) + Succ :: Nat n => Fin n -> Fin (Succ n) + +type instance Base (Fin n) = Maybe + +instance (Nat n, Nat m, GTorEQ m n) => Injection (Fin n) (Fin m) where + inject = unsafeCoerce + +-- | Coerce a `Fin n` into a `Fin (Succ n)`. +finUp :: Nat n => Fin n -> Fin (Succ n) +finUp Zero = Zero +finUp (Succ n) = Succ (finUp n) + +instance (Nat n) => Recursive (Fin n) where + project Zero = Nothing + project (Succ n) = Just $ finUp n + +instance (Nat n) => Eq (Fin n) where + Zero == Zero = True + Succ n == Succ m = n == m + _ == _ = False + +instance Nat n => Ord (Fin n) where + compare Zero Zero = EQ + compare (Succ n) Zero = GT + compare Zero (Succ n) = LT + compare (Succ n) (Succ m) = compare n m + +toInt :: Nat n => Fin n -> Int +toInt = cata alg + where alg Nothing = 0 + alg (Just n) = n + 1 + +instance (Nat n) => Show (Fin n) where + show = show . toInt + +pred :: Nat n => Fin (Succ n) -> Maybe (Fin n) +pred Zero = Nothing +pred (Succ n) = Just n + +-- | Remove an element from a `Fin`'s domain. +-- | Like a generalized `pred`, only you can remove elements other than `Zero`. +finRemove :: Nat n => Fin (Succ n) -> Fin (Succ n) -> Maybe (Fin n) +finRemove n m + | n == m = Nothing + | n > m = pred n + -- I am convinced it is not possible to prove to the compiler + -- that this function is valid without `unsafeCoerce`. + | n < m = Just $ unsafeCoerce n diff --git a/src/Data/Injection.hs b/src/Data/Injection.hs new file mode 100644 index 0000000..982a3cd --- /dev/null +++ b/src/Data/Injection.hs @@ -0,0 +1,11 @@ +{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-} +module Data.Injection (Injection, inject) where + +class Injection a b where + inject :: a -> b + +instance Injection a a where + inject = id + +instance Injection a (Maybe a) where + inject = Just diff --git a/src/Data/Type/Nat.hs b/src/Data/Type/Nat.hs new file mode 100644 index 0000000..c04598e --- /dev/null +++ b/src/Data/Type/Nat.hs @@ -0,0 +1,28 @@ +{-# LANGUAGE EmptyDataDecls, MultiParamTypeClasses, FunctionalDependencies, FlexibleInstances, UndecidableInstances #-} +module Data.Type.Nat (Nat, Zero, Succ, TOrdering, GT, EQ, LT, Compare, GTorEQ) where + +class Nat n +data Zero +instance Nat Zero +data Succ n +instance (Nat n) => Nat (Succ n) + +class TOrdering c +data GT +instance TOrdering GT +data EQ +instance TOrdering EQ +data LT + +class Compare n m c | n m -> c + +instance Compare Zero Zero EQ +instance Nat n => Compare (Succ n) Zero GT +instance Nat n => Compare Zero (Succ n) LT +instance (Nat n, Nat m, TOrdering c, Compare n m c) => Compare (Succ n) (Succ m) c + +class GTorEQ n m +instance GTorEQ Zero Zero +instance Nat n => GTorEQ n n +instance Nat n => GTorEQ (Succ n) Zero +instance (Nat n, Nat m, GTorEQ n m) => GTorEQ (Succ n) (Succ m) diff --git a/src/Data/Vec.hs b/src/Data/Vec.hs new file mode 100644 index 0000000..6f35cc7 --- /dev/null +++ b/src/Data/Vec.hs @@ -0,0 +1,24 @@ +{-# LANGUAGE GADTs, TypeOperators, TypeSynonymInstances, FlexibleInstances #-} +module Data.Vec (Vec (Empty, (:.)), (!.), elemIndexVec, vmap) where + +import Data.Fin (Fin (Zero, Succ)) +import Data.Type.Nat (Nat, Zero, Succ) + +data Vec a n where + Empty :: Vec a Zero + (:.) :: Nat n => a -> Vec a n -> Vec a (Succ n) + +-- | Equivalent to fmap. It is impossible to implement Functor on Vec for stupid reasons. +vmap :: (a -> b) -> Vec a n -> Vec b n +vmap _ Empty = Empty +vmap f (x :. xs) = f x :. vmap f xs + +(!.) :: Nat n => Vec a n -> Fin n -> a +(!.) (x :. _ ) Zero = x +(!.) (_ :. xs) (Succ n) = xs !. n + +elemIndexVec :: (Eq a, Nat n) => a -> Vec a n -> Maybe (Fin n) +elemIndexVec _ Empty = Nothing +elemIndexVec x (x' :. xs) + | x == x' = Just Zero + | otherwise = Succ <$> elemIndexVec x xs diff --git a/src/UntypedLambdaCalculus.hs b/src/UntypedLambdaCalculus.hs index 9adb32e..f218817 100644 --- a/src/UntypedLambdaCalculus.hs +++ b/src/UntypedLambdaCalculus.hs @@ -1,130 +1,113 @@ -{-# LANGUAGE TemplateHaskell, TypeFamilies, DeriveFunctor, DeriveFoldable, DeriveTraversable #-} +{-# LANGUAGE TemplateHaskell, TypeFamilies, DeriveFunctor, DeriveFoldable, DeriveTraversable, FlexibleInstances #-} 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 Control.Monad.Reader (Reader, runReader, ask, local, withReader, reader, asks) +import Data.Fin (Fin (Zero, Succ), finUp, finRemove) import Data.Function (fix) -import Data.Functor.Foldable (Base, Recursive, cata, embed, project) +import Data.Functor.Foldable (Base, Recursive, Corecursive, ListF (Nil, Cons), cata, embed, project) import Data.Functor.Foldable.TH (makeBaseFunctor) -import Data.List (findIndex) -import UntypedLambdaCalculus.Parser (Ast (AstVar, AstLam, AstApp), AstF (AstVarF, AstLamF, AstAppF)) +import Data.Injection (inject) +import Data.Maybe (fromJust) +import Data.Type.Nat (Nat, Succ, Zero) +import Data.Vec (Vec (Empty, (:.)), (!.), vmap, elemIndexVec) +import UntypedLambdaCalculus.Parser (Ast (AstVar, AstLam, AstApp)) --- | 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 - | App Expr Expr +data Expr n = Free String + | Var (Fin n) + | Lam String (Expr (Succ n)) + | App (Expr n) (Expr n) 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 ++ ")" +exprUp :: Nat n => Expr n -> Expr (Succ n) +exprUp (Free v) = Free v +exprUp (Var v) = Var $ finUp v +exprUp (Lam v e) = Lam v $ exprUp e +exprUp (App f x) = App (exprUp f) (exprUp 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 +instance Show (Expr Zero) where + show x = runReader (alg x) Empty + where alg :: Nat n => Expr n -> Reader (Vec String n) String + alg (Free v) = return v + alg (Var v) = reader (\vars -> vars !. v ++ ':' : show v) + alg (Lam v e) = do + body <- withReader (v :.) $ alg e + return $ "(\\" ++ v ++ ". " ++ body ++ ")" + alg (App f' x') = do + f <- alg f' + x <- alg x' + return $ "(" ++ f ++ " " ++ x ++ ")" -- | Determine whether the variable bound by a lambda expression is used in its body. -- | This is used in eta reduction, where `(\x. f x)` reduces to `f` when `x` is not bound in `f`. -unbound :: Expr -> Bool -unbound = cataReader alg 0 - where alg :: Algebra ExprF (Reader Int Bool) - alg (FreeF _) = return True - alg (VarF v) = reader (/= v) - alg (AppF f x) = (&&) <$> f <*> x - alg (LamF _ e) = local (+ 1) e +unbound :: Nat n => Expr (Succ n) -> Bool +unbound x = runReader (alg x) Zero + where alg :: Nat n => Expr (Succ n) -> Reader (Fin (Succ n)) Bool + alg (Free _) = return True + alg (Var v) = reader (/= v) + alg (App f x) = (&&) <$> alg f <*> alg x + alg (Lam _ e) = withReader Succ $ alg e -- | 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 - - +canonym :: Ast -> Expr Zero +canonym x = runReader (alg x) Empty + where alg :: Nat n => Ast -> Reader (Vec String n) (Expr n) + alg (AstVar v) = maybe (Free v) Var <$> elemIndexVec v <$> ask + alg (AstLam v e) = Lam v <$> withReader (v :.) (alg e) + alg (AstApp n m) = App <$> alg n <*> alg m -- | 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 +introduceBindingInExpr :: Nat n => Expr n -> Expr (Succ n) +introduceBindingInExpr (Var v) = Var $ Succ v +introduceBindingInExpr o@(Lam _ _) = exprUp o +introduceBindingInExpr (Free x) = Free x +introduceBindingInExpr (App f x) = App (introduceBindingInExpr f) (introduceBindingInExpr x) -introduceBinding :: Expr -> Reader [Expr] a -> Reader [Expr] a -introduceBinding x = local (\exprs -> x : map introduceBindingInExpr exprs) +intoEta :: Nat n => Expr (Succ n) -> Expr n +intoEta x = runReader (intoEta' x) Zero + where intoEta' :: Nat n => Expr (Succ n) -> Reader (Fin (Succ n)) (Expr n) + intoEta' (Free x) = return $ Free x + intoEta' (Var x) = Var <$> fromJust <$> asks (finRemove x) + intoEta' (App f x) = App <$> intoEta' f <*> intoEta' x + intoEta' (Lam v e) = Lam v <$> withReader Succ (intoEta' e) -intoBinding :: Reader [Expr] a -> Reader [Expr] a -intoBinding = introduceBinding (Var 0) - -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 - -- 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 +subst :: Nat n => Expr n -> Expr (Succ n) -> Expr n +subst val x = runReader (subst' val x) Zero + where subst' :: Nat n => Expr n -> Expr (Succ n) -> Reader (Fin (Succ n)) (Expr n) + subst' _ (Free x) = return $ Free x + subst' val (Var x) = maybe val Var <$> asks (finRemove x) + subst' val (App f x) = App <$> subst' val f <*> subst' val x + subst' val (Lam v e) = Lam v <$> withReader Succ (subst' (introduceBindingInExpr val) 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 +eval :: Nat n => Expr n -> Expr n +eval (App f' x) = case eval f' of + Lam _ e -> eval $ subst x e + f -> App f (eval x) +eval o@(Lam _ (App f (Var Zero))) + | unbound f = eval $ intoEta f + | otherwise = o +eval o = o -- | Is an expression in normal form? -normal :: Expr -> Bool +normal :: Nat n => Expr n -> Bool normal (App (Lam _ _) _) = False -normal (Lam _ (App f (Var 0))) = unbound f +normal (Lam _ (App f (Var Zero))) = unbound f normal (App f x) = normal f && normal x normal _ = True -- | Is an expression in weak head normal form? -whnf :: Expr -> Bool +whnf :: Nat n => Expr n -> Bool whnf (App (Lam _ _) _) = False -whnf (Lam _ (App f (Var 0))) = unbound f +whnf (Lam _ (App f (Var Zero))) = unbound f whnf (App f _) = whnf f whnf _ = True diff --git a/src/UntypedLambdaCalculus/Parser.hs b/src/UntypedLambdaCalculus/Parser.hs index 217ead9..6fdb370 100644 --- a/src/UntypedLambdaCalculus/Parser.hs +++ b/src/UntypedLambdaCalculus/Parser.hs @@ -14,6 +14,7 @@ import Text.Parsec.String data Ast = AstVar String | AstLam String Ast | AstApp Ast Ast + | AstLet String Ast Ast makeBaseFunctor ''Ast @@ -23,6 +24,9 @@ instance Show Ast where alg (AstLamF v e) = "(\\" ++ v ++ ". " ++ e ++ ")" alg (AstAppF f x) = "(" ++ f ++ " " ++ x ++ ")" +somespaces :: Parser () +somespaces = skipMany1 space + -- | A variable name. name :: Parser String name = do @@ -38,6 +42,20 @@ var = AstVar <$> name parens :: Parser a -> Parser a parens = between (char '(') (char ')') +let_ :: Parser Ast +let_ = do + string ".let" + somespaces + v <- name + somespaces + char '=' + somespaces + x <- safeExpr + somespaces + string ".in" + e <- expr + return $ AstApp (AstLam v e) x + -- | A lambda expression. lam :: Parser Ast lam = do