# bound

Making de Bruijn Succ Less

http://github.com/ekmett/bound/

 Version on this page: 1.0.4 LTS Haskell 22.18: 2.0.7@rev:1 Stackage Nightly 2024-04-22: 2.0.7@rev:1 Latest on Hackage: 2.0.7@rev:1

See all snapshots `bound` appears in

Maintained by
This version can be pinned in stack with:`bound-1.0.4@sha256:71f35d8641ee2db8e2321096af765f86e06cf9f1184935883911df9487488817,3153`

#### Module documentation for 1.0.4

• Bound
• Bound.Class
• Bound.Name
• Bound.Scope
• Bound.Scope.Simple
• Bound.Term
• Bound.Var
Depends on 11 packages(full list with versions):

# Bound

## Goals

This library provides convenient combinators for working with “locally-nameless” terms. These can be useful when writing a type checker, evalator, parser, or pretty printer for terms that contain binders like forall or lambda, as they ease the task of avoiding variable capture and testing for alpha-equivalence.

See the documentation on hackage for more information, but here is an example:

``````{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE DeriveFoldable #-}
{-# LANGUAGE DeriveTraversable #-}
import Bound
import Prelude.Extras
import Control.Applicative
import Data.Foldable
import Data.Traversable

infixl 9 :@
data Exp a = V a | Exp a :@ Exp a | Lam (Scope () Exp a)

instance Eq1 Exp
instance Ord1 Exp
instance Show1 Exp
instance Applicative Exp where pure = V; (<*>) = ap

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

There are longer examples in the examples/ folder.

## Contact Information

Contributions and bug reports are welcome!

Please feel free to contact me through github or on the #haskell IRC channel on irc.freenode.net.

-Edward Kmett

## 1.0.4

• Widened version bound on `transformers`.

## 1.0.3

• Added `bitransverseScope`.

## 1.0.2

• Removed unneccesary constraint on `hoistScope`.

## 1.0.1

• Added a monomorphic `hoistScope` for `Bound.Scope.Simple`

## 1.0

• Added instances for `Bound` for all of the `mtl` monads.
• Added `Data` and `Typeable` support to both versions of `Scope`
• Added the missing `Applictive` instance to `Bound.Scope.Simple`
• Moved `hoistScope`, `bitraverseScope`, `transverseScope`, and `instantiateVars` here from the `ermine` compiler.

## 0.9.1.1

• Updated to work with `bifunctors` 4.0

## 0.9.1

• Updated to work with `comonad` 4.0 and `profunctors` 4.0

## 0.9

• Added the missing instance for `Applicative (Scope b f)`

## 0.8

• Added `Serial`, `Binary` and `Serialize` instances for `Scope`.

## 0.7

• Added `Hashable`, `Hashable1` and `Hashable2` instances where appropriate for `Name`, `Var` and `Scope`.

## 0.6.1

• More aggressive inlining
• Added `unvar`, `_B`, `_F` to `Bound.Var`.
• Added `_Name` to `Bound.Name`.

## 0.6

• Support for `prelude-extras` 0.3

## 0.5.1

• Removed my personal inter-package dependency upper bounds
• Updated doctest suite to use exact versions.

## 0.5

• Created a `doctest`-based test suite
• Added the `Name` `Comonad`, to help retain names for bound variables.