bound 0.1.3 → 0.1.4

raw patch · 4 files changed

+290/−67 lines, 4 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

• Bound.hs +63/−4
• Bound/Scope.hs +139/−31
• Bound/Var.hs +4/−3
• bound.cabal +84/−29

@@ -8,12 +8,71 @@ -- Stability   :  experimental -- Portability :  portable --+-- We represent the target language itself as an ideal monad supplied by the+-- user, and provide a 'Scope' monad transformer for introducing bound variables+-- in user supplied terms. Users supply a 'Monad' and 'Traversable' instance, and we+-- traverse to find free variables, and use the 'Monad' to perform substitution+-- that avoids bound variables.+--+-- An untyped lambda calculus:+--+-- > import Bound+-- > import Prelude.Extras+--+-- > infixl 9 :@+-- > data Exp a = V a | Exp a :@ Exp a | Lam (Scope () Exp a)+-- >  deriving (Eq,Ord,Show,Read,Functor,Foldable,Traversable)+--+-- > instance Eq1 Exp   where (==#)      = (==)+-- > instance Ord1 Exp  where compare1   = compare+-- > instance Show1 Exp where showsPrec1 = showsPrec+-- > instance Read1 Exp where readsPrec1 = readsPrec+-- > instance Applicative Exp where pure = V; (<*>) = ap+--+-- > instance Monad Exp where+-- >   return = V+-- >   V a      >>= f = f a+-- >   (x :@ y) >>= f = (x >>= f) :@ (y >>= f)+-- >   Lam e    >>= f = Lam (e >>>= f)+-- >+-- > lam :: Eq a => a -> Exp a -> Exp a+-- > lam v b = Lam (abstract1 v b)+--+-- > whnf :: Exp a -> Exp a+-- > whnf (f :@ a) = case whnf f of+-- >   Lam b -> whnf (instantiate1 a b)+-- >   f'    -> f' :@ a+-- > whnf e = e+-- ---------------------------------------------------------------------------- module Bound-  ( module Bound.Var-  , module Bound.Class-  , module Bound.Scope-  , module Bound.Term+  (+  -- * Scopes introduce bound variables in user terms+    Scope(..)+  -- ** Abstraction over bound variables+  , abstract, abstract1+  -- ** Instantiation of bound variables+  , instantiate, instantiate1+  -- * Combinators for manipulating user terms+  , substitute+  , isClosed+  , closed+  -- * Structures permitting substitution+  , Bound(..)+  , (=<<<)+  -- ** Conversion to Traditional de Bruijn+  , Var(..)+  , fromScope+  , toScope+  -- ** Advanced substitution combinators+  , splat+  , mapBound, mapScope+  , liftMBound, liftMScope+  , foldMapBound, foldMapScope+  , traverseBound_, traverseScope_+  , mapMBound_, mapMScope_+  , traverseBound, traverseScope+  , mapMBound, mapMScope   ) where  import Bound.Var

@@ -15,34 +15,57 @@   , abstract, abstract1   -- * Instantiation   , instantiate, instantiate1-  -- * Substitution-  , splat-  -- * Quotienting+  -- * Traditional de Bruijn   , fromScope   , toScope+  -- * Bound variable manipulation+  , splat+  , bindings+  , mapBound+  , mapScope+  , liftMBound+  , liftMScope+  , foldMapBound+  , foldMapScope+  , traverseBound_+  , traverseScope_+  , mapMBound_+  , mapMScope_+  , traverseBound+  , traverseScope+  , mapMBound+  , mapMScope   ) where +import Bound.Class+import Bound.Var+import Control.Applicative+import Control.Monad hiding (mapM, mapM_)+import Control.Monad.Trans.Class+import Data.Bifunctor+import Data.Bifoldable+import Data.Bitraversable import Data.Foldable+import Data.Monoid import Data.Traversable-import Control.Monad-import Control.Monad.Trans.Class-import Control.Applicative import Prelude.Extras-import Bound.Class-import Bound.Var+import Prelude hiding (foldr, mapM, mapM_) --- | @'Scope' b f a@ is a an @f@ expression with bound variables in @b@, and free variables in @a@+-- | @'Scope' b f a@ is 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--- permitting /O(1)/ weakening and allowing more sharing opportunities. --- Here the deBruijn 0 is represented by the 'B' constructor of 'Var', while the --- de Bruijn 'succ' (which may be applied to an entire tree!) is handled by 'F'.+-- We store bound variables as their generalized de Bruijn representation,+-- in that we're allowed to 'lift' (using 'F') an entire tree rather than only succ individual variables,+-- but we're still only allowed to do so once per 'Scope'. Weakening trees permits /O(1)/ weakening+-- permits more sharing opportunities. Here the deBruijn 0 is represented by the 'B' constructor of+-- 'Var', while the de Bruijn 'succ' (which may be applied to an entire tree!) is handled by 'F'. ----- NB: equality and comparison quotient out the distinct 'F' placements allowed by --- the choice of a generalized de Bruijn representation and return the same result as a traditional de Bruijn+-- NB: equality and comparison quotient out the distinct 'F' placements allowed by+-- the generalized de Bruijn representation and return the same result as a traditional de Bruijn -- representation would.-+--+-- Logically you can think of this as if the shape were the traditional @f (Var b a)@, but the extra +-- 'f a' inside permits us a cheaper 'lift'.+-- newtype Scope b f a = Scope { unscope :: f (Var b (f a)) }  instance Functor f => Functor (Scope b f) where@@ -75,22 +98,16 @@   compare1 a b = liftM Lift2 (fromScope a) `compare1` liftM Lift2 (fromScope b)   -- compare1 a b = compare1 (mangleScope a) (mangleScope b) -mangleScope :: Functor f => Scope b f a -> f (Lift2 Var b (Lift1 f a))-mangleScope (Scope a) = fmap (Lift2 . fmap Lift1) a-{-# INLINE mangleScope #-}--unmangleScope :: Functor f => f (Lift2 Var b (Lift1 f a)) -> Scope b f a-unmangleScope a = Scope (fmap (fmap lower1 . lower2) a)-{-# INLINE unmangleScope #-}-- instance (Functor f, Show b, Show1 f, Show a) => Show  (Scope b f a) where showsPrec = showsPrec1 instance (Functor f, Show b, Show1 f)         => Show1 (Scope b f)   where-  showsPrec1 d a = showParen (d > 10) $ showString "Scope " . showsPrec1 11 (mangleScope a)+  showsPrec1 d a = showParen (d > 10) $ showString "Scope " . showsPrec1 11 (fmap (Lift2 . fmap Lift1) (unscope a))  instance (Functor f, Read b, Read1 f, Read a) => Read  (Scope b f a) where readsPrec = readsPrec1 instance (Functor f, Read b, Read1 f)         => Read1 (Scope b f) where-  readPrec1 = liftM unmangleScope readPrec1+  readsPrec1 d = readParen (d > 10) $ \r -> do+    ("Scope", r') <- lex r+    (s, r'') <- readsPrec1 11 r'+    return (Scope (fmap (fmap lower1 . lower2) s), r'')  instance Bound (Scope b) where   m >>>= f = m >>= lift . f@@ -115,13 +132,13 @@   F a -> a {-# INLINE instantiate #-} --- | Enter a scope with one bound variable, instantiating it+-- | Enter a 'Scope' that binds one variable, instantiating it instantiate1 :: Monad f => f a -> Scope () f a -> f a instantiate1 e = instantiate (const e) {-# INLINE instantiate1 #-}  -- | @'fromScope'@ quotients out the possible placements of 'F' in 'Scope'--- by distributing them all to the leaves. This yields a more traditional +-- by distributing them all to the leaves. This yields a more traditional -- de Bruijn indexing scheme for bound variables. -- -- > fromScope . toScope = id@@ -138,9 +155,100 @@ toScope e = Scope (liftM (fmap return) e) {-# INLINE toScope #-} --- | Perform substitution on both bound and free variables in a scope+-- | Perform substitution on both bound and free variables in a 'Scope' splat :: Monad f => (a -> f c) -> (b -> f c) -> Scope b f a -> f c splat f unbind s = unscope s >>= \v -> case v of   B b -> unbind b   F ea -> ea >>= f {-# INLINE splat #-}++-- Return a list of occurences of the variables bound by this scope+bindings :: Foldable f => Scope b f a -> [b]+bindings (Scope s) = foldr f [] s where+  f (B v) vs = v : vs+  f _ vs     = vs+{-# INLINE bindings #-}++-- | Perform a change of variables on bound variables+mapBound :: Functor f => (b -> b') -> Scope b f a -> Scope b' f a+mapBound f (Scope s) = Scope (fmap f' s) where+  f' (B b) = B (f b)+  f' (F a) = F a+{-# INLINE mapBound #-}++-- | Perform a change of variables, reassigning both bound and free variables.+mapScope :: Functor f => (b -> d) -> (a -> c) -> Scope b f a -> Scope d f c+mapScope f g (Scope s) = Scope $ fmap (bimap f (fmap g)) s+{-# INLINE mapScope #-}++-- | Perform a change of variables on bound variables given only a 'Monad' instance+liftMBound :: Monad m => (b -> b') -> Scope b m a -> Scope b' m a+liftMBound f (Scope s) = Scope (liftM f' s) where+  f' (B b) = B (f b)+  f' (F a) = F a+{-# INLINE liftMBound #-}++-- | A version of 'mapScope' that can be used when you only have the 'Monad' instance+liftMScope :: Monad m => (b -> d) -> (a -> c) -> Scope b m a -> Scope d m c+liftMScope f g (Scope s) = Scope $ liftM (bimap f (liftM g)) s+{-# INLINE liftMScope #-}++-- | Obtain a result by collecting information from both bound and free variables+foldMapBound :: (Foldable f, Monoid r) => (b -> r) -> Scope b f a -> r+foldMapBound f (Scope s) = foldMap f' s where+  f' (B a) = f a+  f' _     = mempty+{-# INLINE foldMapBound #-}++-- | Obtain a result by collecting information from both bound and free variables+foldMapScope :: (Foldable f, Monoid r) => (b -> r) -> (a -> r) -> Scope b f a -> r+foldMapScope f g (Scope s) = foldMap (bifoldMap f (foldMap g)) s+{-# INLINE foldMapScope #-}++traverseBound_ :: (Applicative g, Foldable f) => (b -> g d) -> Scope b f a -> g ()+traverseBound_ f (Scope s) = traverse_ f' s+  where f' (B a) = () <$ f a+        f' _     = pure ()+{-# INLINE traverseBound_ #-}++--- | Traverse both the variables bound by this scope and any free variables.+traverseScope_ :: (Applicative g, Foldable f) => (b -> g d) -> (a -> g c) -> Scope b f a -> g ()+traverseScope_ f g (Scope s) = traverse_ (bitraverse_ f (traverse_ g)) s+{-# INLINE traverseScope_ #-}++-- | mapM_ over the variables bound by this scope+mapMBound_ :: (Monad g, Foldable f) => (b -> g d) -> Scope b f a -> g ()+mapMBound_ f (Scope s) = mapM_ f' s where+  f' (B a) = do _ <- f a; return ()+  f' _     = return ()+{-# INLINE mapMBound_ #-}++--- | A 'traverseScope_' that can be used when you only have a 'Monad' instance+mapMScope_ :: (Monad m, Foldable f) => (b -> m d) -> (a -> m c) -> Scope b f a -> m ()+mapMScope_ f g (Scope s) = mapM_ (bimapM_ f (mapM_ g)) s+{-# INLINE mapMScope_ #-}++--- | Traverse both bound and free variables+traverseBound :: (Applicative g, Traversable f) => (b -> g c) -> Scope b f a -> g (Scope c f a)+traverseBound f (Scope s) = Scope <$> traverse f' s where+  f' (B b) = B <$> f b+  f' (F a) = pure (F a)+{-# INLINE traverseBound #-}++--- | Traverse both bound and free variables+traverseScope :: (Applicative g, Traversable f) => (b -> g d) -> (a -> g c) -> Scope b f a -> g (Scope d f c)+traverseScope f g (Scope s) = Scope <$> traverse (bitraverse f (traverse g)) s+{-# INLINE traverseScope #-}++--- | mapM over both bound and free variables+mapMBound :: (Monad m, Traversable f) => (b -> m c) -> Scope b f a -> m (Scope c f a)+mapMBound f (Scope s) = liftM Scope (mapM f' s) where+  f' (B b) = liftM B (f b)+  f' (F a) = return (F a)+{-# INLINE mapMBound #-}++--- | A 'traverseScope' that can be used when you only have a 'Monad' instance+mapMScope :: (Monad m, Traversable f) => (b -> m d) -> (a -> m c) -> Scope b f a -> m (Scope d f c)+mapMScope f g (Scope s) = liftM Scope (mapM (bimapM f (mapM g)) s)+{-# INLINE mapMScope #-}+

@@ -20,11 +20,12 @@ import Control.Applicative import Control.Monad (ap) import Prelude.Extras-import Text.Read  -- | \"I am not a number, I am a /free monad/!\" -- -- @Var b a@ represents variables that may either be "bound" (@B@) or "free" (@F@)+--+-- It is also technically a free monad in the same near trivial sense as 'Either' data Var b a   = B b -- this is a bound variable   | F a -- this is a free variable@@ -66,9 +67,9 @@ instance Eq2 Var   where (==##)     = (==) instance Ord2 Var  where compare2   = compare instance Show2 Var where showsPrec2 = showsPrec-instance Read2 Var where readPrec2  = readPrec+instance Read2 Var where readsPrec2  = readsPrec  instance Eq b   => Eq1   (Var b) where (==#)      = (==) instance Ord b  => Ord1  (Var b) where compare1   = compare instance Show b => Show1 (Var b) where showsPrec1 = showsPrec-instance Read b => Read1 (Var b) where readPrec1  = readPrec+instance Read b => Read1 (Var b) where readsPrec1  = readsPrec

@@ -1,6 +1,6 @@ name:          bound category:      Language, Compilers/Interpreters-version:       0.1.3+version:       0.1.4 license:       BSD3 cabal-version: >= 1.6 license-file:  LICENSE@@ -10,37 +10,92 @@ homepage:      http://github.com/ekmett/bound/ 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+synopsis:      Haskell 98 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.+   We represent the target language itself as an ideal monad supplied by the+   user, and provide a 'Scope' monad transformer for introducing bound variables+   in user supplied terms. Users supply a 'Monad' and 'Traversable' instance, and+   we traverse to find free variables, and use the Monad to perform substitution+   that avoids bound variables.+   .+   An untyped lambda calculus:+   .+   > import Bound+   > import Prelude.Extras+   .+   > infixl 9 :@+   > data Exp a = V a | Exp a :@ Exp a | Lam (Scope () Exp a)+   >  deriving (Eq,Ord,Show,Read,Functor,Foldable,Traversable)+   .+   > instance Eq1 Exp   where (==#)      = (==)+   > instance Ord1 Exp  where compare1   = compare+   > instance Show1 Exp where showsPrec1 = showsPrec+   > instance Read1 Exp where readsPrec1 = readsPrec+   > instance Applicative Exp where pure = V; (<*>) = ap+   .+   > instance Monad Exp where+   >   return = V+   >   V a      >>= f = f a+   >   (x :@ y) >>= f = (x >>= f) :@ (y >>= f)+   >   Lam e    >>= f = Lam (e >>>= f)+   >+   > lam :: Eq a => a -> Exp a -> Exp a+   > lam v b = Lam (abstract1 v b)+   .+   > whnf :: Exp a -> Exp a+   > whnf (f :@ a) = case whnf f of+   >   Lam b -> whnf (instantiate1 a b)+   >   f'    -> f' :@ a+   > whnf e = e+   .+   The classes from Prelude.Extras are used to facilitate the automatic deriving+   of 'Eq', 'Ord', 'Show, and 'Read' in the presence of polymorphic recursion used+   inside 'Scope'.+   .+   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.+   .+   With generalized de Bruijn term you can 'lift' whole trees instead of just+   applying 'succ' to individual variables, weakening the all variables bound+   by a scope. and by giving binders more structure we can permit easy+   simultaneous substitution.+   .+   The approach was first elaborated upon by Richard Bird and Ross Patterson +   in \"de Bruijn notation as a nested data type\", available from+   <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+   demonstrate that the higher rank @gfold@ combinator they used isn't necessary+   to build the monad and 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 and usage pattern from Conor McBride+   and James McKinna's \"I am not a number: I am a free variable\", available from+   <http://www.cs.st-andrews.ac.uk/~james/RESEARCH/notanum.pdf>, but since the+   set of variables is visible in the type, we can provide stronger type safety+   guarantees.+   .+   There are longer worked examples in the @examples/@ folder:+   .+   <https://github.com/ekmett/bound/tree/master/examples>+   .+   (1) /Simple.hs/ provides an untyped lambda calculus with recursive let bindings.+     and includes an evaluator for the untyped lambda calculus and a longer example+     taken from Lennart Augustsson's "λ-calculus cooked four ways" available from+     <http://www.augustsson.net/Darcs/Lambda/top.pdf>+   .+   2. /Derived.hs/ shows how much of the API can be automated with DeriveTraversable+     and adds combinators for building binders that support pattern matching.+   .+   3. /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+extra-source-files:+  .travis.yml+  examples/Simple.hs+  examples/Deriving.hs+  examples/Overkill.hs  source-repository head   type: git