bound 0.5 → 0.5.0.1

raw patch · 2 files changed

+41/−72 lines, 2 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

• bound.cabal +8/−72
• src/Bound.hs +33/−0

@@ -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'.+   <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:

@@ -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   (