Bound

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:

{-# LANGUAGE DeriveFunctor, DeriveFoldable, DeriveTraversable, TemplateHaskell #-}
import Bound
import Control.Applicative
import Control.Monad (ap)
import Data.Functor.Classes
import Data.Foldable
import Data.Traversable
-- This is from deriving-compat package
import Data.Deriving (deriveEq1, deriveOrd1, deriveRead1, deriveShow1) 

infixl 9 :@
data Exp a = V a | Exp a :@ Exp a | Lam (Scope () Exp a)
  deriving (Functor,Foldable,Traversable)

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)

deriveEq1   ''Exp
deriveOrd1  ''Exp
deriveRead1 ''Exp
deriveShow1 ''Exp

instance Eq a   => Eq   (Exp a) where (==) = eq1
instance Ord a  => Ord  (Exp a) where compare = compare1
instance Show a => Show (Exp a) where showsPrec = showsPrec1
instance Read a => Read (Exp a) where readsPrec = readsPrec1

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.

You can also retain names in your bound variables by using Name and the related combinators from Bound.Name. They are not re-exported from this module by default.

The approach used in this package 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

However, the combinators they used required higher rank types. Here we demonstrate that the higher rank gfold combinator they used isn't necessary to build the monad and use a monad transformer to encapsulate the novel recursion pattern in their generalized de Bruijn representation. It is named Scope to match up with the terminology and usage pattern from Conor McBride and James McKinna's "I am not a number: I am a free variable", available from http://www.cs.ru.nl/~james/RESEARCH/haskell2004.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://foswiki.cs.uu.nl/foswiki/pub/USCS/InterestingPapers/AugustsonLambdaCalculus.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.
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.

Manipulating user terms

substitute :: (Monad f, Eq a) => a -> f a -> f a -> f a

substitute a p w replaces the free variable a with p in w.

>>> substitute "hello" ["goodnight","Gracie"] ["hello","!!!"]
["goodnight","Gracie","!!!"]

isClosed :: Foldable f => f a -> Bool

A closed term has no free variables.

>>> isClosed []
True

>>> isClosed [1,2,3]
False

closed :: Traversable f => f a -> Maybe (f b)

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]

Scopes introduce bound variables

newtype Scope b f a

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.

Constructors

Scope

Fields

• unscope :: f (Var b (f a))

Instances

MonadTrans (Scope b)

Defined in Bound.Scope

Methods

lift :: Monad m => m a -> Scope b m a

Bound (Scope b)

Defined in Bound.Scope

Methods

(>>>=) :: Monad f => Scope b f a -> (a -> f c) -> Scope b f c

MFunctor (Scope b :: (Type -> Type) -> Type -> Type)

Defined in Bound.Scope

Methods

hoist :: forall m n (b0 :: k). Monad m => (forall a. m a -> n a) -> Scope b m b0 -> Scope b n b0

Functor f => Generic1 (Scope b f :: Type -> Type)

Defined in Bound.Scope

Associated Types

type Rep1 (Scope b f) :: k -> Type

Methods

from1 :: forall (a :: k). Scope b f a -> Rep1 (Scope b f) a

to1 :: forall (a :: k). Rep1 (Scope b f) a -> Scope b f a

Monad f => Monad (Scope b f)

The monad permits substitution on free variables, while preserving bound variables

Defined in Bound.Scope

Methods

(>>=) :: Scope b f a -> (a -> Scope b f b0) -> Scope b f b0

(>>) :: Scope b f a -> Scope b f b0 -> Scope b f b0

return :: a -> Scope b f a

Functor f => Functor (Scope b f)

Defined in Bound.Scope

Methods

fmap :: (a -> b0) -> Scope b f a -> Scope b f b0

(<$) :: a -> Scope b f b0 -> Scope b f a

(Functor f, Monad f) => Applicative (Scope b f)

Defined in Bound.Scope

Methods

pure :: a -> Scope b f a

(<*>) :: Scope b f (a -> b0) -> Scope b f a -> Scope b f b0

liftA2 :: (a -> b0 -> c) -> Scope b f a -> Scope b f b0 -> Scope b f c

(*>) :: Scope b f a -> Scope b f b0 -> Scope b f b0

(<*) :: Scope b f a -> Scope b f b0 -> Scope b f a

Foldable f => Foldable (Scope b f)

toList is provides a list (with duplicates) of the free variables

Defined in Bound.Scope

Methods

fold :: Monoid m => Scope b f m -> m

foldMap :: Monoid m => (a -> m) -> Scope b f a -> m

foldMap' :: Monoid m => (a -> m) -> Scope b f a -> m

foldr :: (a -> b0 -> b0) -> b0 -> Scope b f a -> b0

foldr' :: (a -> b0 -> b0) -> b0 -> Scope b f a -> b0

foldl :: (b0 -> a -> b0) -> b0 -> Scope b f a -> b0

foldl' :: (b0 -> a -> b0) -> b0 -> Scope b f a -> b0

foldr1 :: (a -> a -> a) -> Scope b f a -> a

foldl1 :: (a -> a -> a) -> Scope b f a -> a

toList :: Scope b f a -> [a]

null :: Scope b f a -> Bool

length :: Scope b f a -> Int

elem :: Eq a => a -> Scope b f a -> Bool

maximum :: Ord a => Scope b f a -> a

minimum :: Ord a => Scope b f a -> a

sum :: Num a => Scope b f a -> a

product :: Num a => Scope b f a -> a

Traversable f => Traversable (Scope b f)

Defined in Bound.Scope

Methods

traverse :: Applicative f0 => (a -> f0 b0) -> Scope b f a -> f0 (Scope b f b0)

sequenceA :: Applicative f0 => Scope b f (f0 a) -> f0 (Scope b f a)

mapM :: Monad m => (a -> m b0) -> Scope b f a -> m (Scope b f b0)

sequence :: Monad m => Scope b f (m a) -> m (Scope b f a)

(Monad f, Eq b, Eq1 f) => Eq1 (Scope b f)

Defined in Bound.Scope

Methods

liftEq :: (a -> b0 -> Bool) -> Scope b f a -> Scope b f b0 -> Bool

(Monad f, Ord b, Ord1 f) => Ord1 (Scope b f)

Defined in Bound.Scope

Methods

liftCompare :: (a -> b0 -> Ordering) -> Scope b f a -> Scope b f b0 -> Ordering

(Read b, Read1 f) => Read1 (Scope b f)

Defined in Bound.Scope

Methods

liftReadsPrec :: (Int -> ReadS a) -> ReadS [a] -> Int -> ReadS (Scope b f a)

liftReadList :: (Int -> ReadS a) -> ReadS [a] -> ReadS [Scope b f a]

liftReadPrec :: ReadPrec a -> ReadPrec [a] -> ReadPrec (Scope b f a)

liftReadListPrec :: ReadPrec a -> ReadPrec [a] -> ReadPrec [Scope b f a]

(Show b, Show1 f) => Show1 (Scope b f)

Defined in Bound.Scope

Methods

liftShowsPrec :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> Scope b f a -> ShowS

liftShowList :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> [Scope b f a] -> ShowS

(Serial b, Serial1 f) => Serial1 (Scope b f)

Defined in Bound.Scope

Methods

serializeWith :: MonadPut m => (a -> m ()) -> Scope b f a -> m ()

deserializeWith :: MonadGet m => m a -> m (Scope b f a)

(Hashable b, Monad f, Hashable1 f) => Hashable1 (Scope b f)

Defined in Bound.Scope

Methods

liftHashWithSalt :: (Int -> a -> Int) -> Int -> Scope b f a -> Int

(Monad f, Eq b, Eq1 f, Eq a) => Eq (Scope b f a)

Defined in Bound.Scope

Methods

(==) :: Scope b f a -> Scope b f a -> Bool

(/=) :: Scope b f a -> Scope b f a -> Bool

(Typeable b, Typeable f, Data a, Data (f (Var b (f a)))) => Data (Scope b f a)

Defined in Bound.Scope

Methods

gfoldl :: (forall d b0. Data d => c (d -> b0) -> d -> c b0) -> (forall g. g -> c g) -> Scope b f a -> c (Scope b f a)

gunfold :: (forall b0 r. Data b0 => c (b0 -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Scope b f a)

toConstr :: Scope b f a -> Constr

dataTypeOf :: Scope b f a -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Scope b f a))

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Scope b f a))

gmapT :: (forall b0. Data b0 => b0 -> b0) -> Scope b f a -> Scope b f a

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Scope b f a -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Scope b f a -> r

gmapQ :: (forall d. Data d => d -> u) -> Scope b f a -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Scope b f a -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Scope b f a -> m (Scope b f a)

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Scope b f a -> m (Scope b f a)

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Scope b f a -> m (Scope b f a)

(Monad f, Ord b, Ord1 f, Ord a) => Ord (Scope b f a)

Defined in Bound.Scope

Methods

compare :: Scope b f a -> Scope b f a -> Ordering

(<) :: Scope b f a -> Scope b f a -> Bool

(<=) :: Scope b f a -> Scope b f a -> Bool

(>) :: Scope b f a -> Scope b f a -> Bool

(>=) :: Scope b f a -> Scope b f a -> Bool

max :: Scope b f a -> Scope b f a -> Scope b f a

min :: Scope b f a -> Scope b f a -> Scope b f a

(Read b, Read1 f, Read a) => Read (Scope b f a)

Defined in Bound.Scope

Methods

readsPrec :: Int -> ReadS (Scope b f a)

readList :: ReadS [Scope b f a]

readPrec :: ReadPrec (Scope b f a)

readListPrec :: ReadPrec [Scope b f a]

(Show b, Show1 f, Show a) => Show (Scope b f a)

Defined in Bound.Scope

Methods

showsPrec :: Int -> Scope b f a -> ShowS

show :: Scope b f a -> String

showList :: [Scope b f a] -> ShowS

Generic (Scope b f a)

Defined in Bound.Scope

Associated Types

type Rep (Scope b f a) :: Type -> Type

Methods

from :: Scope b f a -> Rep (Scope b f a) x

to :: Rep (Scope b f a) x -> Scope b f a

(Binary b, Serial1 f, Binary a) => Binary (Scope b f a)

Defined in Bound.Scope

Methods

put :: Scope b f a -> Put

get :: Get (Scope b f a)

putList :: [Scope b f a] -> Put

(Serial b, Serial1 f, Serial a) => Serial (Scope b f a)

Defined in Bound.Scope

Methods

serialize :: MonadPut m => Scope b f a -> m ()

deserialize :: MonadGet m => m (Scope b f a)

(Serialize b, Serial1 f, Serialize a) => Serialize (Scope b f a)

Defined in Bound.Scope

Methods

put :: Putter (Scope b f a)

get :: Get (Scope b f a)

NFData (f (Var b (f a))) => NFData (Scope b f a)

Defined in Bound.Scope

Methods

rnf :: Scope b f a -> ()

(Hashable b, Monad f, Hashable1 f, Hashable a) => Hashable (Scope b f a)

Defined in Bound.Scope

Methods

hashWithSalt :: Int -> Scope b f a -> Int

hash :: Scope b f a -> Int

type Rep1 (Scope b f :: Type -> Type)

Defined in Bound.Scope

type Rep1 (Scope b f :: Type -> Type) = D1 ('MetaData "Scope" "Bound.Scope" "bound-2.0.3-IMm1RxjoHWu6bB6DEZNDCu" 'True) (C1 ('MetaCons "Scope" 'PrefixI 'True) (S1 ('MetaSel ('Just "unscope") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (f :.: (Var b :.: Rec1 f))))

type Rep (Scope b f a)

Defined in Bound.Scope

type Rep (Scope b f a) = D1 ('MetaData "Scope" "Bound.Scope" "bound-2.0.3-IMm1RxjoHWu6bB6DEZNDCu" 'True) (C1 ('MetaCons "Scope" 'PrefixI 'True) (S1 ('MetaSel ('Just "unscope") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (f (Var b (f a))))))

Abstraction over bound variables

abstract :: Monad f => (a -> Maybe b) -> f a -> Scope b f a

Capture some free variables in an expression to yield a Scope with bound variables in b

>>> :m + Data.List
>>> abstract (`elemIndex` "bar") "barry"
Scope [B 0,B 1,B 2,B 2,F "y"]

abstract1 :: (Monad f, Eq a) => a -> f a -> Scope () f a

Abstract over a single variable

>>> abstract1 'x' "xyz"
Scope [B (),F "y",F "z"]

Instantiation of bound variables

instantiate :: Monad f => (b -> f a) -> Scope b f a -> f a

Enter a scope, instantiating all bound variables

>>> :m + Data.List
>>> instantiate (\x -> [toEnum (97 + x)]) $ abstract (`elemIndex` "bar") "barry"
"abccy"

instantiate1 :: Monad f => f a -> Scope n f a -> f a

Enter a Scope that binds one variable, instantiating it

>>> instantiate1 "x" $ Scope [B (),F "y",F "z"]
"xyz"

Structures permitting substitution

class Bound t where

Instances of Bound generate left modules over monads.

This means they should satisfy the following laws:

m >>>= return ≡ m
m >>>= (λ x → k x >>= h) ≡ (m >>>= k) >>>= h

This guarantees that a typical Monad instance for an expression type where Bound instances appear will satisfy the Monad laws (see doc/BoundLaws.hs).

If instances of Bound are monad transformers, then m >>>= f ≡ m >>= lift . f implies the above laws, and is in fact the default definition.

This is useful for types like expression lists, case alternatives, schemas, etc. that may not be expressions in their own right, but often contain expressions.

Note: Free isn't "really" a monad transformer, even if the kind matches. Therefore there isn't Bound Free instance.

Minimal complete definition

Nothing

Methods

(>>>=) :: Monad f => t f a -> (a -> f c) -> t f c infixl 1

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

default (>>>=) :: (MonadTrans t, Monad f, Monad (t f)) => t f a -> (a -> f c) -> t f c

Instances

Bound ListT

Defined in Bound.Class

Methods

(>>>=) :: Monad f => ListT f a -> (a -> f c) -> ListT f c

Bound MaybeT

Defined in Bound.Class

Methods

(>>>=) :: Monad f => MaybeT f a -> (a -> f c) -> MaybeT f c

Bound (IdentityT :: (Type -> Type) -> Type -> Type)

Defined in Bound.Class

Methods

(>>>=) :: Monad f => IdentityT f a -> (a -> f c) -> IdentityT f c

Error e => Bound (ErrorT e)

Defined in Bound.Class

Methods

(>>>=) :: Monad f => ErrorT e f a -> (a -> f c) -> ErrorT e f c

Bound (ReaderT r)

Defined in Bound.Class

Methods

(>>>=) :: Monad f => ReaderT r f a -> (a -> f c) -> ReaderT r f c

Bound (StateT s)

Defined in Bound.Class

Methods

(>>>=) :: Monad f => StateT s f a -> (a -> f c) -> StateT s f c

Monoid w => Bound (WriterT w)

Defined in Bound.Class

Methods

(>>>=) :: Monad f => WriterT w f a -> (a -> f c) -> WriterT w f c

Bound (Scope b)

Defined in Bound.Scope.Simple

Methods

(>>>=) :: Monad f => Scope b f a -> (a -> f c) -> Scope b f c

Bound (Scope b)

Defined in Bound.Scope

Methods

(>>>=) :: Monad f => Scope b f a -> (a -> f c) -> Scope b f c

Bound (ContT c)

Defined in Bound.Class

Methods

(>>>=) :: Monad f => ContT c f a -> (a -> f c0) -> ContT c f c0

Monoid w => Bound (RWST r w s)

Defined in Bound.Class

Methods

(>>>=) :: Monad f => RWST r w s f a -> (a -> f c) -> RWST r w s f c

(=<<<) :: (Bound t, Monad f) => (a -> f c) -> t f a -> t f c infixr 1

A flipped version of (>>>=).

(=<<<) = flip (>>>=)

Conversion to Traditional de Bruijn

data Var b a

"I am not a number, I am a free monad!"

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 Either.)

Constructors

B b

this is a bound variable

F a

this is a free variable

Instances

Bitraversable Var

Defined in Bound.Var

Methods

bitraverse :: Applicative f => (a -> f c) -> (b -> f d) -> Var a b -> f (Var c d)

Bifoldable Var

Defined in Bound.Var

Methods

bifold :: Monoid m => Var m m -> m

bifoldMap :: Monoid m => (a -> m) -> (b -> m) -> Var a b -> m

bifoldr :: (a -> c -> c) -> (b -> c -> c) -> c -> Var a b -> c

bifoldl :: (c -> a -> c) -> (c -> b -> c) -> c -> Var a b -> c

Bifunctor Var

Defined in Bound.Var

Methods

bimap :: (a -> b) -> (c -> d) -> Var a c -> Var b d

first :: (a -> b) -> Var a c -> Var b c

second :: (b -> c) -> Var a b -> Var a c

Eq2 Var

Defined in Bound.Var

Methods

liftEq2 :: (a -> b -> Bool) -> (c -> d -> Bool) -> Var a c -> Var b d -> Bool

Ord2 Var

Defined in Bound.Var

Methods

liftCompare2 :: (a -> b -> Ordering) -> (c -> d -> Ordering) -> Var a c -> Var b d -> Ordering

Read2 Var

Defined in Bound.Var

Methods

liftReadsPrec2 :: (Int -> ReadS a) -> ReadS [a] -> (Int -> ReadS b) -> ReadS [b] -> Int -> ReadS (Var a b)

liftReadList2 :: (Int -> ReadS a) -> ReadS [a] -> (Int -> ReadS b) -> ReadS [b] -> ReadS [Var a b]

liftReadPrec2 :: ReadPrec a -> ReadPrec [a] -> ReadPrec b -> ReadPrec [b] -> ReadPrec (Var a b)

liftReadListPrec2 :: ReadPrec a -> ReadPrec [a] -> ReadPrec b -> ReadPrec [b] -> ReadPrec [Var a b]

Show2 Var

Defined in Bound.Var

Methods

liftShowsPrec2 :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> (Int -> b -> ShowS) -> ([b] -> ShowS) -> Int -> Var a b -> ShowS

liftShowList2 :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> (Int -> b -> ShowS) -> ([b] -> ShowS) -> [Var a b] -> ShowS

Serial2 Var

Defined in Bound.Var

Methods

serializeWith2 :: MonadPut m => (a -> m ()) -> (b -> m ()) -> Var a b -> m ()

deserializeWith2 :: MonadGet m => m a -> m b -> m (Var a b)

Hashable2 Var

Defined in Bound.Var

Methods

liftHashWithSalt2 :: (Int -> a -> Int) -> (Int -> b -> Int) -> Int -> Var a b -> Int

Monad (Var b)

Defined in Bound.Var

Methods

(>>=) :: Var b a -> (a -> Var b b0) -> Var b b0

(>>) :: Var b a -> Var b b0 -> Var b b0

return :: a -> Var b a

Functor (Var b)

Defined in Bound.Var

Methods

fmap :: (a -> b0) -> Var b a -> Var b b0

(<$) :: a -> Var b b0 -> Var b a

Applicative (Var b)

Defined in Bound.Var

Methods

pure :: a -> Var b a

(<*>) :: Var b (a -> b0) -> Var b a -> Var b b0

liftA2 :: (a -> b0 -> c) -> Var b a -> Var b b0 -> Var b c

(*>) :: Var b a -> Var b b0 -> Var b b0

(<*) :: Var b a -> Var b b0 -> Var b a

Foldable (Var b)

Defined in Bound.Var

Methods

fold :: Monoid m => Var b m -> m

foldMap :: Monoid m => (a -> m) -> Var b a -> m

foldMap' :: Monoid m => (a -> m) -> Var b a -> m

foldr :: (a -> b0 -> b0) -> b0 -> Var b a -> b0

foldr' :: (a -> b0 -> b0) -> b0 -> Var b a -> b0

foldl :: (b0 -> a -> b0) -> b0 -> Var b a -> b0

foldl' :: (b0 -> a -> b0) -> b0 -> Var b a -> b0

foldr1 :: (a -> a -> a) -> Var b a -> a

foldl1 :: (a -> a -> a) -> Var b a -> a

toList :: Var b a -> [a]

null :: Var b a -> Bool

length :: Var b a -> Int

elem :: Eq a => a -> Var b a -> Bool

maximum :: Ord a => Var b a -> a

minimum :: Ord a => Var b a -> a

sum :: Num a => Var b a -> a

product :: Num a => Var b a -> a

Traversable (Var b)

Defined in Bound.Var

Methods

traverse :: Applicative f => (a -> f b0) -> Var b a -> f (Var b b0)

sequenceA :: Applicative f => Var b (f a) -> f (Var b a)

mapM :: Monad m => (a -> m b0) -> Var b a -> m (Var b b0)

sequence :: Monad m => Var b (m a) -> m (Var b a)

Eq b => Eq1 (Var b)

Defined in Bound.Var

Methods

liftEq :: (a -> b0 -> Bool) -> Var b a -> Var b b0 -> Bool

Ord b => Ord1 (Var b)

Defined in Bound.Var

Methods

liftCompare :: (a -> b0 -> Ordering) -> Var b a -> Var b b0 -> Ordering

Read b => Read1 (Var b)

Defined in Bound.Var

Methods

liftReadsPrec :: (Int -> ReadS a) -> ReadS [a] -> Int -> ReadS (Var b a)

liftReadList :: (Int -> ReadS a) -> ReadS [a] -> ReadS [Var b a]

liftReadPrec :: ReadPrec a -> ReadPrec [a] -> ReadPrec (Var b a)

liftReadListPrec :: ReadPrec a -> ReadPrec [a] -> ReadPrec [Var b a]

Show b => Show1 (Var b)

Defined in Bound.Var

Methods

liftShowsPrec :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> Var b a -> ShowS

liftShowList :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> [Var b a] -> ShowS

Serial b => Serial1 (Var b)

Defined in Bound.Var

Methods

serializeWith :: MonadPut m => (a -> m ()) -> Var b a -> m ()

deserializeWith :: MonadGet m => m a -> m (Var b a)

Hashable b => Hashable1 (Var b)

Defined in Bound.Var

Methods

liftHashWithSalt :: (Int -> a -> Int) -> Int -> Var b a -> Int

Generic1 (Var b :: Type -> Type)

Defined in Bound.Var

Associated Types

type Rep1 (Var b) :: k -> Type

Methods

from1 :: forall (a :: k). Var b a -> Rep1 (Var b) a

to1 :: forall (a :: k). Rep1 (Var b) a -> Var b a

(Eq b, Eq a) => Eq (Var b a)

Defined in Bound.Var

Methods

(==) :: Var b a -> Var b a -> Bool

(/=) :: Var b a -> Var b a -> Bool

(Data b, Data a) => Data (Var b a)

Defined in Bound.Var

Methods

gfoldl :: (forall d b0. Data d => c (d -> b0) -> d -> c b0) -> (forall g. g -> c g) -> Var b a -> c (Var b a)

gunfold :: (forall b0 r. Data b0 => c (b0 -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (Var b a)

toConstr :: Var b a -> Constr

dataTypeOf :: Var b a -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (Var b a))

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Var b a))

gmapT :: (forall b0. Data b0 => b0 -> b0) -> Var b a -> Var b a

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Var b a -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Var b a -> r

gmapQ :: (forall d. Data d => d -> u) -> Var b a -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Var b a -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Var b a -> m (Var b a)

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Var b a -> m (Var b a)

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Var b a -> m (Var b a)

(Ord b, Ord a) => Ord (Var b a)

Defined in Bound.Var

Methods

compare :: Var b a -> Var b a -> Ordering

(<) :: Var b a -> Var b a -> Bool

(<=) :: Var b a -> Var b a -> Bool

(>) :: Var b a -> Var b a -> Bool

(>=) :: Var b a -> Var b a -> Bool

max :: Var b a -> Var b a -> Var b a

min :: Var b a -> Var b a -> Var b a

(Read b, Read a) => Read (Var b a)

Defined in Bound.Var

Methods

readsPrec :: Int -> ReadS (Var b a)

readList :: ReadS [Var b a]

readPrec :: ReadPrec (Var b a)

readListPrec :: ReadPrec [Var b a]

(Show b, Show a) => Show (Var b a)

Defined in Bound.Var

Methods

showsPrec :: Int -> Var b a -> ShowS

show :: Var b a -> String

showList :: [Var b a] -> ShowS

Generic (Var b a)

Defined in Bound.Var

Associated Types

type Rep (Var b a) :: Type -> Type

Methods

from :: Var b a -> Rep (Var b a) x

to :: Rep (Var b a) x -> Var b a

(Binary b, Binary a) => Binary (Var b a)

Defined in Bound.Var

Methods

put :: Var b a -> Put

get :: Get (Var b a)

putList :: [Var b a] -> Put

(Serial b, Serial a) => Serial (Var b a)

Defined in Bound.Var

Methods

serialize :: MonadPut m => Var b a -> m ()

deserialize :: MonadGet m => m (Var b a)

(Serialize b, Serialize a) => Serialize (Var b a)

Defined in Bound.Var

Methods

put :: Putter (Var b a)

get :: Get (Var b a)

(NFData a, NFData b) => NFData (Var b a)

Defined in Bound.Var

Methods

rnf :: Var b a -> ()

(Hashable b, Hashable a) => Hashable (Var b a)

Defined in Bound.Var

Methods

hashWithSalt :: Int -> Var b a -> Int

hash :: Var b a -> Int

type Rep1 (Var b :: Type -> Type)

Defined in Bound.Var

type Rep1 (Var b :: Type -> Type) = D1 ('MetaData "Var" "Bound.Var" "bound-2.0.3-IMm1RxjoHWu6bB6DEZNDCu" 'False) (C1 ('MetaCons "B" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 b)) :+: C1 ('MetaCons "F" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) Par1))

type Rep (Var b a)

Defined in Bound.Var

type Rep (Var b a) = D1 ('MetaData "Var" "Bound.Var" "bound-2.0.3-IMm1RxjoHWu6bB6DEZNDCu" 'False) (C1 ('MetaCons "B" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 b)) :+: C1 ('MetaCons "F" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a)))

fromScope :: Monad f => Scope b f a -> f (Var b a)

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.

Since,

fromScope . toScope ≡ id

we know that

fromScope . toScope . fromScope ≡ fromScope

and therefore (toScope . fromScope) is idempotent.

toScope :: Monad f => f (Var b a) -> Scope b f a

Convert from traditional de Bruijn to generalized de Bruijn indices.

This requires a full tree traversal

Deriving instances

makeBound :: Name -> DecsQ

Use to automatically derive Applicative and Monad instances for your datatype.

Also works for components that are lists or instances of Functor, but still does not work for a great deal of other things.

deriving-compat package may be used to derive the Show1 and Read1 instances

{-# LANGUAGE DeriveFunctor      #-}
{-# LANGUAGE TemplateHaskell    #-}

import Bound                (Scope, makeBound)
import Data.Functor.Classes (Show1, Read1, showsPrec1, readsPrec1)
import Data.Deriving        (deriveShow1, deriveRead1)

data Exp a
  = V a
  | App (Exp a) (Exp a)
  | Lam (Scope () Exp a)
  | ND [Exp a]
  | I Int
  deriving (Functor)

makeBound ''Exp
deriveShow1 ''Exp
deriveRead1 ''Exp
instance Read a => Read (Exp a) where readsPrec = readsPrec1
instance Show a => Show (Exp a) where showsPrec = showsPrec1

and in GHCi

ghci> :set -XDeriveFunctor
ghci> :set -XTemplateHaskell
ghci> import Bound                (Scope, makeBound)
ghci> import Data.Functor.Classes (Show1, Read1, showsPrec1, readsPrec1)
ghci> import Data.Deriving        (deriveShow1, deriveRead1)
ghci> :{
ghci| data Exp a = V a | App (Exp a) (Exp a) | Lam (Scope () Exp a) | ND [Exp a] | I Int deriving (Functor)
ghci| makeBound ''Exp
ghci| deriveShow1 ''Exp
ghci| deriveRead1 ''Exp
ghci| instance Read a => Read (Exp a) where readsPrec = readsPrec1
ghci| instance Show a => Show (Exp a) where showsPrec = showsPrec1
ghci| :}

Eq and Ord instances can be derived similarly

import Data.Functor.Classes (Eq1, Ord1, eq1, compare1)
import Data.Deriving        (deriveEq1, deriveOrd1)

deriveEq1 ''Exp
deriveOrd1 ''Exp
instance Eq a => Eq (Exp a) where (==) = eq1
instance Ord a => Ord (Exp a) where compare = compare1

or in GHCi:

ghci> import Data.Functor.Classes (Eq1, Ord1, eq1, compare1)
ghci> import Data.Deriving        (deriveEq1, deriveOrd1)
ghci> :{
ghci| deriveEq1 ''Exp
ghci| deriveOrd1 ''Exp
ghci| instance Eq a => Eq (Exp a) where (==) = eq1
ghci| instance Ord a => Ord (Exp a) where compare = compare1
ghci| :}

We cannot automatically derive Eq and Ord using the standard GHC mechanism, because instances require Exp to be a Monad:

instance (Monad f, Eq b, Eq1 f, Eq a)    => Eq (Scope b f a)
instance (Monad f, Ord b, Ord1 f, Ord a) => Ord (Scope b f a)