bound 0.2.1 → 0.3.1

raw patch · 12 files changed

+556/−547 lines, 12 filesdep +boundPVP ok

version bump matches the API change (PVP)

Dependencies added: bound

API changes (from Hackage documentation)

Files

• Bound.hs +0/−81
• Bound/Class.hs +0/−45
• Bound/Scope.hs +0/−284
• Bound/Term.hs +0/−36
• Bound/Var.hs +0/−78
• bound.cabal +35/−22
• examples/Simple.hs +3/−1
• src/Bound.hs +75/−0
• src/Bound/Class.hs +45/−0
• src/Bound/Scope.hs +284/−0
• src/Bound/Term.hs +36/−0
• src/Bound/Var.hs +78/−0

@@ -1,81 +0,0 @@--------------------------------------------------------------------------------- |--- Module      :  Bound--- Copyright   :  (C) 2012 Edward Kmett--- License     :  BSD-style (see the file LICENSE)------ Maintainer  :  Edward Kmett <ekmett@gmail.com>--- 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

@@ -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 <ekmett@gmail.com>--- 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 (>>>=)

@@ -1,284 +0,0 @@--------------------------------------------------------------------------------- |--- Module      :  Bound.Scope--- Copyright   :  (C) 2012 Edward Kmett--- License     :  BSD-style (see the file LICENSE)------ Maintainer  :  Edward Kmett <ekmett@gmail.com>--- 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 #-}-

@@ -1,36 +0,0 @@--------------------------------------------------------------------------------- |--- Module      :  Bound.Term--- Copyright   :  (C) 2012 Edward Kmett--- License     :  BSD-style (see the file LICENSE)------ Maintainer  :  Edward Kmett <ekmett@gmail.com>--- 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 #-}

@@ -1,78 +0,0 @@--------------------------------------------------------------------------------- |--- Module      :  Bound.Var--- Copyright   :  (C) 2012 Edward Kmett--- License     :  BSD-style (see the file LICENSE)------ Maintainer  :  Edward Kmett <ekmett@gmail.com>--- 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

@@ -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 <ekmett@gmail.com>@@ -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    <http://www.cs.uwyo.edu/~jlc/courses/5000_fall_08/debruijn_as_nested_datatype.pdf>    .@@ -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-   <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.+   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 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>+   (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.+   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

@@ -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

@@ -0,0 +1,75 @@+-----------------------------------------------------------------------------+-- |+-- Module      :  Bound+-- Copyright   :  (C) 2012 Edward Kmett+-- License     :  BSD-style (see the file LICENSE)+--+-- Maintainer  :  Edward Kmett <ekmett@gmail.com>+-- 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

@@ -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 <ekmett@gmail.com>+-- 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 (>>>=)

@@ -0,0 +1,284 @@+-----------------------------------------------------------------------------+-- |+-- Module      :  Bound.Scope+-- Copyright   :  (C) 2012 Edward Kmett+-- License     :  BSD-style (see the file LICENSE)+--+-- Maintainer  :  Edward Kmett <ekmett@gmail.com>+-- 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 #-}+

@@ -0,0 +1,36 @@+-----------------------------------------------------------------------------+-- |+-- Module      :  Bound.Term+-- Copyright   :  (C) 2012 Edward Kmett+-- License     :  BSD-style (see the file LICENSE)+--+-- Maintainer  :  Edward Kmett <ekmett@gmail.com>+-- 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 #-}

@@ -0,0 +1,78 @@+-----------------------------------------------------------------------------+-- |+-- Module      :  Bound.Var+-- Copyright   :  (C) 2012 Edward Kmett+-- License     :  BSD-style (see the file LICENSE)+--+-- Maintainer  :  Edward Kmett <ekmett@gmail.com>+-- 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