bound
Making de Bruijn Succ Less
http://github.com/ekmett/bound/
| Version on this page: | 1.0.7 |
| LTS Haskell 22.39: | 2.0.7@rev:2 |
| Stackage Nightly 2024-10-31: | 2.0.7@rev:2 |
| Latest on Hackage: | 2.0.7@rev:2 |
Maintained by Edward A. Kmett
This version can be pinned in stack with:
bound-1.0.7@sha256:1ca3a6a5ac827c3de1ecc9be9f1ee09592f1bed0f58be2ffcf861f352ea33032,3513Module documentation for 1.0.7
Depends on 12 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 #-}
import Bound
import Prelude.Extras
import Control.Applicative
import Control.Monad
import Data.Foldable
import Data.Traversable
infixl 9 :@
data Exp a = V a | Exp a :@ Exp a | Lam (Scope () Exp a)
deriving (Eq,Ord,Show,Read,Functor,Foldable,Traversable)
instance Eq1 Exp
instance Ord1 Exp
instance Show1 Exp
instance Read1 Exp
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
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