Made variables indexed by `Fin n` instead of Int.

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

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

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)

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

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 Data.Injection (inject)
-import UntypedLambdaCalculus.Parser (Ast (AstVar, AstLam, AstApp), AstF (AstVarF, AstLamF, AstAppF))
+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
+data Expr n = Free String
-          | Var Int
+            | Var (Fin n)
-          | Lam String Expr
+            | Lam String (Expr (Succ n))
-          | App Expr Expr
+            | App (Expr n) (Expr n)
 
 makeBaseFunctor ''Expr
 
-instance Show Expr where
+exprUp :: Nat n => Expr n -> Expr (Succ n)
-  show = cataReader alg []
+exprUp (Free v) = Free v
-    where alg :: Algebra ExprF (Reader [String] String)
+exprUp (Var v) = Var $ finUp v
-          alg (FreeF v)   = return v
+exprUp (Lam v e) = Lam v $ exprUp e
-          alg (VarF  v)   = reader (\vars -> vars !! v ++ ':' : show v)
+exprUp (App f x) = App (exprUp f) (exprUp x)
-          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.
+instance Show (Expr Zero) where
--- | In other words, data flows outside-in, reductions flow inside-out.
+  show x = runReader (alg x) Empty
-cataReader :: Recursive t => Algebra (Base t) (Reader s a) -> s -> t -> a
+    where alg :: Nat n => Expr n -> Reader (Vec String n) String
-cataReader alg s x = runReader (cata alg x) s
+          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 :: Nat n => Expr (Succ n) -> Bool
-unbound = cataReader alg 0
+unbound x = runReader (alg x) Zero
-  where alg :: Algebra ExprF (Reader Int Bool)
+  where alg :: Nat n => Expr (Succ n) -> Reader (Fin (Succ n)) Bool
-        alg (FreeF _)  = return True
+        alg (Free _)  = return True
-        alg (VarF v)   = reader (/= v)
+        alg (Var v)   = reader (/= v)
-        alg (AppF f x) = (&&) <$> f <*> x
+        alg (App f x) = (&&) <$> alg f <*> alg x
-        alg (LamF _ e) = local (+ 1) e
+        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 :: Ast -> Expr Zero
-canonym = cataReader alg []
+canonym x = runReader (alg x) Empty
-  where alg :: Algebra AstF (Reader [String] Expr)
+  where alg :: Nat n => Ast -> Reader (Vec String n) (Expr n)
-        alg (AstVarF v)   = maybe (Free v) Var <$> findIndex (== v) <$> ask
+        alg (AstVar v)   = maybe (Free v) Var <$> elemIndexVec v <$> ask
-        alg (AstLamF v e) = Lam v <$> local (v :) e
+        alg (AstLam v e) = Lam v <$> withReader (v :.) (alg e)
-        alg (AstAppF n m) = App <$> n <*> m
+        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 :: Nat n => Expr n -> Expr (Succ n)
-introduceBindingInExpr = cataReader alg 0
+introduceBindingInExpr (Var v) = Var $ Succ v
-  where alg :: Algebra ExprF (Reader Int Expr)
+introduceBindingInExpr o@(Lam _ _) = exprUp o
-        alg (VarF v) = reader $ \x ->
+introduceBindingInExpr (Free x) = Free x
-          if v > x then Var $ v + 1 else Var v
+introduceBindingInExpr (App f x) = App (introduceBindingInExpr f) (introduceBindingInExpr x)
-        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
 
-introduceBinding :: Expr -> Reader [Expr] a -> Reader [Expr] a
+intoEta :: Nat n => Expr (Succ n) -> Expr n
-introduceBinding x = local (\exprs -> x : map introduceBindingInExpr exprs)
+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
+subst :: Nat n => Expr n -> Expr (Succ n) -> Expr n
-intoBinding = introduceBinding (Var 0)
+subst val x = runReader (subst' val x) Zero
-
+  where subst' :: Nat n => Expr n -> Expr (Succ n) -> Reader (Fin (Succ n)) (Expr n)
-intoEta :: Reader [Expr] a -> Reader [Expr] a
+        subst' _   (Free x)  = return $ Free x
-intoEta = introduceBinding undefined
+        subst' val (Var x)   = maybe val Var <$> asks (finRemove x)
-
+        subst' val (App f x) = App <$> subst' val f <*> subst' val x
--- | Substitute all bound variables in an expression for their values,
+        subst' val (Lam v e) = Lam v <$> withReader Succ (subst' (introduceBindingInExpr val) e)
--- | 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
 
 -- | Evaluate a variable to normal form.
-eval :: Expr -> Expr
+eval :: Nat n => Expr n -> Expr n
-eval expr = runReader (eval' expr) []
+eval (App f' x) = case eval f' of
-  where eval' (App f' x') = do
+  Lam _ e -> eval $ subst x e
-          f <- eval' f'
+  f -> App f (eval x)
-          x <- eval' x'
+eval o@(Lam _ (App f (Var Zero)))
-          case f of
+  | unbound f = eval $ intoEta f
-            Lam _ e -> introduceBinding x $ eval' e
+  | otherwise = o
-            _ -> return $ App f x
+eval o = o
-        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 :: 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

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