Permalink
Browse files

moved documentation around to make the main cabal page less intimidating

  • Loading branch information...
1 parent 5baaecd commit 8709592303d163ad45bc3ec8f53a203c7aa25e29 @ekmett committed Sep 13, 2012
Showing with 41 additions and 72 deletions.
  1. +8 −72 bound.cabal
  2. +33 −0 src/Bound.hs
View
@@ -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,91 +10,27 @@ stability: experimental
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
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:
+ Slides describing and motivating this approach to name binding are available
+ online at:
.
- > 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
- .
- 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'.
+ <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 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
- <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://www.augustsson.net/Darcs/Lambda/top.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.
+ 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:
View
@@ -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
+-- <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://www.augustsson.net/Darcs/Lambda/top.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
(

0 comments on commit 8709592

Please sign in to comment.