unbound-generics
Support for programming with names and binders using GHC Generics
http://github.com/lambdageek/unbound-generics
Version on this page: | 0.4.3 |
LTS Haskell 21.25: | 0.4.3 |
Stackage Nightly 2024-11-06: | 0.4.4 |
Latest on Hackage: | 0.4.4 |
unbound-generics-0.4.3@sha256:12209c0049000d0dd8c3eb6013d0278a8b269a2421d9758083aab9f58c4b6b4c,5446
Module documentation for 0.4.3
- Unbound
- Unbound.Generics
- Unbound.Generics.LocallyNameless
- Unbound.Generics.LocallyNameless.Alpha
- Unbound.Generics.LocallyNameless.Bind
- Unbound.Generics.LocallyNameless.Embed
- Unbound.Generics.LocallyNameless.Fresh
- Unbound.Generics.LocallyNameless.Ignore
- Unbound.Generics.LocallyNameless.Internal
- Unbound.Generics.LocallyNameless.LFresh
- Unbound.Generics.LocallyNameless.Name
- Unbound.Generics.LocallyNameless.Operations
- Unbound.Generics.LocallyNameless.Rebind
- Unbound.Generics.LocallyNameless.Rec
- Unbound.Generics.LocallyNameless.Shift
- Unbound.Generics.LocallyNameless.Subst
- Unbound.Generics.LocallyNameless.TH
- Unbound.Generics.LocallyNameless.Unsafe
- Unbound.Generics.PermM
- Unbound.Generics.LocallyNameless
- Unbound.Generics
unbound-generics
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.
-
fv :: Alpha t => Fold t (Name n)
The
fv
method returns aFold
(in the sense of the lens library), rather than anUnbound.Util.Collection
instance. That means you will generally have to writetoListOf fv t
or some other summary operation. -
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).isPat :: Alpha t => t -> DisjointSet AnyName
The originalunbound
returned aMaybe [AnyName]
here with the same interpretation asDisjointSet
:Nothing
means an inconsistency was encountered, orJust
the free variables of the pattern.isTerm :: Alpha t => t -> All
open :: Alpha t => AlphaCtx -> NthPatFind -> t -> t
,close :: Alpha t => AlphaCtx -> NamePatFind -> t -> t
whereNthPatFind
andNamePatFind
are newtypes
-
embed :: IsEmbed e => Embedded e -> e
andunembed :: IsEmbed e => e -> Embedded e
The typeclass
IsEmbed
has anIso
(again in the sense of thelens
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 implementembedded = iso yourEmbed yourUnembed
whereiso
comes fromlens
. (Although you can also implement it in terms ofdimap
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 toplevelBind p t
term. Thanks to Stephanie Weirich (sweirich). This adds a newsubstBvs
function to theSubst
class. - Add
substBind
operation that substitutes for the bound variable of aBind (Name a) t
term. This is a specialization ofinstantiate
to the case where the pattern is a singleName a
- Tests for
substBind
by Mark Lemay (marklemay) Thanks! - Expose
Rec
constructor of theRec
type and thectxLevel
function fromAlphaCtx
- 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 forUnbound.Generics.LocallyNameless.Internal.Iso.Exchange
Thanks to Emily Pillmore (emilypi) - Import
MonadPlus
andMonadFix
explicitly when building with mtl-2.3 - Builds with GHC 9.0, GHC 9.2
0.4.1
-
Add
MonadFail
instances forLFreshMT
andFreshMT
-
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 beneathIgnore
. 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 onName a
for alla
, 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 theIgnore 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
orisCoerceVar
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 asMetaVar "u" [("x", 10)]
, we may want to substitute aMeta ("x" + "x")
for"u"
to get10 + 10
(that is, we replace"u"
by the expression"x" + "x"
and immediately apply the substitution10
for"x"
).Now suppose we have an expression
e2
defined asMetaVar "v" [("y", e1)]
(that is, an occurrence of meta var “v” together with a substitution ofe1
from above for"y"
). If we again try to substituteMeta ("x" + "x")
for"u"
ine2
, we would expect to getMetaVar "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, soe1
becomes10 + 10
as before).The bug in previous versions of
unbound-generics
was that we would incorrectly leaveMetaVar "v" [("y", e1)]
unchanged as soon as we saw thatisCoerceVar (MetaVar "v" [("y", e1)])
returnedJust (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 support0.6
. (GHC 8.6.1 support) Thanks Christiaan Baaij.
0.3.3
- Bump
exceptions
upper bound to support0.10.0
0.3.2
- Bump
deepseq >= 1.4.0.0
remove benchmark dependency ondeepseq-generics
- Tested with GHC 8.4.1
- Tested with GHC 8.2.2
- Compile with
-Wcompat
- Add
Semigroup
instances for all types that were previouslyMonoid
instances - Added more examples to the examples/ directory
- Added “exceptions” dependency and
MonadThrow
,MonadCatch
,MonadMask
instances forFreshMT
andLFreshMT
. Thanks Alex McKenna.
0.3.1
- Tested with GHC 8.0.1
- Removed
Generic b
constraint fromSubst b (Name a)
instance.
0.3
- Change types of
open
andclose
to takeNthPatFind
andNamePatFind
instead of generic patterns, update call sites. - Add newtype wrappers and Monoid instances for
NthPatFind
andNamePatFind
- Change
isTerm
to returnAll
instead ofBool
0.2
-
Incorporating some of the extras/oversights from clash-lib Unbound.Generics.LocallyNameless.Extra
- Make
Embed
an instance ofOrd
NFData
instances (see below)
- Make
-
Re-implement
freshen'
andgfreshen
using a free monad to give GHC a chance to inline it all away. This changes the type ofgfreshen
. Major version bump.- Expose
FFM
,liftFFM
andretractFFM
- Expose
-
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
andunembed
to work over anyIsEmbed
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 andacompare'
method toAlpha
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 fromUnbound.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.