packages feed

bound 0.1.2 → 0.1.3

raw patch · 6 files changed

+224/−57 lines, 6 filesPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

API changes (from Hackage documentation)

- Bound.Term: isClosed :: Traversable f => f a -> Bool
+ Bound.Term: isClosed :: Foldable f => f a -> Bool

Files

Bound/Class.hs view
@@ -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 =<<<
Bound/Scope.hs view
@@ -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
Bound/Term.hs view
@@ -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 #-}
bound.cabal view
@@ -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\":+  .+  <http://www.cs.uwyo.edu/~jlc/courses/5000_fall_08/debruijn_as_nested_datatype.pdf>+  .+  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.+  .+  <http://www.cs.st-andrews.ac.uk/~james/RESEARCH/notanum.pdf>+  .+  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
examples/Deriving.hs view
@@ -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)))+
examples/Simple.hs view
@@ -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