bound
Making de Bruijn Succ Less
http://github.com/ekmett/bound/
Version on this page: | 2.0.7 |
LTS Haskell 22.37: | 2.0.7@rev:2 |
Stackage Nightly 2024-10-07: | 2.0.7@rev:2 |
Latest on Hackage: | 2.0.7@rev:2 |
BSD-3-Clause licensed by Edward A. Kmett
Maintained by Edward A. Kmett
This version can be pinned in stack with:
bound-2.0.7@sha256:ca9f8248d42b0873469f5726e2eb892914ca7165dc5dc8fbe039abc8ca712116,4284
Module documentation for 2.0.7
Depends on 14 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, evaluator, 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 #-}
{-# LANGUAGE TemplateHaskell #-}
import Bound
import Control.Applicative
import Control.Monad
import Data.Functor.Classes
import Data.Foldable
import Data.Traversable
import Data.Eq.Deriving (deriveEq1) -- these two are from the
import Text.Show.Deriving (deriveShow1) -- deriving-compat package
infixl 9 :@
data Exp a = V a | Exp a :@ Exp a | Lam (Scope () Exp a)
deriving (Eq,Show,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)
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
deriveEq1 ''Exp
deriveShow1 ''Exp
main :: IO ()
main = do
let term = lam 'x' (V 'x') :@ V 'y'
print term -- Lam (Scope (V (B ()))) :@ V 'y'
print $ whnf term -- V 'y'
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
Changes
2.0.7 [2023.08.06]
- Support building with
template-haskell-2.21.*
(GHC 9.8).
2.0.6 [2023.01.18]
- Allow the examples to build with
base-4.18.*
(GHC 9.6).
2.0.5 [2022.05.07]
- Allow building with
transformers-0.6.*
.
2.0.4 [2021.11.07]
- Allow building with
template-haskell-2.18
(GHC 9.2). - The
Bound.TH
module no longer requires theTemplateHaskell
extension (onlyTemplateHaskellQuotes
) when building with GHC 9.0 or later. - Drop support for pre-8.0 versions of GHC.
2.0.3 [2021.02.05]
- Allow the examples to build with
vector-0.12.2
or later. - The build-type has been changed from
Custom
toSimple
. To achieve this, thedoctests
test suite has been removed in favor of usingcabal-docspec
to run the doctests.
2.0.2 [2020.10.01]
- Allow building with GHC 9.0.
2.0.1
- Add
abstractEither
andinstantiateEither
toBound.Scope
, and addabstractEitherName
andinstantiateEitherName
toBound.Scope.Name
- Add
Generic(1)
instances forName
andScope
- Support
doctest-0.12
2
- GHC 8.0 and 8.2 support
- Converted from
prelude-extras
totransformers
+transformers-compat
for theEq1
,Ord1
,Show1
, andRead1
functionality. makeBound
supportsFunctor
components- Add
MFunctor
instance forScope
- Add
NFData
instances forName
,Scope
, andVar
- Revamp
Setup.hs
to usecabal-doctest
. This makes it build withCabal-1.25
, and makes thedoctest
s work withcabal new-build
and sandboxes.
1.0.7
- Added an
-f-template-haskell
option to allow disablingtemplate-haskell
support. This is an unsupported configuration but may be useful for expert users in sandbox configurations. - Support
cereal
0.5
1.0.6
- Compiles warning-free on GHC 7.10
1.0.5
- Widened version bound on
bifunctors
. - Widened version bound on
profunctors
.
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
forBound.Scope.Simple
1.0
- Added instances for
Bound
for all of themtl
monads. - Added
Data
andTypeable
support to both versions ofScope
- Added the missing
Applictive
instance toBound.Scope.Simple
- Moved
hoistScope
,bitraverseScope
,transverseScope
, andinstantiateVars
here from theermine
compiler.
0.9.1.1
- Updated to work with
bifunctors
4.0
0.9.1
- Updated to work with
comonad
4.0 andprofunctors
4.0
0.9
- Added the missing instance for
Applicative (Scope b f)
0.8.1
- SafeHaskell support
0.8
- Added
Serial
,Binary
andSerialize
instances forScope
.
0.7
- Added
Hashable
,Hashable1
andHashable2
instances where appropriate forName
,Var
andScope
.
0.6.1
- More aggressive inlining
- Added
unvar
,_B
,_F
toBound.Var
. - Added
_Name
toBound.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 many examples
- 100% haddock coverage
- Added the
Name
Comonad
, to help retain names for bound variables. - Bumped dependencies