diff --git a/bound.cabal b/bound.cabal --- a/bound.cabal +++ b/bound.cabal @@ -1,6 +1,6 @@ name: bound category: Language, Compilers/Interpreters -version: 0.5 +version: 0.5.0.1 license: BSD3 cabal-version: >= 1.9.2 license-file: LICENSE @@ -10,7 +10,7 @@ homepage: http://github.com/ekmett/bound/ bug-reports: http://github.com/ekmett/bound/issues copyright: Copyright (C) 2012 Edward A. Kmett -synopsis: Haskell 98/2010 Locally-Nameless Generalized de Bruijn Terms +synopsis: Making de Bruijn Succ Less description: We represent the target language itself as an ideal monad supplied by the user, and provide a 'Scope' monad transformer for introducing bound variables @@ -18,83 +18,19 @@ and we traverse to find free variables, and use the Monad to perform substitution that avoids bound variables. . - An untyped lambda calculus: - . - > import Bound - > import Control.Applicative - > import Control.Monad (ap) - > import Data.Foldable - > import Data.Traversable - > import Prelude.Extras - . - > 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 where (==#) = (==) - > instance Ord1 Exp where compare1 = compare - > instance Show1 Exp where showsPrec1 = showsPrec - > instance Read1 Exp where readsPrec1 = readsPrec - > 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 + Slides describing and motivating this approach to name binding are available + online at: . - The classes from Prelude.Extras are used to facilitate the automatic deriving - of 'Eq', 'Ord', 'Show', and 'Read' in the presence of polymorphic recursion - used inside 'Scope'. + . 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 by giving binders more structure we can permit easy - simultaneous substitution. - . - The approach was first elaborated upon by Richard Bird and Ross Patterson - in \"de Bruijn notation as a nested data type\", available from - - . - 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 , 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: - . - - . - (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 - . - 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. + by a scope and greatly speeding up instantiation. By giving binders more + structure we permit easy simultaneous substitution and further speed up + instantiation. build-type: Simple extra-source-files: diff --git a/src/Bound.hs b/src/Bound.hs --- a/src/Bound.hs +++ b/src/Bound.hs @@ -67,6 +67,39 @@ -- 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 +-- +-- +-- 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 , 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: +-- +-- +-- +-- (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 +-- +-- 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 (