Skip to content
Fetching contributors…
Cannot retrieve contributors at this time
135 lines (132 sloc) 4.54 KB
{-# LANGUAGE CPP #-}
-----------------------------------------------------------------------------
-- |
-- Copyright : (C) 2012 Edward Kmett
-- License : BSD-style (see the file LICENSE)
--
-- Maintainer : Edward Kmett <ekmett@gmail.com>
-- Stability : experimental
-- Portability : portable
--
-- 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.
--
-- An untyped lambda calculus:
--
-- @
-- {-\# LANGUAGE DeriveFunctor, DeriveFoldable, DeriveTraversable \#-}
-- import Bound
-- import Control.Applicative
-- import Control.Monad ('Control.Monad.ap')
-- import Prelude.Extras
-- 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','Data.Foldable.Foldable','Data.Foldable.Traversable')
-- @
--
-- @
-- instance 'Prelude.Extras.Eq1' Exp
-- instance 'Prelude.Extras.Ord1' Exp
-- instance 'Prelude.Extras.Show1' Exp
-- instance 'Prelude.Extras.Read1' Exp
-- instance 'Control.Applicative.Applicative' Exp where 'Control.Applicative.pure' = V; ('<*>') = 'Control.Monad.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
-- @
--
-- More exotic combinators for manipulating a 'Scope' can be imported from
-- "Bound.Scope".
--
-- You can also retain names in your bound variables by using 'Bound.Name.Name'
-- and the related combinators from "Bound.Name". They are not re-exported
-- from this module by default.
--
-- The approach used in this package was first elaborated upon by Richard Bird
-- and Ross Patterson
-- in \"de Bruijn notation as a nested data type\", available from
-- <http://www.cs.uwyo.edu/~jlc/courses/5000_fall_08/debruijn_as_nested_datatype.pdf>
--
-- However, the combinators they used required higher rank types. Here we
-- demonstrate that the higher rank @gfold@ combinator they used isn't necessary
-- to build the monad and use a monad transformer to encapsulate the novel
-- recursion pattern in their generalized de Bruijn representation. It is named
-- 'Scope' to match up with the terminology and usage pattern from Conor McBride
-- and James McKinna's \"I am not a number: I am a free variable\", available
-- from <http://www.cs.st-andrews.ac.uk/~james/RESEARCH/notanum.pdf>, but since
-- the set of variables is visible in the type, we can provide stronger type
-- safety guarantees.
--
-- There are longer examples in the @examples/@ folder:
--
-- <https://github.com/ekmett/bound/tree/master/examples>
--
-- (1) /Simple.hs/ provides an untyped lambda calculus with recursive let
-- bindings and includes an evaluator for the untyped lambda calculus and a
-- longer example taken from Lennart Augustsson's "λ-calculus cooked four
-- ways" available from <http://foswiki.cs.uu.nl/foswiki/pub/USCS/InterestingPapers/AugustsonLambdaCalculus.pdf>
--
-- 2. /Derived.hs/ shows how much of the API can be automated with
-- DeriveTraversable and adds combinators for building binders that support
-- pattern matching.
--
-- 3. /Overkill.hs/ provides very strongly typed pattern matching many modern
-- language extensions, including polymorphic kinds to ensure type safety.
-- In general, the approach taken by Derived seems to deliver a better power
-- to weight ratio.
----------------------------------------------------------------------------
module Bound
(
-- * Manipulating user terms
substitute
, isClosed
, closed
-- * Scopes introduce bound variables
, Scope(..)
-- ** Abstraction over bound variables
, abstract, abstract1
-- ** Instantiation of bound variables
, instantiate, instantiate1
-- * Structures permitting substitution
, Bound(..)
, (=<<<)
-- * Conversion to Traditional de Bruijn
, Var(..)
, fromScope
, toScope
-- * Deriving instances
, makeBound
) where
import Bound.Var
import Bound.Class
import Bound.Scope
import Bound.Term
#ifdef MIN_VERSION_template_haskell
import Bound.TH
#endif
Something went wrong with that request. Please try again.