unbound-0.2.4: Unbound/LocallyNameless.hs
----------------------------------------------------------------------
-- |
-- Module : Unbound.LocallyNameless
-- License : BSD-like (see LICENSE)
-- Maintainer : Brent Yorgey <byorgey@cis.upenn.edu>
-- Stability : experimental
-- Portability : GHC only (-XKitchenSink)
--
-- A generic implementation of standard functions dealing with names
-- and binding structure (alpha equivalence, free variable
-- calculation, capture-avoiding substitution, name permutation, ...)
-- using a locally nameless representation. (See "Unbound.Nominal" for
-- a nominal implementation of the same interface.)
--
-- Normal users of this library should only need to import this module
-- (or "Unbound.Nominal"). In particular, this module is careful to
-- export only an abstract interface with various safety guarantees.
-- Power users who wish to have access to the internals of the library
-- (at the risk of shooting oneself in the foot) can directly import
-- the various implementation modules such as
-- "Unbound.LocallyNameless.Name" and so on.
--
-- /Ten-second tutorial/: use the type combinators 'Bind', 'Embed',
-- 'Rebind', 'Rec', 'TRec', and 'Shift' to specify the binding
-- structure of your data types. Then use Template Haskell to derive
-- generic representations for your types:
--
-- > $(derive [''Your, ''Types, ''Here])
--
-- Finally, declare 'Alpha' and 'Subst' instances for your types.
-- Then you can go to town using all the generically-derived
-- operations like 'aeq', 'fv', 'subst', and so on.
--
-- For more information, see the more in-depth literate Haskell
-- tutorial in the @tutorial@ directory (which can be obtained as part
-- of the library source package: @cabal unpack unbound@) and the
-- examples in the @example@ directory.
--
-- See also: Stephanie Weirich, Brent A. Yorgey, and Tim Sheard.
-- /Binders Unbound/. To appear in ICFP'11, September 2011, Tokyo, Japan. <http://www.cis.upenn.edu/~byorgey/papers/binders-unbound.pdf>.
----------------------------------------------------------------------
module Unbound.LocallyNameless
( -- * Names
Name, AnyName(..),
-- ** Constructing and destructing free names
integer2Name, string2Name, s2n, makeName,
name2Integer, name2String, anyName2Integer, anyName2String,
-- ** Dealing with name sorts
translate, toSortedName,
-- * Type combinators for specifying binding structure
--
-- | 'Bind', 'Embed', 'Rebind', 'Rec', 'TRec', and 'Shift' are
-- special types provided by Unbound for use in specifying the
-- binding structure of your data types.
--
-- An important distinction to keep in mind is the difference
-- between /term types/ and /pattern types/.
--
-- * /Term types/ are normal types whose values represent data in
-- your program. Any 'Name's occurring in term types are
-- either free variables, or /references/ to binders.
--
-- * /Pattern types/ are types which may be used on the left
-- hand side of a 'Bind'. They /bind/ names, that is, any
-- 'Name's occurring in pattern types are /binding sites/ to
-- which other names may refer.
--
-- 'Name' may be used as both a term type (where it represents a
-- free variable/reference) and a pattern type (where it
-- represents a binding site).
--
-- Any first-order algebraic data type (/i.e./ one containing no
-- functions) which contains only term types may be used as a
-- term type, and likewise for algebraic data types containing
-- only pattern types. For example,
--
-- > (Name, [Name])
--
-- may be used as either a term type or a pattern type. On the
-- other hand,
--
-- > (Bind Name Name, Name)
--
-- may only be used as a term type, since @Bind Name Name@ is a
-- term type and not a pattern type.
--
-- We adopt the convention that the type variable @t@ stands for
-- term types, and the type variable @p@ stands for pattern
-- types. It would be nicer if we could actually use Haskell's
-- type system to enforce the distinction, but for various
-- technical reasons (involving the RepLib generic programming
-- framework which is used in the implementation), we cannot.
-- Or at least, we are not sufficiently clever to see how.
-- ** Bind
Bind,
-- *** Bind constructor
bind,
-- *** Bind destructors
-- | Directly pattern-matching on 'Bind' values is not allowed,
-- but there are quite a few different ways to safely \"open\" a
-- binding. (If you want direct, unsafe access to the
-- components of a binding --- e.g. to write a function to
-- compute the size of terms that ignores all names --- you can
-- directly import "Unbound.LocallyNameless.Ops" and use the
-- 'unsafeUnbind' function.)
unbind,
lunbind,
-- *** Simultaneous unbinding
-- | Sometimes one may wish to open several bindings using /same/
-- names for their binding variables --- for example, when
-- checking equality of terms involving binders, so that the
-- free variables in the bodies will match appropriately during
-- recursive calls. Opening two bindings simultaneously is
-- accomplished with 'unbind2' (which picks globally fresh
-- names) and 'lunbind2' (which picks /locally/ fresh names, see
-- the 'LFresh' documentation for more information). 'unbind3'
-- and 'lunbind3' open three bindings simultaneously. In
-- principle, of course, @unbindN@ and @lunbindN@ can be easily
-- implemented for any @N@; please let the maintainers know if
-- for some reason you would like an N > 3.
unbind2, unbind3,
lunbind2, lunbind3,
-- ** Embed
Embed(..),
embed, unembed,
-- ** Rebind
Rebind,
rebind, unrebind,
-- ** Rec
Rec,
rec, unrec,
-- ** TRec
TRec,
trec, untrec, luntrec,
-- ** Shift
Shift(..),
-- * Generically derived operations
-- | This section lists a number of operations which are derived
-- generically for any types whose binding structure is
-- specified via the type combinators described in the previous
-- section.
-- ** Alpha-equivalence
aeq, aeqBinders,
acompare,
-- ** Variable calculations
-- | Functions for computing the free variables or binding
-- variables of a term or pattern. Note that all these
-- functions may return an arbitrary /collection/, which
-- includes lists, sets, and multisets.
fv, fvAny, patfv, patfvAny, binders, bindersAny,
-- *** Collections
Collection(..), Multiset(..),
-- ** Substitution
-- | Capture-avoiding substitution.
Subst(..), SubstName(..),
-- ** Permutations
Perm,
-- *** Working with permutations
single, compose, apply, support, isid, join, empty, restrict, mkPerm,
-- *** Permuting terms
swaps, swapsEmbeds, swapsBinders,
-- * Freshness
-- | When opening a term-level binding ('Bind' or 'TRec'), fresh
-- names must be generated for the binders of its pattern.
-- Fresh names can be generated according to one of two
-- strategies: names can be /globally/ fresh (not conflicting
-- with any other generated names, ever; see 'Fresh') or
-- /locally/ fresh (not conflicting only with a specific set of
-- \"currently in-scope\" names; see 'LFresh'). Generating
-- globally fresh names is simpler and suffices for many
-- applications. Generating locally fresh names tends to be
-- useful when the names are for human consumption, e.g. when
-- implementing a pretty-printer.
-- ** Global freshness
freshen,
-- *** The @Fresh@ class
Fresh(..),
-- *** The @FreshM@ monad
-- | The @FreshM@ monad provides a concrete implementation of the
-- 'Fresh' type class. The @FreshMT@ monad transformer variant
-- can be freely combined with other standard monads and monad
-- transformers from the @transformers@ library.
FreshM, runFreshM,
FreshMT, runFreshMT,
-- ** Local freshness
lfreshen,
-- *** The @LFresh@ class
LFresh(..),
-- *** The @LFreshM@ monad
-- | The @LFreshM@ monad provides a concrete implementation of the
-- 'LFresh' type class. The @LFreshMT@ monad transformer variant
-- can be freely combined with other standard monads and monad
-- transformers from the @transformers@ library.
LFreshM, runLFreshM, getAvoids,
LFreshMT, runLFreshMT,
-- * The @Alpha@ class
Alpha(..),
-- * Re-exported RepLib API for convenience
module Generics.RepLib,
-- * Pay no attention to the man behind the curtain
-- | These type representation objects are exported so they can be
-- referenced by auto-generated code. Please pretend they do not
-- exist.
rName, rBind, rRebind, rEmbed, rRec, rShift
) where
import Unbound.LocallyNameless.Name
import Unbound.LocallyNameless.Fresh
import Unbound.LocallyNameless.Types
import Unbound.LocallyNameless.Alpha
import Unbound.LocallyNameless.Subst
import Unbound.LocallyNameless.Ops
import Unbound.Util
import Unbound.PermM
import Generics.RepLib