bound: Making de Bruijn Succ Less

[ bsd3, compilers-interpreters, language, library ] [ Propose Tags ] [ Report a vulnerability ]

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.

Slides describing and motivating this approach to name binding are available online at:

http://www.slideshare.net/ekmett/bound-making-de-bruijn-succ-less

The goal of this package is to make it as easy as possible to deal with name binding without forcing an awkward monadic style on the user.

With generalized de Bruijn term you can lift whole trees instead of just applying succ to individual variables, weakening the all variables bound by a scope and greatly speeding up instantiation. By giving binders more structure we permit easy simultaneous substitution and further speed up instantiation.


[Skip to Readme]

Flags

Manual Flags

NameDescriptionDefault
template-haskell

You can disable the use of the `template-haskell` package using `-f-template-haskell`.

Disabling this is an unsupported configuration, but it may be useful for accelerating builds in sandboxes for expert users.

Enabled

Use -f <flag> to enable a flag, or -f -<flag> to disable that flag. More info

Downloads

Note: This package has metadata revisions in the cabal description newer than included in the tarball. To unpack the package including the revisions, use 'cabal get'.

Maintainer's Corner

Package maintainers

For package maintainers and hackage trustees

Candidates

  • No Candidates
Versions [RSS] 0.1, 0.1.1, 0.1.2, 0.1.3, 0.1.4, 0.2, 0.2.1, 0.3.1, 0.3.2, 0.4, 0.5, 0.5.0.1, 0.5.0.2, 0.5.1, 0.6, 0.6.1, 0.7, 0.8, 0.8.1, 0.9, 0.9.0.1, 0.9.1, 0.9.1.1, 1.0, 1.0.1, 1.0.2, 1.0.3, 1.0.4, 1.0.5, 1.0.6, 1.0.7, 2, 2.0.1, 2.0.2, 2.0.3, 2.0.4, 2.0.5, 2.0.6, 2.0.7
Change log CHANGELOG.markdown
Dependencies base (>=4 && <4.15), bifunctors (>=3 && <6), binary (>=0.5 && <0.9), bytes (>=0.4 && <1), cereal (>=0.3.5.2 && <0.6), comonad (>=3 && <6), deepseq (>=1.1 && <1.5), ghc-prim, hashable (>=1.2.5.0 && <1.3), mmorph (>=1.0 && <1.2), profunctors (>=3.3 && <6), template-haskell (>=2.7 && <2.17), transformers (>=0.2 && <0.6), transformers-compat (>=0.5 && <1) [details]
Tested with ghc ==7.4.2, ghc ==7.6.3, ghc ==7.8.4, ghc ==7.10.3, ghc ==8.0.2, ghc ==8.2.1
License BSD-3-Clause
Copyright Copyright (C) 2012-2013 Edward A. Kmett
Author Edward A. Kmett
Maintainer Edward A. Kmett <ekmett@gmail.com>
Revised Revision 3 made by ryanglscott at 2021-02-05T12:27:38Z
Category Language, Compilers/Interpreters
Home page http://github.com/ekmett/bound/
Bug tracker http://github.com/ekmett/bound/issues
Source repo head: git clone git://github.com/ekmett/bound.git
Uploaded by ryanglscott at 2017-05-12T15:01:17Z
Distributions LTSHaskell:2.0.7, NixOS:2.0.7, Stackage:2.0.7
Reverse Dependencies 9 direct, 0 indirect [details]
Downloads 37879 total (80 in the last 30 days)
Rating 2.5 (votes: 4) [estimated by Bayesian average]
Your Rating
  • λ
  • λ
  • λ
Status Docs available [build log]
Last success reported on 2017-05-12 [all 1 reports]

Readme for bound-2

[back to package description]

Bound

Hackage Build Status

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