Permalink
Browse files

more doctests and documentation

  • Loading branch information...
1 parent 24ae1f9 commit c235b48e78fccabc3719d20ab513b68c917df191 @ekmett committed Sep 13, 2012
Showing with 103 additions and 40 deletions.
  1. +4 −0 bound.cabal
  2. +41 −24 src/Bound.hs
  3. +16 −4 src/Bound/Class.hs
  4. +13 −8 src/Bound/Scope.hs
  5. +23 −1 src/Bound/Term.hs
  6. +2 −2 src/Bound/Var.hs
  7. +4 −1 tests/doctests.hs
View
@@ -21,6 +21,10 @@ description:
An untyped lambda calculus:
.
> import Bound
+ > import Control.Applicative
+ > import Control.Monad (ap)
+ > import Data.Foldable
+ > import Data.Traversable
> import Prelude.Extras
.
> infixl 9 :@
View
@@ -9,40 +9,57 @@
-- 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
+-- 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
+-- @
+-- {-\# LANGUAGE DeriveFunctor, DeriveFoldable, DeriveTraversable \#-}
+-- import Bound
+-- import Control.Applicative
+-- import Control.Monad ('Control.Monad.ap')
+-- import Prelude.Extras
+-- import Data.Foldable
+-- import Data.Traverable
+-- @
--
--- > infixl 9 :@
--- > data Exp a = V a | Exp a :@ Exp a | Lam (Scope () Exp a)
--- > deriving (Eq,Ord,Show,Read,Functor,Foldable,Traversable)
+-- @
+-- infixl 9 :\@
+-- data Exp a = V a | Exp a :\@ Exp a | Lam ('Scope' () Exp a)
+-- deriving ('Eq','Ord','Show','Read','Functor','Data.Foldable.Foldable','Data.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 'Prelude.Extras.Eq1' Exp where ('Prelude.Extras.==#') = ('==')
+-- instance 'Prelude.Extras.Ord1' Exp where 'Prelude.Extras.compare1' = 'compare'
+-- instance 'Prelude.Extras.Show1' Exp where 'Prelude.Extras.showsPrec1' = 'showsPrec'
+-- instance 'Prelude.Extras.Read1' Exp where 'Prelude.Extras.readsPrec1' = 'readsPrec'
+-- instance 'Control.Applicative.Applicative' Exp where 'Control.Applicative.pure' = V; ('<*>') = 'Control.Monad.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)
+-- @
+-- instance 'Monad' Exp where
+-- 'return' = V
+-- V a '>>=' f = f a
+-- (x :\@ y) '>>=' f = (x '>>=' f) :\@ (y >>= f)
+-- Lam e '>>=' f = Lam (e '>>>=' f)
+-- @
--
--- > whnf :: Exp a -> Exp a
--- > whnf (f :@ a) = case whnf f of
--- > Lam b -> whnf (instantiate1 a b)
--- > f' -> f' :@ a
--- > whnf e = e
+-- @
+-- 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".
View
@@ -12,6 +12,8 @@
-- Stability : experimental
-- Portability : portable
--
+-- This module provides the 'Bound' class, for performing substitution into
+-- things that are not necessarily full monad transformers.
----------------------------------------------------------------------------
module Bound.Class
( Bound(..)
@@ -24,15 +26,22 @@ import Control.Monad.Trans.Class
infixl 1 >>>=
--- | Instances may or may not be monad transformers.
+-- | Instances of 'Bound' may or may not be monad transformers.
--
--- If they are, then you can use @m >>>= f = m >>= lift . f@
+-- If they are, then @m '>>>=' f ≡ m '>>=' 'lift' '.' f@ is required to hold, and is
+-- in fact the default definition. If it is not a 'MonadTrans' instance, then
+-- you have greater flexibility in how to implement this class.
--
-- 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.
-
+-- contain expressions.
class Bound t where
+ -- | Perform substitution
+ --
+ -- If @t@ is an instance of @MonadTrans@ and you are compiling on GHC >= 7.4, then this
+ -- gets the default definition:
+ --
+ -- @m '>>>=' f = m '>>=' 'lift' '.' f@
(>>>=) :: 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)) =>
@@ -41,5 +50,8 @@ class Bound t where
#endif
infixr 1 =<<<
+-- | A flipped version of ('>>>=').
+--
+-- @('=<<<') = 'flip' ('>>>=')@
(=<<<) :: (Bound t, Monad f) => (a -> f c) -> t f a -> t f c
(=<<<) = flip (>>>=)
View
@@ -8,6 +8,10 @@
-- Stability : experimental
-- Portability : portable
--
+-- This is the work-horse of the @bound@ library.
+--
+-- 'Scope' provides a single generalized de Bruijn level
+-- and is often used inside of the definition of binders.
----------------------------------------------------------------------------
module Bound.Scope
( Scope(..)
@@ -171,21 +175,21 @@ 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'
+-- | 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
+-- | 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
+-- | 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)
@@ -226,14 +230,15 @@ foldMapScope :: (Foldable f, Monoid r) =>
foldMapScope f g (Scope s) = foldMap (bifoldMap f (foldMap g)) s
{-# INLINE foldMapScope #-}
+-- | 'traverse_' the bound variables in a 'Scope'.
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.
+-- | '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
@@ -253,29 +258,29 @@ mapMScope_ :: (Monad m, Foldable f) =>
mapMScope_ f g (Scope s) = mapM_ (bimapM_ f (mapM_ g)) s
{-# INLINE mapMScope_ #-}
---- | Traverse both bound and free variables
+-- | 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
+-- | 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
+-- | 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'
+-- | 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)
View
@@ -20,22 +20,44 @@ import Data.Foldable
import Data.Traversable
import Prelude hiding (all)
--- | @'substitute' a p w@ replaces the free variable @a@ with @p@ in @w@
+-- | @'substitute' a p w@ replaces the free variable @a@ with @p@ in @w@.
+--
+-- >>> substitute "hello" ["goodnight","Gracie"] ["hello","!!!"]
+-- ["goodnight","Gracie","!!!"]
substitute :: (Monad f, Eq a) => a -> f a -> f a -> f a
substitute a p w = w >>= \b -> if a == b then p else return b
{-# INLINE substitute #-}
+-- | @'substituteVar' a b w@ replaces a free variable @a@ with another free variable @b@ in @w@.
+--
+-- >>> substitute "Alice" "Bob" ["Alice","Bob","Charlie"]
+-- ["Bob","Bob","Charlie"]
substituteVar :: (Functor f, Eq a) => a -> a -> f a -> f a
substituteVar a p = fmap (\b -> if a == b then p else b)
{-# INLINE substituteVar #-}
-- | If a term has no free variables, you can freely change the type of
-- free variables it is parameterized on.
+--
+-- >>> closed [12]
+-- Nothing
+--
+-- >>> closed ""
+-- Just []
+--
+-- >>> :t closed ""
+-- closed "" :: Maybe [b]
closed :: Traversable f => f a -> Maybe (f b)
closed = traverse (const Nothing)
{-# INLINE closed #-}
-- | A closed term has no free variables.
+--
+-- >>> isClosed []
+-- True
+--
+-- >>> isClosed [1,2,3]
+-- False
isClosed :: Foldable f => f a -> Bool
isClosed = all (const False)
{-# INLINE isClosed #-}
View
@@ -25,9 +25,9 @@ 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\".
+-- A @'Var' b a@ is a variable that may either be \"bound\" ('B') or \"free\" ('F').
--
--- (It is also technically a free monad in the same near trivial sense as
+-- (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
View
@@ -17,7 +17,10 @@ main = getSources >>= \sources -> doctest $
: sources
getSources :: IO [FilePath]
-getSources = filter (isSuffixOf ".hs") <$> go "examples"
+getSources = do
+ examples <- go "examples"
+ src <- go "src"
+ return $ filter (isSuffixOf ".hs") (examples ++ src)
where
go dir = do
(dirs, files) <- getFilesAndDirectories dir

0 comments on commit c235b48

Please sign in to comment.