unbound-generics
Support for programming with names and binders using GHC Generics
http://github.com/lambdageek/unbound-generics
| Version on this page: | 0.4.0 |
| LTS Haskell 21.25: | 0.4.3 |
| Stackage Nightly 2024-11-18: | 0.4.4 |
| Latest on Hackage: | 0.4.4 |
unbound-generics-0.4.0@sha256:bc2541b5919ae64b8421431fe03d9ab4ffabc7710a93b52aa5dd4325422c41be,5470Module documentation for 0.4.0
- 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) = fail $ "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'
_ -> fail "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
fvmethod returns aFold(in the sense of the lens library), rather than anUnbound.Util.Collectioninstance. That means you will generally have to writetoListOf fv tor some other summary operation. -
Utility methods in the
Alphaclass have different types.You should only notice this if you’re implementing an instance of
Alphaby hand (rather than by using the default generic instance).isPat :: Alpha t => t -> DisjointSet AnyNameThe originalunboundreturned aMaybe [AnyName]here with the same interpretation asDisjointSet:Nothingmeans an inconsistency was encountered, orJustthe free variables of the pattern.isTerm :: Alpha t => t -> Allopen :: Alpha t => AlphaCtx -> NthPatFind -> t -> t,close :: Alpha t => AlphaCtx -> NamePatFind -> t -> twhereNthPatFindandNamePatFindare newtypes
-
embed :: IsEmbed e => Embedded e -> eandunembed :: IsEmbed e => e -> Embedded eThe typeclass
IsEmbedhas anIso(again in the sense of thelenslibrary) 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 yourUnembedwhereisocomes fromlens. (Although you can also implement it in terms ofdimapif you don’t want to depend on lens)