unbound-generics

Join the chat at https://gitter.im/lambdageek/unbound-generics Discord

Hackage CI

Support for programming with names and binders using GHC Generics.

Summary

Specify the binding structure of your data type with an expressive set of type combinators, and unbound-generics handles the rest! Automatically derives alpha-equivalence, free variable calculation, capture-avoiding substitution, and more. See Unbound.Generics.LocallyNameless to get started.

This is a reimplementation of (parts of) unbound but using GHC generics instead of RepLib.

Examples

Some examples are in the examples/ directory in the source. And also at unbound-generics on GitHub Pages

Example: Untyped lambda calculus interpreter

Here is how you would implement call by value evaluation for the untyped lambda calculus:

{-# LANGUAGE DeriveDataTypeable, DeriveGeneric, MultiParamTypeClasses #-}
module UntypedLambdaCalc where
import Unbound.Generics.LocallyNameless
import GHC.Generics (Generic)
import Data.Typeable (Typeable)

-- | Variables stand for expressions
type Var = Name Expr

-- | Expressions
data Expr = V Var                -- ^ variables
          | Lam (Bind Var Expr) -- ^ lambdas bind a variable within a body expression
          | App Expr Expr       -- ^ application
          deriving (Show, Generic, Typeable)

-- Automatically construct alpha equivalence, free variable computation and binding operations.
instance Alpha Expr

-- semi-automatically implement capture avoiding substitution of expressions for expressions
instance Subst Expr Expr where
  -- `isvar` identifies the variable case in your AST.
  isvar (V x) = Just (SubstName x)
  isvar _     = Nothing

-- evaluation takes an expression and returns a value while using a source of fresh names
eval :: Expr -> FreshM Expr
eval (V x) = error $ "unbound variable " ++ show x
eval e@Lam{} = return e
eval (App e1 e2) = do
  v1 <- eval e1
  v2 <- eval e2
  case v1 of
   Lam bnd -> do
     -- open the lambda by picking a fresh name for the bound variable x in body
     (x, body) <- unbind bnd
     let body' = subst x v2 body
     eval body'
   _ -> error "application of non-lambda"

example :: Expr
example =
  let x = s2n "x"
      y = s2n "y"
      e = Lam $ bind x (Lam $ bind y (App (V y) (V x)))
  in runFreshM $ eval (App (App e e) e)
  
-- >>> example
-- Lam (<y> App (V 0@0) (Lam (<x> Lam (<y> App (V 0@0) (V 1@0)))))

Differences from unbound

For the most part, I tried to keep the same methods with the same signatures. However there are a few differences.

  1. fv :: Alpha t => Fold t (Name n)

    The fv method returns a Fold (in the sense of the lens library), rather than an Unbound.Util.Collection instance. That means you will generally have to write toListOf fv t or some other summary operation.

  2. Utility methods in the Alpha class have different types.

    You should only notice this if you’re implementing an instance of Alpha by hand (rather than by using the default generic instance).

    1. isPat :: Alpha t => t -> DisjointSet AnyName The original unbound returned a Maybe [AnyName] here with the same interpretation as DisjointSet: Nothing means an inconsistency was encountered, or Just the free variables of the pattern.
    2. isTerm :: Alpha t => t -> All
    3. open :: Alpha t => AlphaCtx -> NthPatFind -> t -> t, close :: Alpha t => AlphaCtx -> NamePatFind -> t -> t where NthPatFind and NamePatFind are newtypes
  3. embed :: IsEmbed e => Embedded e -> e and unembed :: IsEmbed e => e -> Embedded e

    The typeclass IsEmbed has an Iso (again in the sense of the lens library) as a method instead of the above pair of methods.

    Again, you should only notice this if you’re implementing your own types that are instances of IsEmbed. The easiest thing to do is to use implement embedded = iso yourEmbed yourUnembed where iso comes from lens. (Although you can also implement it in terms of dimap if you don’t want to depend on lens)

Changes

NEXT

0.4.3

  • Add an instantiate function that substitutes a list of terms for a collection of bound variables in a toplevel Bind p t term. Thanks to Stephanie Weirich (sweirich). This adds a new substBvs function to the Subst class.
  • Add substBind operation that substitutes for the bound variable of a Bind (Name a) t term. This is a specialization of instantiate to the case where the pattern is a single Name a
  • Tests for substBind by Mark Lemay (marklemay) Thanks!
  • Expose Rec constructor of the Rec type and the ctxLevel function from AlphaCtx
  • Require transformers < 0.6, run CI with GHC 9.4, drop CI with GHC 7.10. Thanks to Andreas Abel (andreaasabel).

0.4.2

  • Add Functor instance for Unbound.Generics.LocallyNameless.Internal.Iso.Exchange Thanks to Emily Pillmore (emilypi)
  • Import MonadPlus and MonadFix explicitly when building with mtl-2.3
  • Builds with GHC 9.0, GHC 9.2

0.4.1

  • Add MonadFail instances for LFreshMT and FreshMT

  • Builds with GHC 8.10

0.4.0

  • New binding specification type Ignore.

    Any two Ignore T terms will always be alpha-equivalent to each other, will be considered to contain no variables, and will not have any substitution apply beneath Ignore. Useful for attaching annotation terms to your AST.

      import Text.Parsec.Pos (SourcePos)
      
      data Expr =
         ...
         | Lambda (Ignore SourcePos) (Bind (Name Expr) Expr)
    

    As expected, any two Lambda expressions will be considered alpha-equivalent even if they differ in source position.

    Note that the Ignore will block operations on Name a for all a, which can be a little unexpected:

      data Ty =
        TyVar (Name Ty)
        | TyArr Ty Ty
      
      instance Subst Ty Ty where
        ...
    
      data Expr =
        ...
        | Var (Name Expr)
        | Lambda (Ignore Ty) (Bind (Name Expr) Expr)
      
       instance Subst Ty Expr
    

    Applying a substitution of a type for a free type variable to a Lambda will not descend into the Ignore Ty.

    Thanks Reed Mullanix (TOTWBF) for the new operation.

  • Fix an issue in substitution where traversal would not continue in an AST node for which isvar or isCoerceVar is defined to return non-Nothing but which had additional structure.

    For example, in a language with meta variables and explicit substitutions:

       data Expr =
         ...
           -- normal variables that stand for expressions
         | Var (Name Expr)
            -- a meta variable occurrence and an explicit substitution
      	  -- of expressions to substitute in for the free variables
         | MetaVar (Name Meta) [(Name Expr, Expr)]
       -- a meta variable stands for an expression with some free term vars
       data Meta = MetaVar Expr
    
       -- substitution for a meta in an expression
       instance Subst Expr Meta where
         isCoerceVar (MetaVar u sub) = Just (SubstCoerce u (Just . applyExplicitSubst sub))
       applyExplicitSubst :: [(Name Expr, Expr)] -> Meta -> Expr
       applyExplicitSubst s (MetaVar e) = substs s e
    

    Given an expression e1 defined as MetaVar "u" [("x", 10)], we may want to substitute a Meta ("x" + "x") for "u" to get 10 + 10 (that is, we replace "u" by the expression "x" + "x" and immediately apply the substitution 10 for "x").

    Now suppose we have an expression e2 defined as MetaVar "v" [("y", e1)] (that is, an occurrence of meta var “v” together with a substitution of e1 from above for "y"). If we again try to substitute Meta ("x" + "x") for "u" in e2, we would expect to get MetaVar "v" [("y", 10 + 10)] (that is, since “v” is not equal to “u”, we leave the meta var alone, but substitute for any occurrences of “u” in the explicit substitution, so e1 becomes 10 + 10 as before).

    The bug in previous versions of unbound-generics was that we would incorrectly leave MetaVar "v" [("y", e1)] unchanged as soon as we saw that isCoerceVar (MetaVar "v" [("y", e1)]) returned Just (SubstCoerce "u" ...) where "u" /= "v".

    Thanks Reed Mullanix (TOTWBF) for finding and fixing this issue. https://github.com/lambdageek/unbound-generics/issues/26

0.3.4

  • Bump containers upper bound to support 0.6. (GHC 8.6.1 support) Thanks Christiaan Baaij.

0.3.3

  • Bump exceptions upper bound to support 0.10.0

0.3.2

  • Bump deepseq >= 1.4.0.0 remove benchmark dependency on deepseq-generics
  • Tested with GHC 8.4.1
  • Tested with GHC 8.2.2
  • Compile with -Wcompat
  • Add Semigroup instances for all types that were previously Monoid instances
  • Added more examples to the examples/ directory
  • Added “exceptions” dependency and MonadThrow, MonadCatch, MonadMask instances for FreshMT and LFreshMT. Thanks Alex McKenna.

0.3.1

  • Tested with GHC 8.0.1
  • Removed Generic b constraint from Subst b (Name a) instance.

0.3

  • Change types of open and close to take NthPatFind and NamePatFind instead of generic patterns, update call sites.
  • Add newtype wrappers and Monoid instances for NthPatFind and NamePatFind
  • Change isTerm to return All instead of Bool

0.2

  • Incorporating some of the extras/oversights from clash-lib Unbound.Generics.LocallyNameless.Extra

    • Make Embed an instance of Ord
    • NFData instances (see below)
  • Re-implement freshen' and gfreshen using a free monad to give GHC a chance to inline it all away. This changes the type of gfreshen. Major version bump.

    • Expose FFM, liftFFM and retractFFM
  • Provide NFData instances for all the combinators. Depend on ‘deepseq’

  • Start benchmarking some of the operations (particularly unbind).

0.1.2.1

  • Fix ghc-7.10 build.
  • Haddock cleanup.

0.1.2

  • Added IsEmbed typeclass

    • Depend on ‘profunctors’
  • Changed embed and unembed to work over any IsEmbed type.

  • Added Shift type for shifting the scope of embedded terms out one level.

0.1.1

  • Added isNullDisjointSet function.
  • Implement a TH makeClosedAlpha splice for constructing trivial leaf instances.

0.1

  • Add acompare functiona and acompare' method to Alpha typeclass. (christiaanb)

    Handwritten Alpha instances will need to define this additional method now. Major version bump.

0.0.3

  • Add ‘name2Integer’ method (christiaanb)

  • Export internal type-directed gaeq, gopen, gclose, etc functions from Unbound.Generics.LocallyNameless.Alpha.

    Allows definitions like:

      instance Alpha Term where
        aeq' _ (Prim t1 _dk1) (Prim t2 _dk2) = t1 == t2
        aeq' c t1             t2             = gaeq c (from t1) (from t2)
    

0.0.2.1

  • Unconditionally add ErrorT and ExceptT instances using transformers-compat (bergmark)

0.0.2

  • Add ‘Rec’ pattern and ‘TRec’ term combinators.

  • Alpha instance for ‘()’

0.0.1

  • Add ‘lunbind2’ function.

  • Doc updates.

  • Switch from ‘HUnit’ to ‘Tasty’ for testing.

0.0.0.90

  • Initial (re-)implementation effort.