diff --git a/Bound.hs b/Bound.hs --- a/Bound.hs +++ b/Bound.hs @@ -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 diff --git a/Bound/Scope.hs b/Bound/Scope.hs --- a/Bound/Scope.hs +++ b/Bound/Scope.hs @@ -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 #-} + diff --git a/Bound/Var.hs b/Bound/Var.hs --- a/Bound/Var.hs +++ b/Bound/Var.hs @@ -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 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.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\": - . - - . - 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. + 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 + + . + 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 + , 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: + . + + . + (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 + + . + 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