unbound-generics: Support for programming with names and binders using GHC Generics

[ bsd3, language, library ] [ Propose Tags ]
Versions [RSS], 0.0.1, 0.0.2,, 0.0.3, 0.1, 0.1.2,, 0.2, 0.3, 0.3.1, 0.3.2, 0.3.3, 0.3.4, 0.4.0, 0.4.1, 0.4.2
Change log Changelog.md
Dependencies ansi-wl-pprint (>= && <0.7), base (>=4.6 && <5), containers (>=0.5 && <0.7), contravariant (>=0.5), deepseq (>=, exceptions (>=0.8 && <0.11), mtl (>=2.1), profunctors (>=4.0), semigroups (>=0.18 && <0.19), template-haskell (>=, transformers (>=0.3), transformers-compat (>=0.3) [details]
License BSD-3-Clause
Copyright (c) 2014-2022, Aleksey Kliger
Author Aleksey Kliger
Maintainer aleksey@lambdageek.org
Category Language
Home page http://github.com/lambdageek/unbound-generics
Bug tracker http://github.com/lambdageek/unbound-generics/issues
Source repo head: git clone git://github.com/lambdageek/unbound-generics.git
Uploaded by AlekseyKliger at 2022-05-20T14:11:59Z
Distributions LTSHaskell:0.4.2, NixOS:0.4.2, Stackage:0.4.2
Downloads 12574 total (49 in the last 30 days)
Rating 2.0 (votes: 1) [estimated by Bayesian average]
Your Rating
  • λ
  • λ
  • λ
Status Docs uploaded by user
Build status unknown [no reports yet]

Readme for unbound-generics-0.4.2

[back to package description]


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

Hackage CI

Support for programming with names and binders using GHC Generics.


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.


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.

  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)