@hackage / bound

Making de Bruijn Succ Less

Latest2.0.7

About

Metadata

  • Last updated , by ryanglscott
  • License BSD-3-Clause
  • Categories Compilers and Interpreters

  • Maintained by: Edward A. Kmett <ekmett@gmail.com>

  • Lottery factor: 0

Links

Installation

Tested Compilers

  1. 9.6.2
  2. 9.4.5
  3. 9.2.8
  4. 9.0.2
  5. 8.10.7
  6. 8.8.4
  7. 8.6.5
  8. 8.4.4
  9. 8.2.2
  10. 8.0.2

Package Flags

Use the -f option with cabal commands to enable flags

    template-haskell (on by default)

    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.

Readme

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