diff --git a/Bound/Class.hs b/Bound/Class.hs --- a/Bound/Class.hs +++ b/Bound/Class.hs @@ -16,9 +16,9 @@ infixl 1 >>>= --- | This may or may not be a monad transformer, +-- | Instantces may or may not be monad transformers. -- --- If it is, then you can use @m >>>= f = m >>= lift . f@ +-- If they are, then you can use @m >>>= f = m >>= lift . f@ -- -- This is useful for types like expression lists, case alternatives, -- schemas, etc. that may not be expressions in their own right, but often @@ -26,7 +26,7 @@ class Bound t where (>>>=) :: Monad f => t f a -> (a -> f c) -> t f c - -- default (>>>=) :: MonadTrans t, Monad f) => t f a -> (a -> f c) -> t f c + -- default (>>>=) :: (MonadTrans t, Monad f) => t f a -> (a -> f c) -> t f c -- m >>>= f = m >>= lift . f infixr 1 =<<< diff --git a/Bound/Scope.hs b/Bound/Scope.hs --- a/Bound/Scope.hs +++ b/Bound/Scope.hs @@ -31,7 +31,7 @@ import Bound.Class import Bound.Var --- | @Scope b f a@ is a an @f@ expression with bound variables in @b@, and free variables in @a@ +-- | @'Scope' b f a@ is a an @f@ expression with bound variables in @b@, and free variables in @a@ -- -- This stores bound variables as their generalized de Bruijn representation, -- in that the succ's for variable ids are allowed to occur anywhere within the tree @@ -48,7 +48,7 @@ instance Functor f => Functor (Scope b f) where fmap f (Scope a) = Scope (fmap (fmap (fmap f)) a) --- | @toList@ is provides a list (with duplicates) of the free variables +-- | @'toList'@ is provides a list (with duplicates) of the free variables instance Foldable f => Foldable (Scope b f) where foldMap f (Scope a) = foldMap (foldMap (foldMap f)) a @@ -95,7 +95,7 @@ instance Bound (Scope b) where m >>>= f = m >>= lift . f --- | Capture some free variables in an expression to yield a Scope with bound variables +-- | Capture some free variables in an expression to yield a 'Scope' with bound variables in @b@ abstract :: Monad f => (a -> Maybe b) -> f a -> Scope b f a abstract f e = Scope (liftM k e) where k y = case f y of @@ -117,18 +117,17 @@ -- | Enter a scope with one bound variable, instantiating it instantiate1 :: Monad f => f a -> Scope () f a -> f a -instantiate1 e = instantiate (\ () -> e) +instantiate1 e = instantiate (const e) {-# INLINE instantiate1 #-} - --- | @fromScope@ quotients out the possible placements of F in Scope --- distributing them all to the leaves. This yields a traditional deBruijn --- indexing scheme for bound variables. +-- | @'fromScope'@ quotients out the possible placements of 'F' in 'Scope' +-- by distributing them all to the leaves. This yields a more traditional +-- de Bruijn indexing scheme for bound variables. -- -- > fromScope . toScope = id -- > fromScope . toScope . fromScope = fromScope -- --- @(toScope . fromScope)@ is idempotent +-- @('toScope' . 'fromScope')@ is idempotent fromScope :: Monad f => Scope b f a -> f (Var b a) fromScope (Scope s) = s >>= \v -> case v of F e -> liftM F e diff --git a/Bound/Term.hs b/Bound/Term.hs --- a/Bound/Term.hs +++ b/Bound/Term.hs @@ -15,10 +15,11 @@ , closed ) where +import Data.Foldable import Data.Traversable -import Data.Maybe (isJust) +import Prelude hiding (all) --- | @substitute p a w@ replaces the free variable @a@ with @p@ in @w@ +-- | @'substitute' p a w@ replaces the free variable @a@ with @p@ in @w@ substitute :: (Monad f, Eq a) => f a -> a -> f a -> f a substitute p a w = w >>= \b -> if a == b then p else return b {-# INLINE substitute #-} @@ -28,6 +29,6 @@ closed = traverse (const Nothing) {-# INLINE closed #-} -isClosed :: Traversable f => f a -> Bool -isClosed = isJust . closed +isClosed :: Foldable f => f a -> Bool +isClosed = all (const False) {-# INLINE isClosed #-} diff --git a/bound.cabal b/bound.cabal --- a/bound.cabal +++ b/bound.cabal @@ -1,6 +1,6 @@ name: bound category: Language, Compilers/Interpreters -version: 0.1.2 +version: 0.1.3 license: BSD3 cabal-version: >= 1.6 license-file: LICENSE @@ -11,7 +11,33 @@ bug-reports: http://github.com/ekmett/bound/issues copyright: Copyright (C) 2012 Edward A. Kmett synopsis: Combinators for manipulating locally-nameless generalized de Bruijn terms -description: Combinators for manipulating locally-nameless generalized de Bruijn terms +description: + The goal of this package is to make it as easy as possible to deal with name binding without forcing an + awkward monadic style on the user. To that end we provide haskell 98 combinators for manipulating + locally-nameless generalized de Bruijn terms, build over user-supplied term types. A generalized + de Bruijn term is one where you can 'succ' whole trees instead of just individual variables. + . + The approach was first elaborated in Bird and Patterson, \"de Bruijn notation as a nested data type\": + . + + . + However, the combinators they used required higher rank types. Here we use a monad transformer to encapsulate + the novel recursion pattern in their generalized de Bruijn representation. It is named Scope to match up + with the terminology from Conor McBride and James McKinna's \"I am not a number: I am a free variable\", + while providing stronger type safety guarantees. + . + + . + There are three worked examples in the examples folder: + . + * /Simple.hs/ provides an untyped lambda calculus with recursive let bindings. + . + * /Derived.hs/ shows how much of the API can be automated with DeriveTraversable + and adds combinators for building binders with pattern matching. + . + * /Overkill.hs/ provides very strongly typed pattern matching many modern type extensions, including + polymorphic kinds to ensure type safety. In general, the approach taken by Derived seems to deliver + a better power to weight ratio. build-type: Simple extra-source-files: .travis.yml examples/Simple.hs examples/Deriving.hs examples/Overkill.hs diff --git a/examples/Deriving.hs b/examples/Deriving.hs --- a/examples/Deriving.hs +++ b/examples/Deriving.hs @@ -12,7 +12,7 @@ infixl 9 :@ data Exp a - = Var a + = V a | Exp a :@ Exp a | Lam {-# UNPACK #-} !Int (Pat Exp a) (Scope Int Exp a) | Let {-# UNPACK #-} !Int [Scope Int Exp a] (Scope Int Exp a) @@ -20,12 +20,12 @@ deriving (Eq,Ord,Show,Read,Functor,Foldable,Traversable) instance Applicative Exp where - pure = Var + pure = V (<*>) = ap instance Monad Exp where - return = Var - Var a >>= f = f a + return = V + V a >>= f = f a (x :@ y) >>= f = (x >>= f) :@ (y >>= f) Lam n p e >>= f = Lam n (p >>>= f) (e >>>= f) Let n bs e >>= f = Let n (map (>>>= f) bs) (e >>>= f) @@ -41,7 +41,7 @@ | WildP | AsP (Pat f a) | ConP String [Pat f a] - | ViewP (f a) (Pat f a) + | ViewP (Scope Int f a) (Pat f a) deriving (Eq,Ord,Show,Read,Functor,Foldable,Traversable) instance Bound Pat where @@ -49,7 +49,7 @@ WildP >>>= _ = WildP AsP p >>>= f = AsP (p >>>= f) ConP g ps >>>= f = ConP g (map (>>>= f) ps) - ViewP e p >>>= f = ViewP (e >>= f) (p >>>= f) + ViewP e p >>>= f = ViewP (e >>>= f) (p >>>= f) data Alt f a = Alt {-# UNPACK #-} !Int (Pat f a) (Scope Int f a) deriving (Eq,Ord,Show,Read,Functor,Foldable,Traversable) @@ -59,23 +59,30 @@ -- ** smart patterns -data P a = P { pattern :: Pat Exp a, bindings :: [a] } +data P a = P { pattern :: [a] -> Pat Exp a, bindings :: [a] } varp :: a -> P a -varp a = P VarP [a] +varp a = P (const VarP) [a] wildp :: P a -wildp = P WildP [] +wildp = P (const WildP) [] asp :: a -> P a -> P a -asp a (P p as) = P (AsP p) (a:as) +asp a (P p as) = P (\bs -> AsP (p (a:bs))) (a:as) conp :: String -> [P a] -> P a -conp g ps = P (ConP g (map pattern ps)) (ps >>= bindings) +conp g ps = P (ConP g . go ps) (ps >>= bindings) + where + go (P p as:ps) bs = p bs : go ps (bs ++ as) + go [] _ = [] +-- | view patterns can view variables that are bound earlier than them in the pattern +viewp :: Eq a => Exp a -> P a -> P a +viewp t (P p as) = P (\bs -> ViewP (abstract (`elemIndex` bs) t) (p bs)) as + -- | smart lam constructor lam :: Eq a => P a -> Exp a -> Exp a -lam (P p as) t = Lam (length as) p (abstract (`elemIndex` as) t) +lam (P p as) t = Lam (length as) (p []) (abstract (`elemIndex` as) t) -- | smart let constructor let_ :: Eq a => [(a, Exp a)] -> Exp a -> Exp a @@ -85,9 +92,25 @@ -- | smart alt constructor alt :: Eq a => P a -> Exp a -> Alt Exp a -alt (P p as) t = Alt (length as) p (abstract (`elemIndex` as) t) +alt (P p as) t = Alt (length as) (p []) (abstract (`elemIndex` as) t) --- ghci> let_ [("x",Var "y"),("y",Var "x" :@ Var "y")] $ lam (varp "z") (Var "z" :@ Var "y") --- ghci> lam (varp "x") (Var "x") --- ghci> lam (conp "Hello" [varp "x", wildp])) (Var "y") --- ghci> lam (varp "x") $ Case (Var "x") [alt (conp "Hello" [varp "z",wildp]) (Var "x"), alt (varp "y") (Var "y")] +-- >>> let_ [("x",V "y"),("y",V "x" :@ V "y")] $ lam (varp "z") (V "z" :@ V "y") +-- Let 2 [Scope (V (B 1)),Scope (V (B 0) :@ V (B 1))] (Scope (Lam 1 VarP (Scope (V (B 0) :@ V (F (V (B 1))))))) + +-- >>> lam (varp "x") (V "x") +-- Lam 1 VarP (Scope (V (B 0))) + +-- >>> lam (conp "Hello" [varp "x", wildp]) (V "y") +-- Lam 1 (ConP "Hello" [VarP,WildP]) (Scope (V (F (V "y")))) + +-- >>> lam (varp "x") $ Case (V "x") [alt (conp "Hello" [varp "z",wildp]) (V "x"), alt (varp "y") (V "y")] +-- Lam 1 VarP (Scope (Case (V (B 0)) [Alt 1 (ConP "Hello" [VarP,WildP]) (Scope (V (F (V (B 0))))),Alt 1 VarP (Scope (V (B 0)))])) + +-- view patterns can reference name from earlier in the same scope +-- >>> lam (conp "F" [varp "x", viewp (V "x") $ varp "y"]) (V "y") +-- Lam 2 (ConP "F" [VarP,ViewP (Scope (V (B 0))) VarP]) (Scope (V (B 1))) + +-- but like in ghc, they refuse to allow references to subsequent bindings in the scope +-- >>> lam (conp "F" [varp "x", viewp (V "y") $ varp "y"]) (V "y") +-- Lam 2 (ConP "F" [VarP,ViewP (Scope (V (F (V "y")))) VarP]) (Scope (V (B 1))) + diff --git a/examples/Simple.hs b/examples/Simple.hs --- a/examples/Simple.hs +++ b/examples/Simple.hs @@ -3,53 +3,171 @@ -- this is a simple example where lambdas only bind a single variable at a time -- this directly corresponds to the usual de bruijn presentation -import Data.Foldable +import Data.List (elemIndex) +import Data.Foldable hiding (notElem) +import Data.Maybe (fromJust) import Data.Traversable import Control.Monad +import Control.Monad.Trans.Class import Control.Applicative -import Prelude hiding (foldr) +import Prelude hiding (foldr,abs) import Prelude.Extras import Bound infixl 9 :@ -data Exp a = Var a | Exp a :@ Exp a | Lam (Scope () Exp a) +data Exp a + = V a + | Exp a :@ Exp a + | Lam (Scope () Exp a) + | Let [Scope Int Exp a] (Scope Int Exp a) deriving (Eq,Ord,Show,Read) +-- | A smart constructor for Lam +-- +-- >>> lam "y" (lam "x" (V "x" :@ V "y")) +-- Lam (Lam (V (B ()) :@ V (F (V (B ()))))) lam :: Eq a => a -> Exp a -> Exp a lam v b = Lam (abstract1 v b) -instance Eq1 Exp where (==#) = (==) -instance Ord1 Exp where compare1 = compare -instance Show1 Exp where showsPrec1 = showsPrec -instance Read1 Exp where readsPrec1 = readsPrec + +-- | A smart constructor for Let bindings + +let_ :: Eq a => [(a,Exp a)] -> Exp a -> Exp a +let_ [] b = b +let_ bs b = Let (map (abstr . snd) bs) (abstr b) + where vs = map fst bs + abstr = abstract (`elemIndex` vs) + instance Functor Exp where fmap = fmapDefault instance Foldable Exp where foldMap = foldMapDefault instance Applicative Exp where - pure = Var + pure = V (<*>) = ap instance Traversable Exp where - traverse f (Var a) = Var <$> f a - traverse f (x :@ y) = (:@) <$> traverse f x <*> traverse f y - traverse f (Lam e) = Lam <$> traverse f e + traverse f (V a) = V <$> f a + traverse f (x :@ y) = (:@) <$> traverse f x <*> traverse f y + traverse f (Lam e) = Lam <$> traverse f e + traverse f (Let bs b) = Let <$> traverse (traverse f) bs <*> traverse f b instance Monad Exp where - return = Var - Var a >>= f = f a + return = V + V a >>= f = f a (x :@ y) >>= f = (x >>= f) :@ (y >>= f) Lam e >>= f = Lam (e >>>= f) + Let bs b >>= f = Let (map (>>>= f) bs) (b >>>= f) --- \ x -> x --- ghci> lam "x" (Var "x") --- Lam (Var (Bound ())) +-- these 4 classes are needed to help Eq, Ord, Show and Read pass through Scope +instance Eq1 Exp where (==#) = (==) +instance Ord1 Exp where compare1 = compare +instance Show1 Exp where showsPrec1 = showsPrec +instance Read1 Exp where readsPrec1 = readsPrec --- \ x -> x y --- ghci> lam "x" (Var "x" :@ Var "y") --- Lam (Var (Bound ()) :@ Var (Free (Var "y"))) +-- | Compute the normal form of an expression +nf :: Exp a -> Exp a +nf e@V{} = e +nf (Lam b) = Lam $ toScope $ nf $ fromScope b +-- nf (Lam (Scope b)) = Lam $ Scope $ fmap (fmap nf) (nf b) +nf (f :@ a) = case whnf f of + Lam b -> nf (instantiate1 a b) + f' -> nf f' :@ nf a +nf (Let bs b) = nf (inst b) + where es = map inst bs + inst = instantiate (es !!) --- \ y -> \x -> x y --- ghci> lam "y" (lam "x" (Var "x" :@ Var "y")) --- Lam (Lam (Var (Bound ()) :@ Var (Free (Var (Bound ()))))) +-- | Reduce a term to weak head normal form +whnf :: Exp a -> Exp a +whnf e@V{} = e +whnf e@Lam{} = e +whnf (f :@ a) = case whnf f of + Lam b -> whnf (instantiate1 a b) + f' -> f' :@ a +whnf (Let bs b) = whnf (inst b) + where es = map inst bs + inst = instantiate (es !!) +infixr 0 ! +(!) :: Eq a => a -> Exp a -> Exp a +(!) = lam + +-- | Lennart Augustsson's example from "The Lambda Calculus Cooked 4 Ways" +-- +-- Modified to use recursive let, because we can. +-- +-- >>> nf cooked == lam "false" (lam "true" (V"false")) +-- True + +true :: Exp String +true = lam "F" $ lam "T" $ V"T" + +cooked :: Exp a +cooked = fromJust $ closed $ let_ + [ ("False", "f" ! "t" ! V"f") + , ("True", "f" ! "t" ! V"t") + , ("if", "b" ! "t" ! "f" ! V"b" :@ V"f" :@ V"t") + , ("Zero", "z" ! "s" ! V"z") + , ("Succ", "n" ! "z" ! "s" ! V"s" :@ V"n") + , ("one", V"Succ" :@ V"Zero") + , ("two", V"Succ" :@ V"one") + , ("three", V"Succ" :@ V"two") + , ("isZero", "n" ! V"n" :@ V"True" :@ ("m" ! V"False")) + , ("const", "x" ! "y" ! V"x") + , ("Pair", "a" ! "b" ! "p" ! V"p" :@ V"a" :@ V"b") + , ("fst", "ab" ! V"ab" :@ ("a" ! "b" ! V"a")) + , ("snd", "ab" ! V"ab" :@ ("a" ! "b" ! V"b")) + -- we have a lambda calculus extended with recursive bindings, so we don't need to use fix + , ("add", "x" ! "y" ! V"x" :@ V"y" :@ ("n" ! V"Succ" :@ (V"add" :@ V"n" :@ V"y"))) + , ("mul", "x" ! "y" ! V"x" :@ V"Zero" :@ ("n" ! V"add" :@ V"y" :@ (V"mul" :@ V"n" :@ V"y"))) + , ("fac", "x" ! V"x" :@ V"one" :@ ("n" ! V"mul" :@ V"x" :@ (V"fac" :@ V"n"))) + , ("eqnat", "x" ! "y" ! V"x" :@ (V"y" :@ V"True" :@ (V"const" :@ V"False")) :@ ("x1" ! V"y" :@ V"False" :@ ("y1" ! V"eqnat" :@ V"x1" :@ V"y1"))) + , ("sumto", "x" ! V"x" :@ V"Zero" :@ ("n" ! V"add" :@ V"x" :@ (V"sumto" :@ V"n"))) + -- but we could if we wanted to + -- , ("fix", "g" ! ("x" ! V"g":@ (V"x":@V"x")) :@ ("x" ! V"g":@ (V"x":@V"x"))) + -- , ("add", V"fix" :@ ("radd" ! "x" ! "y" ! V"x" :@ V"y" :@ ("n" ! V"Succ" :@ (V"radd" :@ V"n" :@ V"y")))) + -- , ("mul", V"fix" :@ ("rmul" ! "x" ! "y" ! V"x" :@ V"Zero" :@ ("n" ! V"add" :@ V"y" :@ (V"rmul" :@ V"n" :@ V"y")))) + -- , ("fac", V"fix" :@ ("rfac" ! "x" ! V"x" :@ V"one" :@ ("n" ! V"mul" :@ V"x" :@ (V"rfac" :@ V"n")))) + -- , ("eqnat", V"fix" :@ ("reqnat" ! "x" ! "y" ! V"x" :@ (V"y" :@ V"True" :@ (V"const" :@ V"False")) :@ ("x1" ! V"y" :@ V"False" :@ ("y1" ! V"reqnat" :@ V"x1" :@ V"y1")))) + -- , ("sumto", V"fix" :@ ("rsumto" ! "x" ! V"x" :@ V"Zero" :@ ("n" ! V"add" :@ V"x" :@ (V"rsumto" :@ V"n")))) + , ("n5", V"add" :@ V"two" :@ V"three") + , ("n6", V"add" :@ V"three" :@ V"three") + , ("n17", V"add" :@ V"n6" :@ (V"add" :@ V"n6" :@ V"n5")) + , ("n37", V"Succ" :@ (V"mul" :@ V"n6" :@ V"n6")) + , ("n703", V"sumto" :@ V"n37") + , ("n720", V"fac" :@ V"n6") + ] (V"eqnat" :@ V"n720" :@ (V"add" :@ V"n703" :@ V"n17")) + +-- TODO: use a real pretty printer + +prettyPrec :: [String] -> Bool -> Int -> Exp String -> ShowS +prettyPrec _ d n (V a) = showString a +prettyPrec vs d n (x :@ y) = showParen d $ + prettyPrec vs False n x . showChar ' ' . prettyPrec vs True n y +prettyPrec (v:vs) d n (Lam b) = showParen d $ + showString v . showString ". " . prettyPrec vs False n (instantiate1 (V v) b) +prettyPrec vs d n (Let bs b) = showParen d $ + showString "let" . foldr (.) id (zipWith showBinding xs bs) . + showString " in " . indent . prettyPrec ys False n (inst b) + where (xs,ys) = splitAt (length bs) vs + inst = instantiate (\n -> V (xs !! n)) + indent = showString ('\n' : replicate (n + 4) ' ') + showBinding x b = indent . showString x . showString " = " . prettyPrec ys False (n + 4) (inst b) + +prettyWith :: [String] -> Exp String -> String +prettyWith vs t = prettyPrec (filter (`notElem` toList t) vs) False 0 t "" + +pretty :: Exp String -> String +pretty = prettyWith $ [ [i] | i <- ['a'..'z']] ++ [i : show j | j <- [1..], i <- ['a'..'z'] ] + +pp :: Exp String -> IO () +pp = putStrLn . pretty + +main = do + pp cooked + let result = nf cooked + if result == true + then putStrLn "Result correct." + else do + putStrLn "Unexpected result:" + pp result