Permalink
Browse files

repository initialized

  • Loading branch information...
0 parents commit e32e40a5b45f784f89eddd0c44cc730e0d7f06eb @ekmett committed Jun 14, 2012
Showing with 312 additions and 0 deletions.
  1. +1 −0 .gitignore
  2. +1 −0 .travis.yml
  3. +9 −0 Bound.hs
  4. +22 −0 Bound/Class.hs
  5. +136 −0 Bound/Scope.hs
  6. +71 −0 Bound/Var.hs
  7. +30 −0 LICENSE
  8. +7 −0 Setup.lhs
  9. +35 −0 bound.cabal
@@ -0,0 +1 @@
+dist
@@ -0,0 +1 @@
+language: haskell
@@ -0,0 +1,9 @@
+module Bound
+ ( module Bound.Var
+ , module Bound.Class
+ , module Bound.Scope
+ ) where
+
+import Bound.Var
+import Bound.Class
+import Bound.Scope
@@ -0,0 +1,22 @@
+-----------------------------------------------------------------------------
+-- |
+-- 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
+
+infixl 1 >>>=
+class Bound t where
+ (>>>=) :: Monad f => t f a -> (a -> f c) -> t f c
+
+infixr 1 =<<<
+(=<<<) :: (Bound t, Monad f) => (a -> f c) -> t f a -> t f c
+(=<<<) = flip (>>>=)
@@ -0,0 +1,136 @@
+-----------------------------------------------------------------------------
+-- |
+-- 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
+ -- * Substitution
+ , substitute
+ -- * Quotienting
+ , fromScope
+ , toScope
+ ) where
+
+import Data.Foldable
+import Data.Traversable
+import Control.Monad
+import Control.Monad.Trans.Class
+import Control.Applicative
+import Prelude.Extras
+import Bound.Class
+import Bound.Var
+import Text.Read hiding (lift)
+
+-- | @Scope b f a@ is a an f expression with bound variables b, and free variables a
+--
+-- This stores bound variables as their generalized deBruijn 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.
+
+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)
+
+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 (Free (return a)))
+ Scope e >>= f = Scope $ e >>= \v -> case v of
+ Bound b -> return (Bound b)
+ Free ea -> ea >>= unscope . f
+
+instance MonadTrans (Scope b) where
+ lift m = Scope (return (Free m))
+
+mangleScope :: Functor f => Scope b f a -> Lift1 f (Lift2 Var b (Lift1 f a))
+mangleScope (Scope a) = Lift1 (fmap (Lift2 . fmap Lift1) a)
+{-# INLINE mangleScope #-}
+
+unmangleScope :: Functor f => Lift1 f (Lift2 Var b (Lift1 f a)) -> Scope b f a
+unmangleScope (Lift1 a) = Scope (fmap (fmap lower1 . lower2) a)
+{-# INLINE unmangleScope #-}
+
+instance (Functor f, Eq b, Eq1 f, Eq a) => Eq (Scope b f a) where
+ a == b = mangleScope a == mangleScope b
+
+instance (Functor f, Ord b, Ord1 f, Ord a) => Ord (Scope b f a) where
+ compare a b = compare (mangleScope a) (mangleScope b)
+
+instance (Functor f, Show b, Show1 f, Show a) => Show (Scope b f a) where
+ showsPrec d a = showsPrec d (mangleScope a)
+
+instance (Functor f, Read b, Read1 f, Read a) => Read (Scope b f a) where
+ readPrec = liftM unmangleScope readPrec
+
+instance Bound (Scope b) where
+ m >>>= f = m >>= lift . f
+
+-- | capture some free variables in an expression to yield a Scope with bound variables
+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 -> Bound z
+ Nothing -> Free (return y)
+{-# INLINE abstract #-}
+
+-- | 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, 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
+ Bound b -> k b
+ Free a -> a
+{-# INLINE instantiate #-}
+
+-- | enter a scope with one bound variable, instantiating it
+instantiate1 :: Monad f => f a -> Scope () f a -> f a
+instantiate1 e = instantiate (\ () -> e)
+{-# INLINE instantiate1 #-}
+
+-- | @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 #-}
+
+-- | @fromScope@ quotients out the various placements of Free in Scope
+-- distributing them all to the leaves. This yields a traditional deBruijn
+-- 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
+ Free e -> liftM Free e
+ Bound b -> return (Bound b)
+{-# INLINE fromScope #-}
+
+toScope :: Monad f => f (Var b a) -> Scope b f a
+toScope e = Scope (liftM (fmap return) e)
+{-# INLINE toScope #-}
+
+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
+ Bound b -> unbind b
+ Free ea -> ea >>= f
@@ -0,0 +1,71 @@
+-----------------------------------------------------------------------------
+-- |
+-- 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
+import Text.Read
+
+data Var b a
+ = Bound b
+ | Free a
+ deriving (Eq,Ord,Show,Read)
+
+instance Functor (Var b) where
+ fmap _ (Bound b) = Bound b
+ fmap f (Free a) = Free (f a)
+
+instance Foldable (Var b) where
+ foldMap f (Free a) = f a
+ foldMap _ _ = mempty
+
+instance Traversable (Var b) where
+ traverse f (Free a) = Free <$> f a
+ traverse _ (Bound b) = pure (Bound b)
+
+instance Applicative (Var b) where
+ pure = Free
+ (<*>) = ap
+
+instance Monad (Var b) where
+ return = Free
+ Free a >>= f = f a
+ Bound b >>= _ = Bound b
+
+instance Bifunctor Var where
+ bimap f _ (Bound b) = Bound (f b)
+ bimap _ g (Free a) = Free (g a)
+
+instance Bifoldable Var where
+ bifoldMap f _ (Bound b) = f b
+ bifoldMap _ g (Free a) = g a
+
+instance Bitraversable Var where
+ bitraverse f _ (Bound b) = Bound <$> f b
+ bitraverse _ g (Free a) = Free <$> g a
+
+instance Eq2 Var where (==##) = (==)
+instance Ord2 Var where compare2 = compare
+instance Show2 Var where showsPrec2 = showsPrec
+instance Read2 Var where readPrec2 = readPrec
+
+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
30 LICENSE
@@ -0,0 +1,30 @@
+Copyright 2012 Edward Kmett
+
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions
+are met:
+
+1. Redistributions of source code must retain the above copyright
+ notice, this list of conditions and the following disclaimer.
+
+2. Redistributions in binary form must reproduce the above copyright
+ notice, this list of conditions and the following disclaimer in the
+ documentation and/or other materials provided with the distribution.
+
+3. Neither the name of the author nor the names of his contributors
+ may be used to endorse or promote products derived from this software
+ without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE AUTHORS ``AS IS'' AND ANY EXPRESS OR
+IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED
+WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
+DISCLAIMED. IN NO EVENT SHALL THE AUTHORS OR CONTRIBUTORS BE LIABLE FOR
+ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
+DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS
+OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION)
+HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT,
+STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
+ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
+POSSIBILITY OF SUCH DAMAGE.
@@ -0,0 +1,7 @@
+#!/usr/bin/runhaskell
+> module Main (main) where
+
+> import Distribution.Simple
+
+> main :: IO ()
+> main = defaultMain
@@ -0,0 +1,35 @@
+name: bound
+category: Language, Compilers/Interpreters
+version: 0.1
+license: BSD3
+cabal-version: >= 1.6
+license-file: LICENSE
+author: Edward A. Kmett
+maintainer: Edward A. Kmett <ekmett@gmail.com>
+stability: experimental
+homepage: http://github.com/ekmett/bound/
+bug-reports: http://github.com/ekmett/bound/issues
+copyright: Copyright (C) 2012 Edward A. Kmett
+synopsis: Simple combinators for working with locally-nameless generalized de Bruijn terms in Haskell 98
+description: "I am not a number, I am a free monad!"
+build-type: Simple
+extra-source-files: .travis.yml
+
+source-repository head
+ type: git
+ location: git://github.com/ekmett/bound.git
+
+library
+ build-depends:
+ base >= 4 && < 5,
+ bifunctors >= 0.1.3 && < 0.2,
+ prelude-extras >= 0.2 && < 0.3,
+ transformers >= 0.2 && < 0.4
+
+ exposed-modules:
+ Bound
+ Bound.Class
+ Bound.Var
+ Bound.Scope
+
+ ghc-options: -Wall

0 comments on commit e32e40a

Please sign in to comment.