diff --git a/Bound.hs b/Bound.hs deleted file mode 100644 --- a/Bound.hs +++ /dev/null @@ -1,81 +0,0 @@ ------------------------------------------------------------------------------ --- | --- Module : Bound --- Copyright : (C) 2012 Edward Kmett --- License : BSD-style (see the file LICENSE) --- --- Maintainer : Edward Kmett --- 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 - ( - -- * 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 -import Bound.Class -import Bound.Scope -import Bound.Term diff --git a/Bound/Class.hs b/Bound/Class.hs deleted file mode 100644 --- a/Bound/Class.hs +++ /dev/null @@ -1,45 +0,0 @@ -{-# LANGUAGE CPP #-} -#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 704 -{-# LANGUAGE DefaultSignatures #-} -#endif ------------------------------------------------------------------------------ --- | --- Module : Bound.Class --- Copyright : (C) 2012 Edward Kmett --- License : BSD-style (see the file LICENSE) --- --- Maintainer : Edward Kmett --- Stability : experimental --- Portability : portable --- ----------------------------------------------------------------------------- -module Bound.Class - ( Bound(..) - , (=<<<) - ) where - -#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 704 -import Control.Monad.Trans.Class -#endif - -infixl 1 >>>= - --- | Instances may or may not be monad transformers. --- --- 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 --- contain one. - -class Bound t where - (>>>=) :: Monad f => t f a -> (a -> f c) -> t f c -#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 704 - default (>>>=) :: (MonadTrans t, Monad f, Monad (t f)) => - t f a -> (a -> f c) -> t f c - m >>>= f = m >>= lift . f -#endif - -infixr 1 =<<< -(=<<<) :: (Bound t, Monad f) => (a -> f c) -> t f a -> t f c -(=<<<) = flip (>>>=) diff --git a/Bound/Scope.hs b/Bound/Scope.hs deleted file mode 100644 --- a/Bound/Scope.hs +++ /dev/null @@ -1,284 +0,0 @@ ------------------------------------------------------------------------------ --- | --- Module : Bound.Scope --- Copyright : (C) 2012 Edward Kmett --- License : BSD-style (see the file LICENSE) --- --- Maintainer : Edward Kmett --- Stability : experimental --- Portability : portable --- ----------------------------------------------------------------------------- -module Bound.Scope - ( Scope(..) - -- * Abstraction - , abstract, abstract1 - -- * Instantiation - , instantiate, instantiate1 - -- * 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 Prelude.Extras -import Prelude hiding (foldr, mapM, mapM_) - --- | @'Scope' b f a@ is an @f@ expression with bound variables in @b@, --- and free variables in @a@ --- --- 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 and 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 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 - fmap f (Scope a) = Scope (fmap (fmap (fmap f)) a) - --- | @'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 - -instance Traversable f => Traversable (Scope b f) where - traverse f (Scope a) = Scope <$> traverse (traverse (traverse f)) a - --- | The monad permits substitution on free variables, while preserving --- bound variables -instance Monad f => Monad (Scope b f) where - return a = Scope (return (F (return a))) - Scope e >>= f = Scope $ e >>= \v -> case v of - B b -> return (B b) - F ea -> ea >>= unscope . f - -instance MonadTrans (Scope b) where - lift m = Scope (return (F m)) - -instance (Monad f, Eq b, Eq1 f, Eq a) => Eq (Scope b f a) where - (==) = (==#) -instance (Monad f, Eq b, Eq1 f) => Eq1 (Scope b f) where - a ==# b = liftM Lift2 (fromScope a) ==# liftM Lift2 (fromScope b) - -- a ==# b = mangleScope a ==# mangleScope b - -instance (Monad f, Ord b, Ord1 f, Ord a) => Ord (Scope b f a) where - compare = compare1 -instance (Monad f, Ord b, Ord1 f) => Ord1 (Scope b f) where - compare1 a b = liftM Lift2 (fromScope a) `compare1` liftM Lift2 (fromScope b) - -- compare1 a b = compare1 (mangleScope a) (mangleScope b) - -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 (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 - 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 - --- | 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 - Just z -> B z - Nothing -> F (return y) -{-# INLINE abstract #-} - --- | Enter a scope, instantiating all bound variables -instantiate :: Monad f => (b -> f a) -> Scope b f a -> f a -instantiate k e = unscope e >>= \v -> case v of - B b -> k b - F a -> a -{-# INLINE instantiate #-} - --- * Special purpose combinators - --- | Abstract over a single variable -abstract1 :: (Monad f, Eq a) => a -> f a -> Scope () f a -abstract1 a = abstract (\b -> if a == b then Just () else Nothing) -{-# INLINE abstract1 #-} - --- | 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 --- de Bruijn indexing scheme for bound variables. --- --- > fromScope . toScope = id --- > fromScope . toScope . fromScope = fromScope --- --- @('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 - B b -> return (B b) -{-# INLINE fromScope #-} - --- | Convert from traditional de Bruijn to generalized de Bruijn indices. --- --- This requires a full tree traversal -toScope :: Monad f => f (Var b a) -> Scope b f a -toScope e = Scope (liftM (fmap return) e) -{-# INLINE toScope #-} - --- | 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/Term.hs b/Bound/Term.hs deleted file mode 100644 --- a/Bound/Term.hs +++ /dev/null @@ -1,36 +0,0 @@ ------------------------------------------------------------------------------ --- | --- Module : Bound.Term --- Copyright : (C) 2012 Edward Kmett --- License : BSD-style (see the file LICENSE) --- --- Maintainer : Edward Kmett --- Stability : experimental --- Portability : portable --- ----------------------------------------------------------------------------- -module Bound.Term - ( substitute - , isClosed - , closed - ) where - -import Data.Foldable -import Data.Traversable -import Prelude hiding (all) - --- | @'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 #-} - --- | If a term has no free variables, you can freely change the type of --- free variables it is parameterized on. -closed :: Traversable f => f a -> Maybe (f b) -closed = traverse (const Nothing) -{-# INLINE closed #-} - --- | A closed term has no free variables. -isClosed :: Foldable f => f a -> Bool -isClosed = all (const False) -{-# INLINE isClosed #-} diff --git a/Bound/Var.hs b/Bound/Var.hs deleted file mode 100644 --- a/Bound/Var.hs +++ /dev/null @@ -1,78 +0,0 @@ ------------------------------------------------------------------------------ --- | --- Module : Bound.Var --- Copyright : (C) 2012 Edward Kmett --- License : BSD-style (see the file LICENSE) --- --- Maintainer : Edward Kmett --- Stability : experimental --- Portability : portable --- ----------------------------------------------------------------------------- -module Bound.Var - ( Var(..) - ) where - -import Data.Foldable -import Data.Traversable -import Data.Monoid (mempty) -import Data.Bifunctor -import Data.Bifoldable -import Data.Bitraversable -import Control.Applicative -import Control.Monad (ap) -import Prelude.Extras - --- | \"I am not a number, I am a /free monad/!\" --- --- A @Var b a@ is a variable that may either be \"bound\" or \"free\". --- --- (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 - deriving (Eq,Ord,Show,Read) - -instance Functor (Var b) where - fmap _ (B b) = B b - fmap f (F a) = F (f a) - -instance Foldable (Var b) where - foldMap f (F a) = f a - foldMap _ _ = mempty - -instance Traversable (Var b) where - traverse f (F a) = F <$> f a - traverse _ (B b) = pure (B b) - -instance Applicative (Var b) where - pure = F - (<*>) = ap - -instance Monad (Var b) where - return = F - F a >>= f = f a - B b >>= _ = B b - -instance Bifunctor Var where - bimap f _ (B b) = B (f b) - bimap _ g (F a) = F (g a) - -instance Bifoldable Var where - bifoldMap f _ (B b) = f b - bifoldMap _ g (F a) = g a - -instance Bitraversable Var where - bitraverse f _ (B b) = B <$> f b - bitraverse _ g (F a) = F <$> g a - -instance Eq2 Var where (==##) = (==) -instance Ord2 Var where compare2 = compare -instance Show2 Var where showsPrec2 = showsPrec -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 readsPrec1 = readsPrec diff --git a/bound.cabal b/bound.cabal --- a/bound.cabal +++ b/bound.cabal @@ -1,8 +1,8 @@ name: bound category: Language, Compilers/Interpreters -version: 0.2.1 +version: 0.3.1 license: BSD3 -cabal-version: >= 1.6 +cabal-version: >= 1.9.2 license-file: LICENSE author: Edward A. Kmett maintainer: Edward A. Kmett @@ -10,13 +10,13 @@ homepage: http://github.com/ekmett/bound/ bug-reports: http://github.com/ekmett/bound/issues copyright: Copyright (C) 2012 Edward A. Kmett -synopsis: Haskell 98 Locally-Nameless Generalized de Bruijn Terms +synopsis: Haskell 98/2010 Locally-Nameless Generalized de Bruijn Terms description: 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. + 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: . @@ -49,8 +49,8 @@ > 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'. + 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. @@ -60,7 +60,7 @@ 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 + The approach was first elaborated upon by Richard Bird and Ross Patterson in \"de Bruijn notation as a nested data type\", available from . @@ -69,26 +69,28 @@ 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. + 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 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 - + (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. + 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. + 3. /Overkill.hs/ provides very strongly typed pattern matching many modern + language 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: @@ -103,6 +105,7 @@ location: git://github.com/ekmett/bound.git library + hs-source-dirs: src build-depends: base >= 4 && < 5, bifunctors >= 0.1.3 && < 0.2, @@ -117,3 +120,13 @@ Bound.Var ghc-options: -Wall -O2 -fspec-constr -fdicts-cheap + +test-suite Simple + build-depends: + base >= 4 && < 5, + prelude-extras >= 0.2 && < 0.3, + transformers >= 0.2 && < 0.4, + bound + type: exitcode-stdio-1.0 + hs-source-dirs: examples + main-is: Simple.hs diff --git a/examples/Simple.hs b/examples/Simple.hs --- a/examples/Simple.hs +++ b/examples/Simple.hs @@ -1,4 +1,4 @@ -module Simple where +module Main where -- this is a simple example where lambdas only bind a single variable at a time -- this directly corresponds to the usual de bruijn presentation @@ -13,6 +13,7 @@ import Prelude hiding (foldr,abs) import Prelude.Extras import Bound +import System.Exit infixl 9 :@ @@ -171,3 +172,4 @@ else do putStrLn "Unexpected result:" pp result + exitFailure diff --git a/src/Bound.hs b/src/Bound.hs new file mode 100644 --- /dev/null +++ b/src/Bound.hs @@ -0,0 +1,75 @@ +----------------------------------------------------------------------------- +-- | +-- Module : Bound +-- Copyright : (C) 2012 Edward Kmett +-- License : BSD-style (see the file LICENSE) +-- +-- Maintainer : Edward Kmett +-- 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 +-- +-- More exotic combinators for manipulating a 'Scope' can be imported from +-- "Bound.Scope". +-- +---------------------------------------------------------------------------- +module Bound + ( + -- * Manipulating user terms + substitute + , isClosed + , closed + -- * Scopes introduce bound variables + , Scope(..) + -- ** Abstraction over bound variables + , abstract, abstract1 + -- ** Instantiation of bound variables + , instantiate, instantiate1 + -- * Structures permitting substitution + , Bound(..) + , (=<<<) + -- * Conversion to Traditional de Bruijn + , Var(..) + , fromScope + , toScope + ) where + +import Bound.Var +import Bound.Class +import Bound.Scope +import Bound.Term diff --git a/src/Bound/Class.hs b/src/Bound/Class.hs new file mode 100644 --- /dev/null +++ b/src/Bound/Class.hs @@ -0,0 +1,45 @@ +{-# LANGUAGE CPP #-} +#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 704 +{-# LANGUAGE DefaultSignatures #-} +#endif +----------------------------------------------------------------------------- +-- | +-- Module : Bound.Class +-- Copyright : (C) 2012 Edward Kmett +-- License : BSD-style (see the file LICENSE) +-- +-- Maintainer : Edward Kmett +-- Stability : experimental +-- Portability : portable +-- +---------------------------------------------------------------------------- +module Bound.Class + ( Bound(..) + , (=<<<) + ) where + +#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 704 +import Control.Monad.Trans.Class +#endif + +infixl 1 >>>= + +-- | Instances may or may not be monad transformers. +-- +-- 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 +-- contain one. + +class Bound t where + (>>>=) :: Monad f => t f a -> (a -> f c) -> t f c +#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 704 + default (>>>=) :: (MonadTrans t, Monad f, Monad (t f)) => + t f a -> (a -> f c) -> t f c + m >>>= f = m >>= lift . f +#endif + +infixr 1 =<<< +(=<<<) :: (Bound t, Monad f) => (a -> f c) -> t f a -> t f c +(=<<<) = flip (>>>=) diff --git a/src/Bound/Scope.hs b/src/Bound/Scope.hs new file mode 100644 --- /dev/null +++ b/src/Bound/Scope.hs @@ -0,0 +1,284 @@ +----------------------------------------------------------------------------- +-- | +-- Module : Bound.Scope +-- Copyright : (C) 2012 Edward Kmett +-- License : BSD-style (see the file LICENSE) +-- +-- Maintainer : Edward Kmett +-- Stability : experimental +-- Portability : portable +-- +---------------------------------------------------------------------------- +module Bound.Scope + ( Scope(..) + -- * Abstraction + , abstract, abstract1 + -- * Instantiation + , instantiate, instantiate1 + -- * 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 Prelude.Extras +import Prelude hiding (foldr, mapM, mapM_) + +-- | @'Scope' b f a@ is an @f@ expression with bound variables in @b@, +-- and free variables in @a@ +-- +-- 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 and 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 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 + fmap f (Scope a) = Scope (fmap (fmap (fmap f)) a) + +-- | @'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 + +instance Traversable f => Traversable (Scope b f) where + traverse f (Scope a) = Scope <$> traverse (traverse (traverse f)) a + +-- | The monad permits substitution on free variables, while preserving +-- bound variables +instance Monad f => Monad (Scope b f) where + return a = Scope (return (F (return a))) + Scope e >>= f = Scope $ e >>= \v -> case v of + B b -> return (B b) + F ea -> ea >>= unscope . f + +instance MonadTrans (Scope b) where + lift m = Scope (return (F m)) + +instance (Monad f, Eq b, Eq1 f, Eq a) => Eq (Scope b f a) where + (==) = (==#) +instance (Monad f, Eq b, Eq1 f) => Eq1 (Scope b f) where + a ==# b = liftM Lift2 (fromScope a) ==# liftM Lift2 (fromScope b) + -- a ==# b = mangleScope a ==# mangleScope b + +instance (Monad f, Ord b, Ord1 f, Ord a) => Ord (Scope b f a) where + compare = compare1 +instance (Monad f, Ord b, Ord1 f) => Ord1 (Scope b f) where + compare1 a b = liftM Lift2 (fromScope a) `compare1` liftM Lift2 (fromScope b) + -- compare1 a b = compare1 (mangleScope a) (mangleScope b) + +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 (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 + 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 + +-- | 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 + Just z -> B z + Nothing -> F (return y) +{-# INLINE abstract #-} + +-- | Enter a scope, instantiating all bound variables +instantiate :: Monad f => (b -> f a) -> Scope b f a -> f a +instantiate k e = unscope e >>= \v -> case v of + B b -> k b + F a -> a +{-# INLINE instantiate #-} + +-- * Special purpose combinators + +-- | Abstract over a single variable +abstract1 :: (Monad f, Eq a) => a -> f a -> Scope () f a +abstract1 a = abstract (\b -> if a == b then Just () else Nothing) +{-# INLINE abstract1 #-} + +-- | 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 +-- de Bruijn indexing scheme for bound variables. +-- +-- > fromScope . toScope = id +-- > fromScope . toScope . fromScope = fromScope +-- +-- @('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 + B b -> return (B b) +{-# INLINE fromScope #-} + +-- | Convert from traditional de Bruijn to generalized de Bruijn indices. +-- +-- This requires a full tree traversal +toScope :: Monad f => f (Var b a) -> Scope b f a +toScope e = Scope (liftM (fmap return) e) +{-# INLINE toScope #-} + +-- | 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/src/Bound/Term.hs b/src/Bound/Term.hs new file mode 100644 --- /dev/null +++ b/src/Bound/Term.hs @@ -0,0 +1,36 @@ +----------------------------------------------------------------------------- +-- | +-- Module : Bound.Term +-- Copyright : (C) 2012 Edward Kmett +-- License : BSD-style (see the file LICENSE) +-- +-- Maintainer : Edward Kmett +-- Stability : experimental +-- Portability : portable +-- +---------------------------------------------------------------------------- +module Bound.Term + ( substitute + , isClosed + , closed + ) where + +import Data.Foldable +import Data.Traversable +import Prelude hiding (all) + +-- | @'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 #-} + +-- | If a term has no free variables, you can freely change the type of +-- free variables it is parameterized on. +closed :: Traversable f => f a -> Maybe (f b) +closed = traverse (const Nothing) +{-# INLINE closed #-} + +-- | A closed term has no free variables. +isClosed :: Foldable f => f a -> Bool +isClosed = all (const False) +{-# INLINE isClosed #-} diff --git a/src/Bound/Var.hs b/src/Bound/Var.hs new file mode 100644 --- /dev/null +++ b/src/Bound/Var.hs @@ -0,0 +1,78 @@ +----------------------------------------------------------------------------- +-- | +-- Module : Bound.Var +-- Copyright : (C) 2012 Edward Kmett +-- License : BSD-style (see the file LICENSE) +-- +-- Maintainer : Edward Kmett +-- Stability : experimental +-- Portability : portable +-- +---------------------------------------------------------------------------- +module Bound.Var + ( Var(..) + ) where + +import Data.Foldable +import Data.Traversable +import Data.Monoid (mempty) +import Data.Bifunctor +import Data.Bifoldable +import Data.Bitraversable +import Control.Applicative +import Control.Monad (ap) +import Prelude.Extras + +-- | \"I am not a number, I am a /free monad/!\" +-- +-- A @Var b a@ is a variable that may either be \"bound\" or \"free\". +-- +-- (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 + deriving (Eq,Ord,Show,Read) + +instance Functor (Var b) where + fmap _ (B b) = B b + fmap f (F a) = F (f a) + +instance Foldable (Var b) where + foldMap f (F a) = f a + foldMap _ _ = mempty + +instance Traversable (Var b) where + traverse f (F a) = F <$> f a + traverse _ (B b) = pure (B b) + +instance Applicative (Var b) where + pure = F + (<*>) = ap + +instance Monad (Var b) where + return = F + F a >>= f = f a + B b >>= _ = B b + +instance Bifunctor Var where + bimap f _ (B b) = B (f b) + bimap _ g (F a) = F (g a) + +instance Bifoldable Var where + bifoldMap f _ (B b) = f b + bifoldMap _ g (F a) = g a + +instance Bitraversable Var where + bitraverse f _ (B b) = B <$> f b + bitraverse _ g (F a) = F <$> g a + +instance Eq2 Var where (==##) = (==) +instance Ord2 Var where compare2 = compare +instance Show2 Var where showsPrec2 = showsPrec +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 readsPrec1 = readsPrec