diff --git a/README b/README --- a/README +++ b/README @@ -7,6 +7,17 @@ -- Stability : experimental -- Portability : non-portable -- --- See http://code.google.com/p/replib/ for more information. ----------------------------------------------------------------------------- +Specify the binding structure of your data type with an expressive set +of type combinators, and Unbound handles the rest! Automatically +derives alpha-equivalence, free variable calculation, capture-avoiding +substitution, and more. + +To install (requires GHC 7), just + + cabal install unbound + +To get started using the library, see the tutorial in the tutorial/ +directory and the extensive Haddock documentation (start with the +Unbound.LocallyNameless module). diff --git a/Unbound/LocallyNameless.hs b/Unbound/LocallyNameless.hs --- a/Unbound/LocallyNameless.hs +++ b/Unbound/LocallyNameless.hs @@ -3,79 +3,253 @@ -- | -- Module : Unbound.LocallyNameless -- License : BSD-like (see LICENSE) --- --- Maintainer : Stephanie Weirich +-- Maintainer : Brent Yorgey -- Stability : experimental --- Portability : non-portable (-XKitchenSink) +-- Portability : GHC only (-XKitchenSink) -- --- A generic implementation of name binding functions using a locally --- nameless representation. Datatypes with binding can be defined --- using the 'Name' and 'Bind' types. Expressive patterns for binding --- come from the 'Embed' and 'Rebind' types. +-- 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.) -- --- Important classes are: +-- 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. -- --- * 'Alpha' -- the class of types and patterns that include binders, +-- /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: -- --- * 'Subst' -- for subtitution functions. +-- > $(derive [''Your, ''Types, ''Here]) -- --- Name generation is controlled via monads which implement the --- 'Fresh' and 'LFresh' classes. +-- 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 Yorgey, and Tim Sheard. +-- /Binders Unbound/. Submitted, March 2011. . ---------------------------------------------------------------------- module Unbound.LocallyNameless - ( -- * Basic types - Name, AnyName(..), Bind, Embed(..), Rebind, Rec, TRec, Shift(..), + ( -- * Names + Name, AnyName(..), - -- ** Utilities + -- ** Constructing and destructing free names integer2Name, string2Name, s2n, makeName, name2Integer, name2String, anyName2Integer, anyName2String, - name1,name2,name3,name4,name5,name6,name7,name8,name9,name10, - translate, + -- ** Dealing with name sorts + translate, toSortedName, - -- * The 'Alpha' class - Alpha(..), - swaps, swapsEmbeds, swapsBinders, + -- * 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 - Collection(..), Multiset(..), + -- ** 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, - -- * Binding operations - bind, unsafeUnbind, + -- *** Collections + Collection(..), Multiset(..), - -- * The 'Fresh' class - Fresh(..), freshen, - unbind, unbind2, unbind3, + -- ** 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, - -- * The 'LFresh' class - LFresh(..), + -- ** Local freshness lfreshen, - lunbind, lunbind2, lunbind3, + -- *** 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, - -- * Rebinding operations - rebind, unrebind, - - -- * Rec operations - rec, unrec, - trec, untrec, luntrec, + -- * The @Alpha@ class + Alpha(..), - -- XXX export embed, unembed, shift, unshift. - -- XXX should embed/unembed work for Shifts as well? + -- * Re-exported RepLib API for convenience - -- * Substitution - Subst(..), SubstName(..), + module Generics.RepLib, -- * Pay no attention to the man behind the curtain - -- $paynoattention + + -- | 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 @@ -86,8 +260,6 @@ import Unbound.LocallyNameless.Subst import Unbound.LocallyNameless.Ops import Unbound.Util +import Unbound.PermM --- $paynoattention --- These type representation objects are exported so they can be --- referenced by auto-generated code. Please pretend they do not --- exist. +import Generics.RepLib diff --git a/Unbound/LocallyNameless/Alpha.hs b/Unbound/LocallyNameless/Alpha.hs --- a/Unbound/LocallyNameless/Alpha.hs +++ b/Unbound/LocallyNameless/Alpha.hs @@ -1,12 +1,15 @@ {-# LANGUAGE RankNTypes , FlexibleContexts , GADTs + , TypeFamilies #-} ---------------------------------------------------------------------- -- | -- Module : Unbound.LocallyNameless.Alpha -- License : BSD-like (see LICENSE) +-- Maintainer : Brent Yorgey +-- Portability : GHC only (-XKitchenSink) -- ---------------------------------------------------------------------- @@ -65,16 +68,14 @@ -- The Alpha class ------------------------------------------------------------ --- | The 'Alpha' type class is for types which may contain names. The +-- | The @Alpha@ type class is for types which may contain names. The -- 'Rep1' constraint means that we can only make instances of this -- class for types that have generic representations (which can be -- automatically derived by RepLib.) -- --- Note that the methods of 'Alpha' should never be called directly! --- Instead, use other methods provided by this module which are --- defined in terms of 'Alpha' methods. (The only reason they are --- exported is to make them available to automatically-generated --- code.) +-- Note that the methods of @Alpha@ should almost never be called +-- directly. Instead, use other methods provided by this module +-- which are defined in terms of @Alpha@ methods. -- -- Most of the time, the default definitions of these methods will -- suffice, so you can make an instance for your data type by simply @@ -82,6 +83,29 @@ -- -- > instance Alpha MyType -- +-- Occasionally, however, it may be useful to override the default +-- implementations of one or more @Alpha@ methods for a particular +-- type. For example, consider a type like +-- +-- > data Term = ... +-- > | Annotation Stuff Term +-- +-- where the @Annotation@ constructor of @Term@ associates some sort +-- of annotation with a term --- say, information obtained from a +-- parser about where in an input file the term came from. This +-- information is needed to produce good error messages, but should +-- not be taken into consideration when, say, comparing two @Term@s +-- for alpha-equivalence. In order to make 'aeq' ignore +-- annotations, you can override the implementation of @aeq'@ like +-- so: +-- +-- > instance Alpha Term where +-- > aeq' c (Annotation _ t1) t2 = aeq' c t1 t2 +-- > aeq' c t1 (Annotation _ t2) = aeq' c t1 t2 +-- > aeq' c t1 t2 = aeqR1 rep1 t1 t2 +-- +-- Note how the call to 'aeqR1' handles all the other cases generically. +-- class (Show a, Rep1 AlphaD a) => Alpha a where -- | See 'swaps'. @@ -104,6 +128,10 @@ aeq' :: AlphaCtx -> a -> a -> Bool aeq' = aeqR1 rep1 + -- | See 'acompare'. + acompare' :: AlphaCtx -> a -> a -> Ordering + acompare' = acompareR1 rep1 + {- -- | See 'match'. match' :: AlphaCtx -> a -> a -> Maybe (Perm AnyName) @@ -118,13 +146,10 @@ open :: Alpha b => AlphaCtx -> b -> a -> a open = openR1 rep1 - -- | See 'acompare'. - acompare' :: AlphaCtx -> a -> a -> Ordering - acompare' = acompareR1 rep1 - -- | @isPat x@ dynamically checks whether @x@ can be used as a valid - -- pattern. The default instance returns @True@ if at all - -- possible. + -- pattern. The default instance returns @Just@ if at all + -- possible. If successful, returns a list of names bound by the + -- pattern. isPat :: a -> Maybe [AnyName] isPat = isPatR1 rep1 @@ -154,6 +179,32 @@ findpatrec :: a -> AnyName -> FindResult findpatrec = findpatR1 rep1 +-- | Type class for embedded terms (either @Embed@ or @Shift@). +class IsEmbed e where + type Embedded e :: * + + -- | Construct an embedded term, which is an instance of 'Embed' + -- with any number of enclosing 'Shift's. That is, @embed@ can have + -- any of the types + -- + -- * @t -> Embed t@ + -- + -- * @t -> Shift (Embed t)@ + -- + -- * @t -> Shift (Shift (Embed t))@ + -- + -- and so on. + embed :: Embedded e -> e + + -- | Destruct an embedded term. @unembed@ can have any of the types + -- + -- * @Embed t -> t@ + -- + -- * @Shift (Embed t) -> t@ + -- + -- and so on. + unembed :: e -> Embedded e + ------------------------------------------------------------ -- Pattern operation internals ------------------------------------------------------------ @@ -763,6 +814,12 @@ findpatrec _ _ = mempty nthpatrec _ = mempty +instance IsEmbed (Embed t) where + type Embedded (Embed t) = t + + embed = Embed + unembed (Embed t) = t + instance Alpha a => Alpha (Shift a) where -- The contents of Shift may only be an Embed or another Shift. @@ -773,6 +830,11 @@ close c b (Shift x) = Shift (close (decr c) b x) open c b (Shift x) = Shift (open (decr c) b x) +instance IsEmbed e => IsEmbed (Shift e) where + type Embedded (Shift e) = Embedded e + + embed = Shift . embed + unembed (Shift e) = unembed e -- Instances for other types use the default definitions. instance Alpha Bool diff --git a/Unbound/LocallyNameless/Fresh.hs b/Unbound/LocallyNameless/Fresh.hs --- a/Unbound/LocallyNameless/Fresh.hs +++ b/Unbound/LocallyNameless/Fresh.hs @@ -71,9 +71,11 @@ -- Fresh ------------------------------------------------------------ --- | Type class for monads which can generate new globally unique --- 'Name's based on a given 'Name'. +-- | The @Fresh@ type class governs monads which can generate new +-- globally unique 'Name's based on a given 'Name'. class Monad m => Fresh m where + + -- | Generate a new globally unique name based on the given one. fresh :: Name a -> m (Name a) -- | The @FreshM@ monad transformer. Keeps track of the lowest index @@ -82,7 +84,7 @@ newtype FreshMT m a = FreshMT { unFreshMT :: St.StateT Integer m a } deriving (Functor, Applicative, Monad, St.MonadState Integer, MonadPlus, MonadIO) --- | Run a 'FreshMT' computation starting in an empty context. +-- | Run a 'FreshMT' computation (with the global index starting at zero). runFreshMT :: Monad m => FreshMT m a -> m a runFreshMT m = contFreshMT m 0 @@ -102,7 +104,7 @@ -- incremented every time 'fresh' is called. type FreshM = FreshMT Identity --- | Run a FreshM computation in an empty context. +-- | Run a FreshM computation (with the global index starting at zero). runFreshM :: FreshM a -> a runFreshM = runIdentity . runFreshMT @@ -166,27 +168,19 @@ -- LFresh --------------------------------------------------- --- XXX todo: generalize 'avoid' to take an arbitrary term/pattern? --- would make the modules recursive though... -- | This is the class of monads that support freshness in an -- (implicit) local scope. Generated names are fresh for the current --- local scope, but not globally fresh. +-- local scope, not necessarily globally fresh. class Monad m => LFresh m where -- | Pick a new name that is fresh for the current (implicit) scope. lfresh :: Rep a => Name a -> m (Name a) - -- | Avoid the given names when freshening in the subcomputation. + -- | Avoid the given names when freshening in the subcomputation, + -- that is, add the given names to the in-scope set. avoid :: [AnyName] -> m a -> m a --- | A simple reader monad instance for 'LFresh'. -instance LFresh (Reader Integer) where - lfresh (Nm r (s,j)) = do { n <- ask; return (Nm r (s, max j (n+1))) } - avoid [] = id - avoid names = local (max k) - where k = maximum (map anyName2Integer names) - -- | The LFresh monad transformer. Keeps track of a set of names to --- avoid, and when asked for a fresh one will choose the first unused --- numerical name. +-- avoid, and when asked for a fresh one will choose the first numeric +-- prefix of the given name which is currently unused. newtype LFreshMT m a = LFreshMT { unLFreshMT :: ReaderT (Set AnyName) m a } deriving (Functor, Applicative, Monad, MonadReader (Set AnyName), MonadIO, MonadPlus) diff --git a/Unbound/LocallyNameless/Name.hs b/Unbound/LocallyNameless/Name.hs --- a/Unbound/LocallyNameless/Name.hs +++ b/Unbound/LocallyNameless/Name.hs @@ -11,17 +11,41 @@ -- | -- Module : Unbound.LocallyNameless.Name -- License : BSD-like (see LICENSE) --- --- Maintainer : Stephanie Weirich --- Stability : experimental --- Portability : XXX +-- Maintainer : Brent Yorgey +-- Portability : GHC only -- --- XXX write me +-- An implementation of names in a locally nameless representation. ---------------------------------------------------------------------- -module Unbound.LocallyNameless.Name where --- XXX todo make explicit export list +module Unbound.LocallyNameless.Name + ( -- * Name types + Name(..) + , AnyName(..) + + -- * Constructing and destructing free names + + , integer2Name, string2Name, s2n, makeName + + , name2Integer, name2String + , anyName2Integer, anyName2String + + -- * Sorts + + , toSortedName, translate, getR + + -- * Utility + + , isBound, isFree + + -- * Representations + -- | Automatically generated representation objects. + + , rR, rR1 + , rName, rName1 + , rAnyName, rAnyName1 + ) where + import Generics.RepLib $(derive_abstract [''R]) @@ -29,9 +53,12 @@ -- | 'Name's are things that get bound. This type is intentionally -- abstract; to create a 'Name' you can use 'string2Name' or --- 'integer2Name'. The type parameter is a tag, or /sort/, which tells --- us what sorts of things this name may stand for. The sort must --- be an instance of the 'Rep' type class. +-- 'integer2Name'. The type parameter is a tag, or /sort/, which +-- tells us what sorts of things this name may stand for. The sort +-- must be a /representable/ type, /i.e./ an instance of the 'Rep' +-- type class from the @RepLib@ generic programming framework. +-- +-- To hide the sort of a name, use 'AnyName'. data Name a = Nm (R a) (String, Integer) -- free names | Bn (R a) Integer Integer -- bound names / binding level + pattern index @@ -39,13 +66,24 @@ $(derive [''Name]) --- | A name with a hidden (existentially quantified) sort. +-- | A name with a hidden (existentially quantified) sort. To hide +-- the sort of a name, use the 'AnyName' constructor directly; to +-- extract a name with a hidden sort, use 'toSortedName'. data AnyName = forall a. Rep a => AnyName (Name a) +-- | Test whether a name is a bound variable (i.e. a reference to some +-- binding site, represented as a de Bruijn index). Normal users of +-- the library should not need this function, as it is impossible to +-- encounter a bound name when using the abstract interface provided +-- by "Unbound.LocallyNameless". isBound :: Name a -> Bool isBound (Nm _ _) = False isBound (Bn _ _ _) = True +-- | Test whether a name is a free variable. Normal users of the +-- library should not need this function, as all the names +-- encountered will be free variables when using the abstract +-- interface provided by "Unbound.LocallyNameless". isFree :: Name a -> Bool isFree (Nm _ _) = True isFree (Bn _ _ _) = False @@ -76,21 +114,6 @@ -- Utilities ------------------------------------------------------------ --- some convenient names for testing -name1, name2, name3, name4, name5, name6, name7, name8, name9, name10, name11 - :: Rep a => Name a -name1 = integer2Name 1 -name2 = integer2Name 2 -name3 = integer2Name 3 -name4 = integer2Name 4 -name5 = integer2Name 5 -name6 = integer2Name 6 -name7 = integer2Name 7 -name8 = integer2Name 8 -name9 = integer2Name 9 -name10 = integer2Name 10 -name11 = integer2Name 11 - --instance Read Name where -- read s = error "FIXME" @@ -118,14 +141,16 @@ anyName2String :: AnyName -> String anyName2String (AnyName nm) = name2String nm +-- | Cast a name with an existentially hidden sort to an explicitly +-- sorted name. toSortedName :: Rep a => AnyName -> Maybe (Name a) toSortedName (AnyName n) = gcastR (getR n) rep n --- | Create a 'Name' from an 'Integer'. +-- | Create a free 'Name' from an 'Integer'. integer2Name :: Rep a => Integer -> Name a integer2Name n = makeName "" n --- | Create a 'Name' from a 'String'. +-- | Create a free 'Name' from a 'String'. string2Name :: Rep a => String -> Name a string2Name s = makeName s 0 @@ -133,7 +158,7 @@ s2n :: Rep a => String -> Name a s2n = string2Name --- | Create a 'Name' from a @String@ and an @Integer@ index. +-- | Create a free 'Name' from a @String@ and an @Integer@ index. makeName :: Rep a => String -> Integer -> Name a makeName s i = Nm rep (s,i) @@ -142,7 +167,7 @@ getR (Nm r _) = r getR (Bn r _ _) = r --- | Change the sort of a name +-- | Change the sort of a name. translate :: (Rep b) => Name a -> Name b translate (Nm _ x) = Nm rep x translate (Bn _ x y) = Bn rep x y diff --git a/Unbound/LocallyNameless/Ops.hs b/Unbound/LocallyNameless/Ops.hs --- a/Unbound/LocallyNameless/Ops.hs +++ b/Unbound/LocallyNameless/Ops.hs @@ -1,3 +1,14 @@ + +---------------------------------------------------------------------- +-- | +-- Module : Unbound.LocallyNameless.Ops +-- License : BSD-like (see LICENSE) +-- Maintainer : Brent Yorgey +-- Portability : GHC only (-XKitchenSink) +-- +-- Generic operations defined in terms of the RepLib framework and the +-- 'Alpha' type class. +---------------------------------------------------------------------- module Unbound.LocallyNameless.Ops where import Generics.RepLib @@ -15,10 +26,12 @@ -- Binding operations ---------------------------------------------------------- --- | A smart constructor for binders, also sometimes known as --- \"close\". -bind :: (Alpha c, Alpha b) => b -> c -> Bind b c -bind b c = B b (closeT b c) +-- | A smart constructor for binders, also sometimes referred to as +-- \"close\". Free variables in the term are taken to be references +-- to matching binders in the pattern. (Free variables with no +-- matching binders will remain free.) +bind :: (Alpha p, Alpha t) => p -> t -> Bind p t +bind p t = B p (closeT p t) -- | A destructor for binders that does /not/ guarantee fresh -- names for the binders. @@ -40,41 +53,49 @@ -- Rebinding operations ---------------------------------------------------------- --- | Constructor for binding in patterns. -rebind :: (Alpha a, Alpha b) => a -> b -> Rebind a b -rebind a b = R a (closeP a b) +-- | Constructor for rebinding patterns. +rebind :: (Alpha p1, Alpha p2) => p1 -> p2 -> Rebind p1 p2 +rebind p1 p2 = R p1 (closeP p1 p2) -- | Compare for alpha-equality. -instance (Alpha a, Alpha b, Eq b) => Eq (Rebind a b) where +instance (Alpha p1, Alpha p2, Eq p2) => Eq (Rebind p1 p2) where b1 == b2 = b1 `aeqBinders` b2 --- | Destructor for `Rebind`. It does not need a monadic context for --- generating fresh names, since `Rebind` can only occur in the --- pattern of a `Bind`; hence a previous call to `open` must have --- already freshened the names at this point. -unrebind :: (Alpha a, Alpha b) => Rebind a b -> (a, b) -unrebind (R a b) = (a, openP a b) +-- | Destructor for rebinding patterns. It does not need a monadic +-- context for generating fresh names, since @Rebind@ can only occur +-- in the pattern of a 'Bind'; hence a previous call to 'unbind' (or +-- something similar) must have already freshened the names at this +-- point. +unrebind :: (Alpha p1, Alpha p2) => Rebind p1 p2 -> (p1, p2) +unrebind (R p1 p2) = (p1, openP p1 p2) ---------------------------------------------------------- -- Rec operations ---------------------------------------------------------- -rec :: (Alpha a) => a -> Rec a -rec a = Rec (closeP a a) where +-- | Constructor for recursive patterns. +rec :: (Alpha p) => p -> Rec p +rec p = Rec (closeP p p) where -unrec :: (Alpha a) => Rec a -> a -unrec (Rec a) = openP a a +-- | Destructor for recursive patterns. +unrec :: (Alpha p) => Rec p -> p +unrec (Rec p) = openP p p ---------------------------------------------------------- -- TRec operations ---------------------------------------------------------- +-- | Constructor for recursive abstractions. trec :: Alpha p => p -> TRec p trec p = TRec $ bind (rec p) () +-- | Destructor for recursive abstractions which picks globally fresh +-- names for the binders. untrec :: (Fresh m, Alpha p) => TRec p -> m p untrec (TRec b) = (unrec . fst) `liftM` unbind b +-- | Destructor for recursive abstractions which picks /locally/ fresh +-- names for binders (see 'LFresh'). luntrec :: (LFresh m, Alpha p) => TRec p -> m p luntrec (TRec b) = lunbind b $ return . unrec . fst @@ -82,12 +103,13 @@ -- Wrappers for operations in the Alpha class ---------------------------------------------------------- --- | Determine alpha-equivalence of terms. +-- | Determine the alpha-equivalence of two terms. aeq :: Alpha t => t -> t -> Bool aeq t1 t2 = aeq' initial t1 t2 -- | Determine (alpha-)equivalence of patterns. Do they bind the same --- variables and have alpha-equal annotations? +-- variables in the same patterns and have alpha-equivalent +-- annotations in matching positions? aeqBinders :: Alpha p => p -> p -> Bool aeqBinders p1 p2 = aeq' initial p1 p2 @@ -107,13 +129,13 @@ . cmap toSortedName . fvAny --- | Calculate the variables (of any sort) that occur freely within --- pattern annotations (but are not bound by the pattern). +-- | Calculate the variables (of any sort) that occur freely in terms +-- embedded within a pattern (but are not bound by the pattern). patfvAny :: (Alpha p, Collection f) => p -> f AnyName patfvAny = fv' (pat initial) -- | Calculate the variables of a particular sort that occur freely in --- pattern annotations (but are not bound by the pattern). +-- terms embedded within a pattern (but are not bound by the pattern). patfv :: (Rep a, Alpha p, Collection f) => p -> f (Name a) patfv = filterC . cmap toSortedName @@ -130,30 +152,31 @@ -- | Apply a permutation to a term. -swaps :: Alpha a => Perm AnyName -> a -> a +swaps :: Alpha t => Perm AnyName -> t -> t swaps = swaps' initial -- | Apply a permutation to the binding variables in a pattern. --- Embedded terms are left alone by the permutation. -swapsBinders :: Alpha a => Perm AnyName -> a -> a +-- Embedded terms are left alone by the permutation. +swapsBinders :: Alpha p => Perm AnyName -> p -> p swapsBinders = swaps' initial --- | Apply a permutation to the annotations in a pattern. Binding --- names are left alone by the permutation. -swapsEmbeds :: Alpha a => Perm AnyName -> a -> a +-- | Apply a permutation to the embedded terms in a pattern. Binding +-- names are left alone by the permutation. +swapsEmbeds :: Alpha p => Perm AnyName -> p -> p swapsEmbeds = swaps' (pat initial) - --- | \"Locally\" freshen a pattern replacing all binding names with --- new names that have not already been used. The second argument is --- a continuation, which takes the renamed term and a permutation that --- specifies how the pattern has been renamed. +-- | \"Locally\" freshen a pattern, replacing all binding names with +-- new names that are not already \"in scope\". The second argument +-- is a continuation, which takes the renamed term and a permutation +-- that specifies how the pattern has been renamed. The resulting +-- computation will be run with the in-scope set extended by the +-- names just generated. lfreshen :: (Alpha p, LFresh m) => p -> (p -> Perm AnyName -> m b) -> m b lfreshen = lfreshen' (pat initial) --- | Freshen a pattern by replacing all old /binding/ 'Name's with new --- fresh 'Name's, returning a new pattern and a @'Perm' 'Name'@ --- specifying how 'Name's were replaced. +-- | Freshen a pattern by replacing all old binding 'Name's with new +-- fresh 'Name's, returning a new pattern and a @'Perm' 'Name'@ +-- specifying how 'Name's were replaced. freshen :: (Alpha p, Fresh m) => p -> m (p, Perm AnyName) freshen = freshen' (pat initial) @@ -183,16 +206,21 @@ -- Opening binders ------------------------------------------------------------ --- | Unbind (also known as \"open\") is the destructor for --- bindings. It ensures that the names in the binding are fresh. -unbind :: (Fresh m, Alpha p, Alpha t) => Bind p t -> m (p,t) +-- | Unbind (also known as \"open\") is the simplest destructor for +-- bindings. It ensures that the names in the binding are globally +-- fresh, using a monad which is an instance of the 'Fresh' type +-- class. +unbind :: (Fresh m, Alpha p, Alpha t) => Bind p t -> m (p,t) unbind (B p t) = do (p', _) <- freshen p return (p', openT p' t) --- | Unbind two terms with the same fresh names, provided the --- binders have the same number of binding variables. -unbind2 :: (Fresh m, Alpha p1, Alpha p2, Alpha t1, Alpha t2) => +-- | Unbind two terms with the /same/ fresh names, provided the +-- binders have the same number of binding variables. If the +-- patterns have different numbers of binding variables, return +-- @Nothing@. Otherwise, return the renamed patterns and the +-- associated terms. +unbind2 :: (Fresh m, Alpha p1, Alpha p2, Alpha t1, Alpha t2) => Bind p1 t1 -> Bind p2 t2 -> m (Maybe (p1,t1,p2,t2)) unbind2 (B p1 t1) (B p2 t2) = do case mkPerm (fvAny p1) (fvAny p2) of @@ -203,8 +231,9 @@ Nothing -> return Nothing -- | Unbind three terms with the same fresh names, provided the --- binders have the same number of binding variables. -unbind3 :: (Fresh m, Alpha p1, Alpha p2, Alpha p3, Alpha t1, Alpha t2, Alpha t3) => +-- binders have the same number of binding variables. See the +-- documentation for 'unbind2' for more details. +unbind3 :: (Fresh m, Alpha p1, Alpha p2, Alpha p3, Alpha t1, Alpha t2, Alpha t3) => Bind p1 t1 -> Bind p2 t2 -> Bind p3 t3 -> m (Maybe (p1,t1,p2,t2,p3,t3)) unbind3 (B p1 t1) (B p2 t2) (B p3 t3) = do case ( mkPerm (fvAny p1) (fvAny p2) @@ -216,14 +245,22 @@ swaps (p' <> pm13) p3, openT p1' t3) _ -> return Nothing --- | Destruct a binding in an 'LFresh' monad. +-- | @lunbind@ opens a binding in an 'LFresh' monad, ensuring that the +-- names chosen for the binders are /locally/ fresh. The components +-- of the binding are passed to a /continuation/, and the resulting +-- monadic action is run in a context extended to avoid choosing new +-- names which are the same as the ones chosen for this binding. +-- +-- For more information, see the documentation for the 'LFresh' type +-- class. lunbind :: (LFresh m, Alpha p, Alpha t) => Bind p t -> ((p, t) -> m c) -> m c lunbind (B p t) g = lfreshen p (\x _ -> g (x, openT x t)) --- | Unbind two terms with the same fresh names, provided the --- binders have the same number of binding variables. +-- | Unbind two terms with the same locally fresh names, provided the +-- patterns have the same number of binding variables. See the +-- documentation for 'unbind2' and 'lunbind' for more details. lunbind2 :: (LFresh m, Alpha p1, Alpha p2, Alpha t1, Alpha t2) => Bind p1 t1 -> Bind p2 t2 -> (Maybe (p1,t1,p2,t2) -> m r) -> m r lunbind2 (B p1 t1) (B p2 t2) g = @@ -233,8 +270,9 @@ swaps (pm2 <> pm1) p2, openT p1' t2)) Nothing -> g Nothing --- | Unbind three terms with the same fresh names, provided the --- binders have the same number of binding variables. +-- | Unbind three terms with the same locally fresh names, provided +-- the binders have the same number of binding variables. See the +-- documentation for 'unbind2' and 'lunbind' for more details. lunbind3 :: (LFresh m, Alpha p1, Alpha p2, Alpha p3, Alpha t1, Alpha t2, Alpha t3) => Bind p1 t1 -> Bind p2 t2 -> Bind p3 t3 -> (Maybe (p1,t1,p2,t2,p3,t3) -> m r) -> diff --git a/Unbound/LocallyNameless/Subst.hs b/Unbound/LocallyNameless/Subst.hs --- a/Unbound/LocallyNameless/Subst.hs +++ b/Unbound/LocallyNameless/Subst.hs @@ -6,6 +6,15 @@ , ScopedTypeVariables #-} +---------------------------------------------------------------------- +-- | +-- Module : Unbound.LocallyNameless.Subst +-- License : BSD-like (see LICENSE) +-- Maintainer : Brent Yorgey +-- Portability : GHC only (-XKitchenSink) +-- +-- The @Subst@ type class for generic capture-avoiding substitution. +---------------------------------------------------------------------- module Unbound.LocallyNameless.Subst where import Data.List (find) @@ -22,19 +31,21 @@ data SubstName a b where SubstName :: (a ~ b) => Name a -> SubstName a b --- | The 'Subst' class governs capture-avoiding substitution. To +-- | The @Subst@ class governs capture-avoiding substitution. To -- derive this class, you only need to indicate where the variables -- are in the data type, by overriding the method 'isvar'. class (Rep1 (SubstD b) a) => Subst b a where - -- | If the argument is a variable, return its name wrapped in the - -- 'SubstName' constructor. Return 'Nothing' for non-variable - -- arguments. The default implementation always returns - -- 'Nothing'. + -- | This is the only method which normally needs to be implemented + -- explicitly. If the argument is a variable, return its name + -- wrapped in the 'SubstName' constructor. Return 'Nothing' for + -- non-variable arguments. The default implementation always + -- returns 'Nothing'. isvar :: a -> Maybe (SubstName a b) isvar x = Nothing - -- | @'subst' nm sub tm@ substitutes @sub@ for @nm@ in @tm@. + -- | @'subst' nm sub tm@ substitutes @sub@ for @nm@ in @tm@. It has + -- a default generic implementation in terms of @isvar@. subst :: Name b -> b -> a -> a subst n u x | isFree n = case (isvar x :: Maybe (SubstName a b)) of @@ -42,7 +53,8 @@ Nothing -> substR1 rep1 n u x subst m u x = error $ "Cannot substitute for bound variable " ++ show m - -- | Perform several simultaneous substitutions. + -- | Perform several simultaneous substitutions. This method also + -- has a default generic implementation in terms of @isvar@. substs :: [(Name b, b)] -> a -> a substs ss x | all (isFree . fst) ss = diff --git a/Unbound/LocallyNameless/Test.hs b/Unbound/LocallyNameless/Test.hs --- a/Unbound/LocallyNameless/Test.hs +++ b/Unbound/LocallyNameless/Test.hs @@ -6,15 +6,14 @@ , UndecidableInstances #-} -module Generics.RepLib.Bind.LocallyNameless.Test where +module Unbound.LocallyNameless.Test where import qualified Data.Set as S -import Generics.RepLib hiding (GT) -import Generics.RepLib.Bind.LocallyNameless -import Generics.RepLib.Bind.LocallyNameless.Alpha -import Generics.RepLib.Bind.LocallyNameless.Name -import Generics.RepLib.Bind.PermM +import Unbound.LocallyNameless hiding (GT) +import Unbound.LocallyNameless.Alpha +import Unbound.LocallyNameless.Name +import Unbound.PermM -------------------- TESTING CODE -------------------------------- data Exp = V (Name Exp) @@ -73,7 +72,7 @@ assert "a14" $ bind (rebind (Embed nameA) ()) () `naeq` bind (rebind (Embed nameB) ()) () assert "a15" $ (rebind (nameA, Embed nameA) ()) `naeq` - (rebind (name4, Embed nameC) ()) + (rebind (nameA, Embed nameC) ()) assert "a16" $ bind (nameA, nameB) nameA `naeq` bind (nameB, nameA) nameA assert "a17" $ bind (nameA, nameB) nameA `naeq` bind (nameA, nameB) nameB assert "a18" $ (nameA, nameA) `naeq` (nameA, nameB) @@ -101,8 +100,8 @@ L (bind n (mkbig names (A (V n) body))) mkbig [] body = body -big1 = mkbig (map integer2Name (take 100 [1 ..])) (V name11) -big2 = mkbig (map integer2Name (take 101 [1 ..])) (V name11) +big1 = mkbig (map integer2Name (take 100 [1 ..])) (V nameA) +big2 = mkbig (map integer2Name (take 101 [1 ..])) (V nameA) tests_nth = do @@ -116,7 +115,7 @@ tests_big = do assert "b1" $ big1 `naeq` big2 assert "b2" $ fv big1 == emptyNE - assert "b3" $ big1 `aeq` subst name11 (V name11) big1 + assert "b3" $ big1 `aeq` subst nameA (V nameA) big1 tests_acompare = do -- Names compare in the obvious way. diff --git a/Unbound/LocallyNameless/Types.hs b/Unbound/LocallyNameless/Types.hs --- a/Unbound/LocallyNameless/Types.hs +++ b/Unbound/LocallyNameless/Types.hs @@ -5,6 +5,18 @@ , MultiParamTypeClasses #-} +---------------------------------------------------------------------- +-- | +-- Module : Unbound.LocallyNameless.Types +-- License : BSD-like (see LICENSE) +-- +-- Maintainer : Brent Yorgey +-- Stability : experimental +-- Portability : GHC only +-- +-- Special type combinators for specifying binding structure. +---------------------------------------------------------------------- + module Unbound.LocallyNameless.Types ( Bind(..) , Rebind(..) @@ -15,7 +27,11 @@ , module Unbound.LocallyNameless.Name -- * Pay no attention to the man behind the curtain - -- $paynoattention + + -- | These type representation objects are exported so they can be + -- referenced by auto-generated code. Please pretend they do not + -- exist. + , rBind, rRebind, rEmbed, rRec, rShift ) where @@ -29,10 +45,9 @@ -- Bind -------------------------------------------------- --- | The type of a binding. We can 'Bind' an @a@ object in a @b@ --- object if we can create \"fresh\" @a@ objects, and @a@ objects --- can occur unbound in @b@ objects. Often @a@ is 'Name' but that --- need not be the case. +-- | The most fundamental combinator for expressing binding structure +-- is 'Bind'. The /term type/ @Bind p t@ represents a pattern @p@ +-- paired with a term @t@, where names in @p@ are bound within @t@. -- -- Like 'Name', 'Bind' is also abstract. You can create bindings -- using 'bind' and take them apart with 'unbind' and friends. @@ -47,8 +62,11 @@ -- Rebind -------------------------------------------------- --- | 'Rebind' supports \"telescopes\" --- that is, patterns where --- bound variables appear in multiple subterms. +-- | @Rebind@ allows for /nested/ bindings. If @p1@ and @p2@ are +-- pattern types, then @Rebind p1 p2@ is also a pattern type, +-- similar to the pattern type @(p1,p2)@ except that @p1@ +-- /scopes over/ @p2@. That is, names within terms embedded in @p2@ +-- may refer to binders in @p1@. data Rebind p1 p2 = R p1 p2 instance (Show a, Show b) => Show (Rebind a b) where @@ -58,9 +76,10 @@ -- Rec -------------------------------------------------- --- | 'Rec' supports recursive patterns --- that is, patterns where --- any variables anywhere in the pattern are bound in the pattern --- itself. Useful for lectrec (and Agda's dot notation). +-- | If @p@ is a pattern type, then @Rec p@ is also a pattern type, +-- which is /recursive/ in the sense that @p@ may bind names in terms +-- embedded within itself. Useful for encoding e.g. lectrec and +-- Agda's dot notation. data Rec p = Rec p instance Show a => Show (Rec a) where @@ -69,10 +88,14 @@ -- TRec -------------------------------------------------- --- | 'TRec' is a standalone variant of 'Rec' -- that is, if @p@ is a --- pattern type then @TRec p@ is a term type. It is isomorphic to --- @Bind (Rec p) ()@. - +-- | @TRec@ is a standalone variant of 'Rec': the only difference is +-- that whereas @'Rec' p@ is a pattern type, @TRec p@ +-- is a /term type/. It is isomorphic to @'Bind' ('Rec' p) ()@. +-- +-- Note that @TRec@ corresponds to Pottier's /abstraction/ construct +-- from alpha-Caml. In this context, @'Embed' t@ corresponds to +-- alpha-Caml's @inner t@, and @'Shift' ('Embed' t)@ corresponds to +-- alpha-Caml's @outer t@. newtype TRec p = TRec (Bind (Rec p) ()) instance Show a => Show (TRec a) where @@ -82,12 +105,18 @@ -- Embed -------------------------------------------------- --- XXX improve this doc --- | An annotation is a \"hole\" in a pattern where variables can be --- used, but not bound. For example, patterns may include type --- annotations, and those annotations can reference variables --- without binding them. Annotations do nothing special when they --- appear elsewhere in terms. +-- | @Embed@ allows for terms to be /embedded/ within patterns. Such +-- embedded terms do not bind names along with the rest of the +-- pattern. For examples, see the tutorial or examples directories. +-- +-- If @t@ is a /term type/, then @Embed t@ is a /pattern type/. +-- +-- @Embed@ is not abstract since it involves no binding, and hence +-- it is safe to manipulate directly. To create and destruct +-- @Embed@ terms, you may use the @Embed@ constructor directly. +-- (You may also use the functions 'embed' and 'unembed', which +-- additionally can construct or destruct any number of enclosing +-- 'Shift's at the same time.) newtype Embed t = Embed t deriving Eq instance Show a => Show (Embed a) where @@ -102,10 +131,7 @@ instance Show a => Show (Shift a) where showsPrec p (Shift a) = showString "{" . showsPrec 0 a . showString "}" --- $paynoattention --- These type representation objects are exported so they can be --- referenced by auto-generated code. Please pretend they do not --- exist. +-- Pay no attention... $(derive [''Bind, ''Embed, ''Rebind, ''Rec, ''Shift]) diff --git a/Unbound/Nominal.hs b/Unbound/Nominal.hs --- a/Unbound/Nominal.hs +++ b/Unbound/Nominal.hs @@ -2,24 +2,21 @@ -- | -- Module : Unbound.Nominal -- License : BSD-like (see LICENSE) --- -- Maintainer : Stephanie Weirich -- Stability : experimental -- Portability : non-portable (-XKitchenSink) -- --- Generic implementation of name binding functions, based on the library --- RepLib. This version uses a nominal representation of binding structure. --- --- DISCLAIMER: this module probably contains bugs and may be --- slower than "Unbound.LocallyNameless". At this point --- we recommend it only for the curious or intrepid. +-- A generic implementation of standard functions dealing with names +-- and binding structure (alpha equivalence, free variable +-- calculation, capture-avoiding substitution, name permutation, ...) +-- using a nominal representation. -- --- Datatypes with binding defined using the 'Name' and 'Bind' types. --- Important classes are --- 'Alpha' -- the class of types that include binders. --- These classes are generic, and default implementations exist for all --- representable types. This file also defines a third generic class, --- 'Subst' -- for subtitution functions. +-- DISCLAIMER: this module almost certainly contains bugs and may be +-- slower than "Unbound.LocallyNameless". The documentation is also +-- sparse and likely out of date. At this point we recommend it only +-- for the curious or intrepid. We are actively working on bringing +-- it up to speed as a viable alternative to +-- "Unbound.LocallyNameless". -- -------------------------------------------------------------------------- module Unbound.Nominal @@ -63,7 +60,10 @@ AlphaCtx, matchR1, -- * Pay no attention to the man behind the curtain - -- $paynoattention + + -- | 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.Nominal.Name diff --git a/Unbound/PermM.hs b/Unbound/PermM.hs --- a/Unbound/PermM.hs +++ b/Unbound/PermM.hs @@ -1,11 +1,8 @@ ---------------------------------------------------------------------- -- | -- Module : Unbound.Perm --- Copyright : ??? --- License : BSD --- +-- License : BSD-like (see LICENSE) -- Maintainer : Stephanie Weirich --- Stability : experimental -- Portability : portable -- -- A slow, but hopefully correct implementation of permutations. @@ -25,6 +22,10 @@ (<>) :: Monoid m => m -> m -> m (<>) = mappend +-- | A /permutation/ is a bijective function from names to names +-- which is the identity on all but a finite set of names. They +-- form the basis for nominal approaches to binding, but can +-- also be useful in general. newtype Perm a = Perm (Map a a) instance Ord a => Eq (Perm a) where @@ -35,13 +36,16 @@ instance Show a => Show (Perm a) where show (Perm p) = show p +-- | Apply a permutation to an element of the domain. apply :: Ord a => Perm a -> a -> a apply (Perm p) x = Map.findWithDefault x x p +-- | Create a permutation which swaps two elements. single :: Ord a => a -> a -> Perm a single x y = if x == y then Perm Map.empty else Perm (Map.insert x y (Map.insert y x Map.empty)) +-- | The empty (identity) permutation. empty :: Perm a empty = Perm Map.empty @@ -52,17 +56,19 @@ Perm (Map.fromList ([ (x,Map.findWithDefault y y b) | (x,y) <- Map.toList a] ++ [ (x, Map.findWithDefault x x b) | x <- Map.keys b, Map.notMember x a])) +-- | Permutations form a monoid under composition. instance Ord a => Monoid (Perm a) where mempty = empty mappend = compose --- | isid -- do all keys map to themselves? +-- | Is this the identity permutation? isid :: Ord a => Perm a -> Bool isid (Perm p) = Map.foldrWithKey (\ a b r -> r && a == b) True p --- | Join two permutation. Fail if the two permutations map the same --- name to two different variables. +-- | /Join/ two permutations by taking the union of their relation +-- graphs. Fail if they are inconsistent, i.e. map the same element +-- to two different elements. join :: Ord a => Perm a -> Perm a -> Maybe (Perm a) join (Perm p1) (Perm p2) = let overlap = Map.intersectionWith (==) p1 p2 in @@ -70,9 +76,12 @@ Just (Perm (Map.union p1 p2)) else Nothing +-- | The /support/ of a permutation is the set of elements which are +-- not fixed. support :: Ord a => Perm a -> [a] support (Perm p) = [ x | x <- Map.keys p, Map.findWithDefault x x p /= x] +-- | Restrict a permutation to a certain domain. restrict :: Ord a => Perm a -> [a] -> Perm a restrict (Perm p) l = Perm (foldl' (\p' k -> Map.delete k p') p l) diff --git a/Unbound/Util.hs b/Unbound/Util.hs --- a/Unbound/Util.hs +++ b/Unbound/Util.hs @@ -1,3 +1,13 @@ +---------------------------------------------------------------------- +-- | +-- Module : Unbound.Util +-- License : BSD-like (see LICENSE) +-- Maintainer : Brent Yorgey +-- Portability : GHC only (-XKitchenSink) +-- +-- Various utilities for the Unbound library. +---------------------------------------------------------------------- + module Unbound.Util where import Data.Maybe (catMaybes) @@ -21,12 +31,23 @@ -- | Collections are foldable types that support empty, singleton, -- union, and map operations. The result of a free variable -- calculation may be any collection. Instances are provided for --- lists and sets. +-- lists, sets, and multisets. class F.Foldable f => Collection f where + + -- | An empty collection. Must be the identity for @union@. emptyC :: f a + + -- | Create a singleton collection. singleton :: a -> f a + + -- | An associative combining operation. The @Ord@ constraint is in + -- order to accommodate sets. union :: Ord a => f a -> f a -> f a + + -- | Collections must be functorial. The normal @Functor@ class + -- won't do because of the @Ord@ constraint on sets. cmap :: (Ord a, Ord b) => (a -> b) -> f a -> f b + -- | Combine a list of containers into one. unions :: (Ord a, Collection f) => [f a] -> f a diff --git a/examples/Basic.hs b/examples/Basic.hs --- a/examples/Basic.hs +++ b/examples/Basic.hs @@ -1,4 +1,3 @@ --- OPTIONS -fglasgow-exts -fth -fallow-undecidable-instances {-# LANGUAGE TemplateHaskell, UndecidableInstances, ScopedTypeVariables, FlexibleInstances, MultiParamTypeClasses #-} ----------------------------------------------------------------------------- -- | diff --git a/examples/DepCalc.hs b/examples/DepCalc.hs --- a/examples/DepCalc.hs +++ b/examples/DepCalc.hs @@ -91,9 +91,7 @@ -} - -import Generics.RepLib -import Generics.RepLib.Bind.LocallyNameless +import Unbound.LocallyNameless import Data.Monoid import Control.Monad @@ -125,7 +123,7 @@ deriving Show data Tele = Empty - | Cons (Rebind (Name Exp, Annot Exp) Tele) + | Cons (Rebind (Name Exp, Embed Exp) Tele) deriving Show type Ctx = [ (Name Exp, Exp) ] @@ -162,7 +160,7 @@ mkTele :: [(String, Exp)] -> Tele mkTele [] = Empty -mkTele ((x,e) : t) = Cons (rebind (string2Name x, Annot e) (mkTele t)) +mkTele ((x,e) : t) = Cons (rebind (string2Name x, Embed e) (mkTele t)) {- Polymorphic identity function -} @@ -218,7 +216,7 @@ checkTele :: Ctx -> Tele -> M Ctx checkTele g Empty = return g checkTele g (Cons rb) = do - let ((x,Annot t), tele) = unrebind rb + let ((x,Embed t), tele) = unrebind rb a <- infer g t check g a EStar checkTele ((x,t) : g) tele @@ -279,7 +277,7 @@ checks :: Ctx -> [Exp] -> Tele -> M () checks _ [] Empty = ok checks g (e:es) (Cons rb) = do - let ((x, Annot a), t') = unrebind rb + let ((x, Embed a), t') = unrebind rb check g e a checks (subst x e g) (subst x e es) (subst x e t') checks _ _ _ = throwError $ "Unequal number of parameters and arguments" diff --git a/examples/F.hs b/examples/F.hs --- a/examples/F.hs +++ b/examples/F.hs @@ -1,31 +1,31 @@ -{-# LANGUAGE TemplateHaskell, +{-# LANGUAGE TemplateHaskell, ScopedTypeVariables, FlexibleInstances, MultiParamTypeClasses, FlexibleContexts, - UndecidableInstances, + UndecidableInstances, GADTs #-} module F where -import Generics.RepLib -import Generics.RepLib.Bind.LocallyNameless +import Unbound.LocallyNameless + import Control.Monad import Control.Monad.Trans.Error import Data.List as List --- System F with type and term variables +-- System F with type and term variables type TyName = Name Ty type TmName = Name Tm data Ty = TyVar TyName - | Arr Ty Ty + | Arr Ty Ty | All (Bind TyName Ty) deriving Show data Tm = TmVar TmName - | Lam (Bind (TmName, Annot Ty) Tm) + | Lam (Bind (TmName, Embed Ty) Tm) | TLam (Bind TyName Tm) | App Tm Tm | TApp Tm Ty @@ -33,8 +33,8 @@ $(derive [''Ty, ''Tm]) ------------------------------------------------------- -instance Alpha Ty where +------------------------------------------------------ +instance Alpha Ty where instance Alpha Tm where instance Subst Tm Ty where @@ -60,7 +60,7 @@ -- /\a. \x:a. x polyid :: Tm -polyid = TLam (bind a (Lam (TyVar a) (bind x (TmVar x)))) +polyid = TLam (bind a (Lam (bind (x, Embed (TyVar a)) (TmVar x)))) -- All a. a -> a polyidty :: Ty @@ -78,63 +78,63 @@ type M = ErrorT String FreshM -runM :: M a -> a +runM :: M a -> a runM m = case (runFreshM (runErrorT m)) of Left s -> error s - Right a -> a + Right a -> a checkTyVar :: Ctx -> TyName -> M () -checkTyVar g v = do - if List.elem v (getDelta g) then +checkTyVar g v = do + if List.elem v (getDelta g) then return () - else - throwError "NotFound" + else + throwError "NotFound" lookupTmVar :: Ctx -> TmName -> M Ty -lookupTmVar g v = do - case lookup v (getGamma g) of +lookupTmVar g v = do + case lookup v (getGamma g) of Just s -> return s Nothing -> throwError "NotFound" -extendTy :: TyName -> Ctx -> Ctx +extendTy :: TyName -> Ctx -> Ctx extendTy n ctx = ctx { getDelta = n : (getDelta ctx) } - + extendTm :: TmName -> Ty -> Ctx -> Ctx extendTm n ty ctx = ctx { getGamma = (n, ty) : (getGamma ctx) } tcty :: Ctx -> Ty -> M () -tcty g (TyVar x) = - checkTyVar g x -tcty g (All b) = do +tcty g (TyVar x) = + checkTyVar g x +tcty g (All b) = do (x, ty') <- unbind b tcty (extendTy x g) ty' -tcty g (Arr t1 t2) = do - tcty g t1 +tcty g (Arr t1 t2) = do + tcty g t1 tcty g t2 ti :: Ctx -> Tm -> M Ty -ti g (TmVar x) = lookupTmVar g x -ti g (Lam ty1 bnd) = do - (x, t) <- unbind bnd +ti g (TmVar x) = lookupTmVar g x +ti g (Lam bnd) = do + ((x, Embed ty1), t) <- unbind bnd tcty g ty1 ty2 <- ti (extendTm x ty1 g) t return (Arr ty1 ty2) -ti g (App t1 t2) = do +ti g (App t1 t2) = do ty1 <- ti g t1 ty2 <- ti g t2 - case ty1 of - Arr ty11 ty21 | ty2 `aeq` ty11 -> + case ty1 of + Arr ty11 ty21 | ty2 `aeq` ty11 -> return ty21 - _ -> throwError "TypeError" -ti g (TLam bnd) = do + _ -> throwError "TypeError" +ti g (TLam bnd) = do (x, t) <- unbind bnd ty <- ti (extendTy x g) t return (All (bind x ty)) ti g (TApp t ty) = do tyt <- ti g t case tyt of - (All b) -> do - tcty g ty + (All b) -> do + tcty g ty (n1, ty1) <- unbind b return $ subst n1 ty ty1 diff --git a/examples/LC-smallstep.hs b/examples/LC-smallstep.hs --- a/examples/LC-smallstep.hs +++ b/examples/LC-smallstep.hs @@ -18,8 +18,7 @@ import qualified Text.Parsec.Token as P import Text.Parsec.Language (haskellDef) -import Generics.RepLib.Bind.LocallyNameless -import Generics.RepLib +import Unbound.LocallyNameless data Term = Var (Name Term) | App Term Term diff --git a/examples/LC.hs b/examples/LC.hs --- a/examples/LC.hs +++ b/examples/LC.hs @@ -20,8 +20,7 @@ -- based on the untyped lambda calculus. module LC where -import Generics.RepLib -import Generics.RepLib.Bind.LocallyNameless +import Unbound.LocallyNameless import Control.Monad.Reader (Reader, runReader) import Data.Set as S @@ -47,7 +46,7 @@ -- | All new functions should be defined in a monad that can generate --- locally fresh names. +-- locally fresh names. type M a = FreshM a diff --git a/examples/LCRec.hs b/examples/LCRec.hs --- a/examples/LCRec.hs +++ b/examples/LCRec.hs @@ -20,8 +20,7 @@ -- based on the untyped lambda calculus. module LCRec where -import Generics.RepLib -import Generics.RepLib.Bind.LocallyNameless +import Unbound.LocallyNameless import Control.Monad.Reader (Reader, runReader) import Data.Set as S import Data.List as L @@ -30,7 +29,7 @@ data Exp = Var (Name Exp) | Lam (Bind (Name Exp) Exp) | App Exp Exp - | Letrec (Bind (Rec [(Name Exp, Annot Exp)]) Exp) + | Letrec (Bind (Rec [(Name Exp, Embed Exp)]) Exp) deriving Show -- Use RepLib to derive representation types @@ -49,7 +48,7 @@ -- | All new functions should be defined in a monad that can generate --- locally fresh names. +-- locally fresh names. type M a = FreshM a @@ -88,12 +87,12 @@ App e1 (Var y) | y == x && x `S.notMember` fv e1 -> return e1 otherwise -> return (Lam (bind x e')) red (Var x) = return $ (Var x) -red (Letrec bnd) = do +red (Letrec bnd) = do (r, body) <- unbind bnd -- get the variable definitions let vars = unrec r -- substitute them all (once) throughout the body, iteratively - let newbody = foldr (\ (x,Annot rhs) body -> subst x rhs body) body vars + let newbody = foldr (\ (x,Embed rhs) body -> subst x rhs body) body vars let fvs = fv newbody -- garbage collect, if possible if (L.any (\ (x,_) -> x `S.member` fvs) vars) then @@ -138,7 +137,7 @@ false = lam x (lam y (Var y)) if_ x y z = (App (App x y) z) -e = Letrec (bind (rec [(y, Annot(Var x)), (x, Annot (Var z))]) (Var y)) +e = Letrec (bind (rec [(y, Embed(Var x)), (x, Embed (Var z))]) (Var y)) main :: IO () main = do diff --git a/examples/LF.hs b/examples/LF.hs --- a/examples/LF.hs +++ b/examples/LF.hs @@ -25,9 +25,9 @@ import Prelude hiding (lookup) -import Generics.RepLib.Bind.LocallyNameless -import Generics.RepLib.Bind.Fresh (contLFreshM) -import Generics.RepLib +import Unbound.LocallyNameless +import Unbound.LocallyNameless.Fresh (contLFreshM) +import Unbound.LocallyNameless.Ops (unsafeUnbind) import Text.Parsec hiding ((<|>)) import qualified Text.Parsec.Token as P @@ -56,18 +56,18 @@ ------------------------------ -- Kinds -data Kind = KPi (Bind (Name Tm, Annot Ty) Kind) -- {x:ty} k +data Kind = KPi (Bind (Name Tm, Embed Ty) Kind) -- {x:ty} k | Type -- type deriving Show -- Types, also called "Families" -data Ty = TyPi (Bind (Name Tm, Annot Ty) Ty) -- {x:ty} ty +data Ty = TyPi (Bind (Name Tm, Embed Ty) Ty) -- {x:ty} ty | TyApp Ty Tm -- ty tm | TyConst (Name Ty) -- a deriving Show -- Terms, also called "Objects" -data Tm = Lam (Bind (Name Tm, Annot Ty) Tm) -- [x:ty] tm +data Tm = Lam (Bind (Name Tm, Embed Ty) Tm) -- [x:ty] tm | TmApp Tm Tm -- tm tm | TmVar (Name Tm) -- x deriving Show @@ -135,14 +135,14 @@ type Erased Kind = SKind erase Type = SKType erase (KPi b) = SKArr (erase ty) (erase k) - where ((_, Annot ty), k) = unsafeUnbind b + where ((_, Embed ty), k) = unsafeUnbind b -- this is actually safe since we ignore the name -- and promise to erase it from k. instance Erasable Ty where type Erased Ty = STy erase (TyPi b) = STyArr (erase t1) (erase t2) - where ((_, Annot t1), t2) = unsafeUnbind b + where ((_, Embed t1), t2) = unsafeUnbind b erase (TyApp ty _) = erase ty erase (TyConst c) = STyConst c @@ -377,7 +377,7 @@ tyEq ty1 ty2 k = whileChecking (TyEq ty1 ty2 k) $ tyEq' ty1 ty2 k tyEq' (TyPi bnd1) (TyPi bnd2) SKType = -- XXX - lunbind2 bnd1 bnd2 $ \(Just ((x, Annot a1), a2, (_, Annot b1), b2)) -> do + lunbind2 bnd1 bnd2 $ \(Just ((x, Embed a1), a2, (_, Embed b1), b2)) -> do tyEq a1 b1 SKType withTmBinding x (erase a1) $ tyEq a2 b2 SKType @@ -415,8 +415,8 @@ kEq Type Type = return () kEq k1@(KPi bnd1) k2@(KPi bnd2) = whileChecking (KEq k1 k2) $ - lunbind bnd1 $ \((x, Annot a), k) -> - lunbind bnd2 $ \((_, Annot b), l) -> do + lunbind bnd1 $ \((x, Embed a), k) -> + lunbind bnd2 $ \((_, Embed b), l) -> do tyEq a b SKType withTmBinding x (erase a) $ kEq k l @@ -438,14 +438,14 @@ tyCheck' t@(TmApp m1 m2) = do bnd <- unTyPi =<< tyCheck m1 a2 <- tyCheck m2 - lunbind bnd $ \((x, Annot a2'), a1) -> do + lunbind bnd $ \((x, Embed a2'), a1) -> do withErasedCtx $ tyEq a2' a2 SKType return $ subst x m2 a1 tyCheck' t@(Lam bnd) = - lunbind bnd $ \((x, Annot a1), m2) -> do + lunbind bnd $ \((x, Embed a1), m2) -> do isType =<< kCheck a1 a2 <- withTmBinding x a1 $ tyCheck m2 - return $ TyPi (bind (x, Annot a1) a2) + return $ TyPi (bind (x, Embed a1) a2) -- Compute the kind of a type. kCheck :: Ty -> TcM Ctx Kind @@ -456,11 +456,11 @@ kCheck' (TyApp a m) = do bnd <- unKPi =<< kCheck a b <- tyCheck m - lunbind bnd $ \((x, Annot b'), k) -> do + lunbind bnd $ \((x, Embed b'), k) -> do withErasedCtx $ tyEq b' b SKType return $ subst x m k kCheck' (TyPi bnd) = - lunbind bnd $ \((x, Annot a1), a2) -> do + lunbind bnd $ \((x, Embed a1), a2) -> do isType =<< kCheck a1 isType =<< (withTmBinding x a1 $ kCheck a2) return Type @@ -472,7 +472,7 @@ sortCheck' :: Kind -> TcM Ctx () sortCheck' Type = return () sortCheck' (KPi bnd) = - lunbind bnd $ \((x, Annot a), k) -> do + lunbind bnd $ \((x, Embed a), k) -> do isType =<< kCheck a withTmBinding x a $ sortCheck k @@ -546,7 +546,7 @@ <|> Lam <$> ( bind <$> brackets ((,) <$> var - <*> (Annot <$> (sym ":" *> parseTy)) + <*> (Embed <$> (sym ":" *> parseTy)) ) <*> parseTm ) @@ -562,13 +562,13 @@ -- [x:ty] ty TyPi <$> (bind <$> braces ((,) <$> var - <*> (Annot <$> (sym ":" *> parseTy)) + <*> (Embed <$> (sym ":" *> parseTy)) ) <*> parseTy) -- te -> ty <|> try (TyPi <$> (bind - <$> ((,) (string2Name "_") . Annot <$> parseTyExpr) + <$> ((,) (string2Name "_") . Embed <$> parseTyExpr) <*> (op "->" *> parseTy) )) @@ -601,13 +601,13 @@ -- {x:ty} k KPi <$> (bind <$> braces ((,) <$> var - <*> (Annot <$> (sym ":" *> parseTy)) + <*> (Embed <$> (sym ":" *> parseTy)) ) <*> parseKind) -- ka -> k <|> try (KPi <$> (bind - <$> ((,) (string2Name "_") . Annot <$> parseTyExpr) + <$> ((,) (string2Name "_") . Embed <$> parseTyExpr) <*> (op "->" *> parseKind) )) @@ -707,7 +707,7 @@ instance Pretty Kind where ppr Type = return $ text "type" - ppr (KPi bnd) = lunbind bnd $ \((x, Annot ty), k) -> do + ppr (KPi bnd) = lunbind bnd $ \((x, Embed ty), k) -> do x' <- ppr x ty' <- ppr ty k' <- ppr k @@ -721,7 +721,7 @@ tm' <- ppr tm return $ ty' <+> PP.parens tm' ppr (TyConst c) = ppr c - ppr (TyPi bnd) = lunbind bnd $ \((x, Annot ty1), ty2) -> do + ppr (TyPi bnd) = lunbind bnd $ \((x, Embed ty1), ty2) -> do x' <- ppr x ty1' <- ppr ty1 ty2' <- ppr ty2 @@ -733,10 +733,10 @@ ppr sty = ppr (uneraseTy sty) uneraseTy (STyConst c) = TyConst c -uneraseTy (STyArr t1 t2) = TyPi (bind (string2Name "_", Annot (uneraseTy t1)) (uneraseTy t2)) +uneraseTy (STyArr t1 t2) = TyPi (bind (string2Name "_", Embed (uneraseTy t1)) (uneraseTy t2)) uneraseK SKType = Type -uneraseK (SKArr sty sk) = KPi (bind (string2Name "_", Annot (uneraseTy sty)) (uneraseK sk)) +uneraseK (SKArr sty sk) = KPi (bind (string2Name "_", Embed (uneraseTy sty)) (uneraseK sk)) instance Pretty SKind where ppr sk = ppr (uneraseK sk) @@ -747,7 +747,7 @@ tm1' <- ppr tm1 tm2' <- ppr tm2 return $ tm1' <+> PP.parens tm2' - ppr (Lam bnd) = lunbind bnd $ \((x, Annot ty), tm) -> do + ppr (Lam bnd) = lunbind bnd $ \((x, Embed ty), tm) -> do x' <- ppr x ty' <- ppr ty tm' <- ppr tm diff --git a/examples/STLC.hs b/examples/STLC.hs --- a/examples/STLC.hs +++ b/examples/STLC.hs @@ -18,14 +18,18 @@ module STLC where -import Generics.RepLib -import Generics.RepLib.Bind.LocallyNameless +import Unbound.LocallyNameless import Control.Monad.Reader import Data.Set as S data Ty = TInt | TUnit | Arr Ty Ty deriving (Show, Eq) -data Exp = Lit Int | Var Name | Lam (Bind Name Exp) | App Exp Ty Exp | EUnit + +data Exp = Lit Int + | Var (Name Exp) + | Lam (Bind (Name Exp) Exp) + | App Exp Ty Exp + | EUnit deriving Show -- Use RepLib to derive representation types @@ -41,11 +45,7 @@ isvar (Var x) = Just (SubstName x) isvar _ = Nothing --- Equivalence for expressions is alpha equivalence. So we can't derive Eq --- until we've made it a member of the Alpha class -deriving instance Eq Exp - -type Ctx = [(Name, Ty)] +type Ctx = [(Name Exp, Ty)] -- A monad that can generate locally fresh names type M a = Reader Integer a @@ -77,7 +77,7 @@ patheq e1' e2' algeq e1 e2 TUnit = return True algeq e1 e2 (Arr t1 t2) = do - x <- lfresh name1 + x <- lfresh (s2n "x") algeq (App e1 t1 (Var x)) (App e2 t1 (Var x)) t2 -- path equivalence (for terms in weak-head normal form) @@ -126,10 +126,10 @@ -- Reduce both sides until you find a match. redcomp :: Exp -> Exp -> M Bool -redcomp e1 e2 = if e1 == e2 then return True else do +redcomp e1 e2 = if e1 `aeq` e2 then return True else do e1' <- red e1 e2' <- red e2 - if e1' == e1 && e2' == e2 + if e1' `aeq` e1 && e2' `aeq` e2 then return False else redcomp e1' e2' @@ -168,13 +168,16 @@ if f (runReader c (0 :: Integer)) then return () else print ("Assertion " ++ s ++ " failed") +name1, name2 :: Name Exp +name1 = s2n "x" +name2 = s2n "y" main :: IO () main = do - -- \x.x == \x.y - assert "a1" $ Lam (bind name1 (Var name1)) == Lam (bind name2 (Var name2)) + -- \x.x === \x.y + assert "a1" $ Lam (bind name1 (Var name1)) `aeq` Lam (bind name2 (Var name2)) -- \x.x /= \x.y - assert "a2" $ Lam (bind name1 (Var name2)) /= Lam (bind name1 (Var name1)) + assert "a2" . not $ Lam (bind name1 (Var name2)) `aeq` Lam (bind name1 (Var name1)) -- [] |- \x. x : () -> () assertM id "tc1" $ tc [] (Lam (bind name1 (Var name1))) (Arr TUnit TUnit) -- [] |- \x. x () : (Unit -> Int) -> Int diff --git a/examples/abstract.hs b/examples/abstract.hs --- a/examples/abstract.hs +++ b/examples/abstract.hs @@ -24,8 +24,8 @@ module Abstract where import Generics.RepLib -import Generics.RepLib.Bind.LocallyNameless -import Generics.RepLib.Bind.PermM +import Unbound.LocallyNameless + import qualified Data.Set as S import Control.Monad.Reader (Reader, runReader) @@ -62,9 +62,9 @@ -- (2) match all source positions together -- aeq' c s1 s2 = True -- (3) only match equal source positions together --- aeq' c s1 s2 = s1 == s2 --- +-- aeq' c s1 s2 = s1 == s2 -- +-- -- Below, we choose option (2) because we would like -- (alpha-)equivalence for Exp to ignore the source position -- information. Two free variables with the same name but with @@ -74,7 +74,6 @@ instance Alpha SourcePos where aeq' c s1 s2 = True acompare' c s1 s2 = EQ - match' c s1 s2 = Just empty instance Alpha Exp where diff --git a/examples/functor.hs b/examples/functor.hs --- a/examples/functor.hs +++ b/examples/functor.hs @@ -1,25 +1,24 @@ -{-# LANGUAGE TemplateHaskell, +{-# LANGUAGE TemplateHaskell, ScopedTypeVariables, FlexibleInstances, MultiParamTypeClasses, FlexibleContexts, - UndecidableInstances, + UndecidableInstances, GADTs #-} module Functor where -import Generics.RepLib hiding (Int) -import Generics.RepLib.Bind.LocallyNameless +import Unbound.LocallyNameless hiding (Int) import Control.Monad import Control.Monad.Trans.Error import Data.List as List -{- So we can't actually do modules like I was thinking of. +{- So we can't actually do modules like I was thinking of. Substitution in modules only "delays" capture not avoids it. -} type TyName = Name Type -type ModName = Name Module +type ModName = Name Module data Type = TyVar TyName | Int @@ -27,13 +26,13 @@ | Path Module TyName deriving Show -data ModDef = TyDef TyName (Maybe (Annot Type)) - | ModDef ModName Module - -- here is the question. For submodules should - -- it be Annot Module or just Module? For the +data ModDef = TyDef TyName (Maybe (Embed Type)) + | ModDef ModName Module + -- here is the question. For submodules should + -- it be Embed Module or just Module? For the -- former, then the "binding" names of the submodule -- could be bound by the outer module. For the latter - -- a submodule can't use the same name as the outer + -- a submodule can't use the same name as the outer -- module. deriving Show data Module = Struct (Rec [ModDef]) @@ -44,8 +43,8 @@ $(derive [''Type, ''ModDef, ''Module]) ------------------------------------------------------- -instance Alpha Type where +------------------------------------------------------ +instance Alpha Type where instance Alpha Module where instance Alpha ModDef where @@ -75,38 +74,37 @@ g = string2Name "G" f :: Module -f = Functor (bind x - (Struct (rec [TyDef t (Just (Annot Bool)), - TyDef u (Just (Annot (TyVar x)))]))) +f = Functor (bind x + (Struct (rec [TyDef t (Just (Embed Bool)), + TyDef u (Just (Embed (TyVar x)))]))) m :: Module -m = Struct (rec [TyDef t (Just (Annot Int)), +m = Struct (rec [TyDef t (Just (Embed Int)), ModDef g (ModApp f (TyVar t))]) -red :: Fresh m => Module -> m Module -red (ModApp m1 t) = do +red :: Fresh m => Module -> m Module +red (ModApp m1 t) = do m1' <- red m1 - case m1' of - Functor bnd -> do + case m1' of + Functor bnd -> do (x, m1'') <- unbind bnd red (subst x t m1'') _ -> return (ModApp m1 t) -red (Struct s) = do +red (Struct s) = do defs <- mapM redDef (unrec s) - return (Struct (rec defs)) + return (Struct (rec defs)) red m = return m redDef :: Fresh m => ModDef -> m ModDef -redDef (ModDef f m) = do +redDef (ModDef f m) = do m' <- red m return (ModDef f m') redDef d = return d -m3 = Struct (rec [TyDef t Nothing, - TyDef u (Just (Annot (TyVar t)))]) +m3 = Struct (rec [TyDef t Nothing, + TyDef u (Just (Embed (TyVar t)))]) m2 :: Module m2 = runFreshM (red m) - - + diff --git a/examples/functor2.hs b/examples/functor2.hs --- a/examples/functor2.hs +++ b/examples/functor2.hs @@ -1,15 +1,14 @@ -{-# LANGUAGE TemplateHaskell, +{-# LANGUAGE TemplateHaskell, ScopedTypeVariables, FlexibleInstances, MultiParamTypeClasses, FlexibleContexts, - UndecidableInstances, + UndecidableInstances, GADTs #-} module Functor2 where -import Generics.RepLib hiding (Int) -import Generics.RepLib.Bind.LocallyNameless +import Unbound.LocallyNameless hiding (Int) import Control.Monad import Control.Monad.Trans.Error import Data.List as List @@ -18,7 +17,7 @@ -} type TyName = Name Type -type ModName = Name Module +type ModName = Name Module data Type = TyVar TyName | Int @@ -26,8 +25,8 @@ | Path Module String deriving Show -data ModDef = TyDef TyName (Maybe (Annot Type)) - | ModDef ModName (Annot Module) +data ModDef = TyDef TyName (Maybe (Embed Type)) + | ModDef ModName (Embed Module) deriving Show data Module = Struct (Bind (Rec [(String,ModDef)]) ()) @@ -38,8 +37,8 @@ $(derive [''Type, ''ModDef, ''Module]) ------------------------------------------------------- -instance Alpha Type where +------------------------------------------------------ +instance Alpha Type where instance Alpha Module where instance Alpha ModDef where @@ -70,37 +69,36 @@ g = string2Name "G" f :: Module -f = Functor (bind x - (Struct (bind (rec - [("t", TyDef t (Just (Annot Bool))), - ("u", TyDef u (Just (Annot (TyVar x))))]) ()))) +f = Functor (bind x + (Struct (bind (rec + [("t", TyDef t (Just (Embed Bool))), + ("u", TyDef u (Just (Embed (TyVar x))))]) ()))) m :: Module -m = Struct (bind (rec [("t", TyDef t (Just (Annot Int))), - ("g", ModDef g (Annot (ModApp f (TyVar t))))]) ()) +m = Struct (bind (rec [("t", TyDef t (Just (Embed Int))), + ("g", ModDef g (Embed (ModApp f (TyVar t))))]) ()) -red :: Fresh m => Module -> m Module -red (ModApp m1 t) = do +red :: Fresh m => Module -> m Module +red (ModApp m1 t) = do m1' <- red m1 - case m1' of - Functor bnd -> do + case m1' of + Functor bnd -> do (x, m1'') <- unbind bnd red (subst x t m1'') _ -> return (ModApp m1 t) -red (Struct s) = do +red (Struct s) = do (r,()) <- unbind s defs <- mapM redDef (unrec r) - return (Struct (bind (rec defs) ())) + return (Struct (bind (rec defs) ())) red m = return m redDef :: Fresh m => (String,ModDef) -> m (String,ModDef) -redDef (s,ModDef f (Annot m)) = do +redDef (s,ModDef f (Embed m)) = do m' <- red m - return (s,ModDef f (Annot m')) + return (s,ModDef f (Embed m')) redDef d = return d m2 :: Module m2 = runFreshM (red m) - - + diff --git a/examples/issue15.hs b/examples/issue15.hs --- a/examples/issue15.hs +++ b/examples/issue15.hs @@ -6,7 +6,7 @@ module Issue15 where import Generics.RepLib -import qualified Generics.RepLib.Bind.LocallyNameless as LN +import qualified Unbound.LocallyNameless as LN data Foo = Foo (LN.Name Foo) diff --git a/tutorial/Tutorial.lhs b/tutorial/Tutorial.lhs --- a/tutorial/Tutorial.lhs +++ b/tutorial/Tutorial.lhs @@ -1,25 +1,31 @@ -Programming with binders using RepLib -===================================== +Programming with binders using Unbound +====================================== *Names* are the bane of every language implementation: they play an unavoidable, central role, yet are tedious to deal with and surprisingly tricky to get right. -RepLib includes a flexible and powerful library for programming with +Unbound is a flexible and powerful library for programming with names and binders, which makes programming with binders easy and painless. Built on top of RepLib's generic programming framework, it does a lot of work behind the scenes to provide you with a seamless, "it just works" experience. This literate Haskell tutorial will walk you through the basics of -using the library. +using Unbound. The [Haddock documentation for +Unbound](http://hackage.haskell.org/package/unbound) is also a good +source of information. For something more academic, you may also be +interested in reading +* [Stephanie Weirich, Brent Yorgey, and Tim Sheard. Binders +Unbound.](http://www.cis.upenn.edu/~byorgey/papers/binders-unbound.pdf) +Submitted, March 2011. + The untyped lambda calculus --------------------------- Let's start by writing a simple untyped lambda calculus -interpreter. This will illustrate the basic functionality of the -binding library. +interpreter. This will illustrate the basic functionality of Unbound. **Preliminaries** @@ -38,17 +44,14 @@ assured, however, that the instances generated by RepLib *are* decidable; it's just that GHC can't prove it. -Now for some imports: +Now to import the library: -> import Generics.RepLib -> import Generics.RepLib.Bind.LocallyNameless +> import Unbound.LocallyNameless -We import the RepLib library as well as the locally nameless -implementation of the binding library. (RepLib also provides a nominal -version in `Generics.RepLib.Bind.Nominal`. At the moment these are -simply two different implementations providing essentially the same -interface. The locally nameless version is more mature, but you are -welcome to experiment with using the nominal version in its place.) +We import the locally nameless implementation of Unbound (A nominal +implementation is also provided in `Unbound.Nominal`. However, at the +moment it is likely full of bugs and is poorly documented, so we +recommend sticking with the locally nameless implementation for now.) A few other imports we'll need for this particular example: @@ -78,19 +81,19 @@ constructors are worth looking at in detail. First, the `Var` constructor holds a `Name Term`. `Name` is an -abstract type for representing names provided by RepLib. `Name`s are -indexed by the sorts of things to which they can refer (or more +abstract type for representing names, provided by Unbound. `Name`s +are indexed by the sorts of things to which they can refer (or more precisely, the sorts of things which can be substituted for them). Here, a variable is simply a name for some `Term`, so we use the type `Name Term`. -Lambdas are where names are *bound*, so we use the special `Bind` type -also provided by RepLib. Something of type `Bind p b` represents a -pair consisting of a *pattern* `p` and a *body* `b`. The pattern may -bind names which occur in `b`. Here is where the power of generic -programming comes into play: we may use (almost) any types at all as -patterns and bodies, and RepLib will be able to handle it with very -little extra guidance from us. +Lambdas are where names are *bound*, so we use the special `Bind` +combinator, also provided by the library. Something of type `Bind p b` +represents a pair consisting of a *pattern* `p` and a *body* `b`. The +pattern may bind names which occur in `b`. Here is where the power of +generic programming comes into play: we may use (almost) any types at +all as patterns and bodies, and Unbound will be able to handle it with +very little extra guidance from us. In this particular case, a lambda simply binds a single name, so the pattern is just a `Name Term`, and the body is just another `Term`. @@ -110,7 +113,8 @@ the default implementations, written in terms of those generic instances we had RepLib derive for us, work just fine. But in special situations it's possible to override specific methods in the `Alpha` -class with our own implementations. +class with our own implementations (see the documentation for an +example). We only need to provide one more thing: a `Subst Term Term` instance. In general, an instance for `Subst b a` means that we can @@ -152,13 +156,15 @@ *Main> lam "x" (lam "y" (var "x")) Lam ( Lam ( Var 1@0)) -The `1@0` is a *de Bruijn index*, which refers to the 0th variable of -the 1st (counting outwards from 0) enclosing binding site; that is, to -`x`. Recall that the left-hand side of a `Bind` can be an arbitrary -data structure potentially containing multiple names (a *pattern*), -like a pair or a list; hence the need for the index after the `@`. Of -course, in this particular example we only ever bind one name at once, -so the index after the `@` will always be zero. +Don't worry about the `1@0` thing: Unbound handles all the details of +this for you. However, if you must know, it is a *de Bruijn index*, +which refers to the 0th variable of the 1st (counting outwards from 0) +enclosing binding site; that is, to `x`. Recall that the left-hand +side of a `Bind` can be an arbitrary data structure potentially +containing multiple names (a *pattern*), like a pair or a list; hence +the need for the index after the `@`. Of course, in this particular +example we only ever bind one name at once, so the index after the `@` +will always be zero. We can check that substitution works as we expect. Substituting for `x` in a term where `x` does not occur free has no effect: @@ -243,7 +249,7 @@ We can use [Parsec](http://hackage.haskell.org/package/parsec) to write a tiny parser for our lambda calculus: -> lexer = P.makeTokenParser haskellDef +> lexer = P.makeTokenParser haskellDef > parens = P.parens lexer > brackets = P.brackets lexer > ident = P.identifier lexer @@ -309,21 +315,22 @@ -- | Avoid the given names when freshening in the subcomputation. avoid :: [AnyName] -> m a -> m a -Monads which are instances of `LFresh` maintain a set of names that -are to be avoided. `lfresh` generates a name which is guaranteed not -to be in the set, and `avoid` runs a subcomputation with some -additional names that should be avoided. You probably won't need to -call these methods explicitly very often; more useful are some methods -built on top of these such as `lunbind`: +Monads which are instances of `LFresh` maintain a set of "currently +in-scope" names which are to be avoided when generating new +names. `lfresh` generates a name which is guaranteed not to be in the +set, and `avoid` runs a subcomputation with some additional names +added to the in-scope set. You probably won't need to call these +methods explicitly very often; more useful are some methods built on +top of these such as `lunbind`: - lunbind :: (LFresh m, Alpha a, Alpha b) => Bind a b -> ((a, b) -> m c) -> m c + lunbind :: (LFresh m, Alpha p, Alpha t) => Bind p t -> ((p, t) -> m r) -> m r `lunbind` corresponds to `unbind` but works in an `LFresh` context. It destructs a binding, avoiding only names curently in scope, and runs a subcomputation while additionally avoiding the chosen name(s). Let's rewrite our pretty-printer in terms of `LFresh`. The only -change we need to make is to use a continuation-passing style for the +change we need to make is to use continuation-passing style for the call to `lunbind` in place of the normal monadic sequencing used with `unbind`. @@ -347,6 +354,10 @@ Much better! +Note: the tutorial from this point on is still under construction, so +expect some rough edges -- although you may still find the material +useful! + A simple dependent calculus --------------------------- @@ -390,7 +401,7 @@ telescopes also have their own internal binding structure. > data Tele = Empty -> | Cons (Rebind (Name Exp, Annot Exp) Tele) +> | Cons (Rebind (Name Exp, Embed Exp) Tele) > deriving Show A telescope can be empty, of course, or else it is a variable binding @@ -410,13 +421,13 @@ this is not correct. The `Exp` is a type annotation for the name, and any names occurring in it are actually *references* to previously bound names, not binding sites themselves. For this purpose the -`Annot` wrapper is provided, which specifies that the wrapped type -- +`Embed` wrapper is provided, which specifies that the wrapped type -- which would otherwise be considered a binding pattern -- is only an annotation whose names refer back to previous bindings. Pop quiz: why would - | Cons (Rebind (Name Exp) (Annot Exp, Tele)) + | Cons (Rebind (Name Exp) (Embed Exp, Tele)) also be incorrect? @@ -465,11 +476,11 @@ > > mkTele :: [(String, Exp)] -> Tele > mkTele [] = Empty -> mkTele ((x,e) : t) = Cons (rebind (string2Name x, Annot e) (mkTele t)) +> mkTele ((x,e) : t) = Cons (rebind (string2Name x, Embed e) (mkTele t)) These are fairly straightforward, and we note only the second case of `mkTele`, where we use `rebind` for creating a `Rebind` structure, and -wrap `e` in an `Annot` constructor. +wrap `e` in an `Embed` constructor. We can test things out so far by creating a few example terms. Here is the polymorphic identity function: @@ -529,7 +540,7 @@ > lookUp n Empty = throwError $ "Not in scope: " ++ show n > lookUp v (Cons rb) | v == x = return a > | otherwise = lookUp v t' -> where ((x, Annot a), t') = unrebind rb +> where ((x, Embed a), t') = unrebind rb (We also note in passing that `appTele` and `lookUp` would be perfect opportunities to use GHC's `ViewPatterns`, but for simplicity's sake @@ -572,7 +583,7 @@ > checkList :: Tele -> [Exp] -> Tele -> M () > checkList _ [] Empty = ok > checkList g (e:es) (Cons rb) = do -> let ((x, Annot a), t') = unrebind rb +> let ((x, Embed a), t') = unrebind rb > check g e a > checkList (subst x e g) (subst x e es) (subst x e t') > checkList _ _ _ = throwError $ "Unequal number of parameters and arguments" diff --git a/unbound.cabal b/unbound.cabal --- a/unbound.cabal +++ b/unbound.cabal @@ -1,5 +1,5 @@ name: unbound -version: 0.2 +version: 0.2.1 license: BSD3 license-file: LICENSE build-type: Simple @@ -7,7 +7,6 @@ tested-with: GHC == 7.0.1 author: Stephanie Weirich maintainer: Brent Yorgey - Chris Casinghino Stephanie Weirich homepage: http://code.google.com/p/replib/ category: Language, Generics, Compilers/Interpreters @@ -22,7 +21,8 @@ expressive set of type combinators, and Unbound handles the rest! Automatically derives alpha-equivalence, free variable calculation, - capture-avoiding substitution, and more. + capture-avoiding substitution, and more. See + "Unbound.LocallyNameless" to get started. Library build-depends: base >= 4.3 && < 5, RepLib >= 0.4.0,