Copyright  (c) 2013 Edward Kmett 2021 Marco Zocca 

License  BSD 
Maintainer  github.com/ocramz 
Stability  experimental 
Portability  POSIX 
Safe Haskell  SafeInferred 
Language  Haskell2010 
Example
The whnf
function in this example shows how to betareduce a term of the untyped lambda calculus.
Note : the Show instance of Exp depends on its Show1 instance (since Exp has one type parameter), which can be derived Generically
. This works on most recent versions of GHC (>= 8.6.1).
Note 2 : the example below requires language extensions DeriveFunctor
, DeriveFoldable
, DeriveTraversable
and DerivingVia
.
import Bound.Simple (Scope, Bound(..), abstract1, instantiate1) import Data.Functor.Classes (Show1) import Data.Functor.Classes.Generic (Generically(..)) import GHC.Generics (Generic1) infixl 9 :@ data Exp a = V a  Exp a :@ Exp a  Lam (Scope () Exp a) deriving (Show, Functor, Foldable, Traversable, Generic1) deriving (Show1) via Generically Exp instance Applicative Exp where pure = V; k <*> m = ap k m instance Monad Exp where return = V V a >>= f = f a (x :@ y) >>= f = (x >>= f) :@ (y >>= f) Lam e >>= f = Lam (e>>>=
f) lam :: Eq a => a > Exp a > Exp a lam v b = Lam (abstract1
v b) whnf :: Exp a > Exp a whnf (e1 :@ e2) = case whnf e1 of Lam b > whnf (instantiate1
e2 b) f' > f' :@ e2 whnf e = e main :: IO () main = do let term = lamx
(Vx
) :@ Vy
print term  Lam (Scope (V (B ()))) :@ Vy
print $ whnf term  Vy
Synopsis
 class Bound t where
 data Scope b f a
 toScope :: f (Var b a) > Scope b f a
 fromScope :: Scope b f a > f (Var b a)
 data Var b a
 abstract :: Functor f => (a > Maybe b) > f a > Scope b f a
 abstract1 :: (Functor f, Eq a) => a > f a > Scope () f a
 instantiate :: Monad f => (b > f a) > Scope b f a > f a
 instantiate1 :: Monad f => f a > Scope n f a > f a
 bindings :: Foldable f => Scope b f a > [b]
 hoistScope :: (f (Var b a) > g (Var b a)) > Scope b f a > Scope b g a
 closed :: Traversable f => f a > Maybe (f b)
 substitute :: (Monad f, Eq a) => a > f a > f a > f a
 substituteVar :: (Functor f, Eq a) => a > a > f a > f a
 isClosed :: Foldable f => f a > Bool
 newtype Generically f a = Generically {
 unGenerically :: f a
Documentation
Nothing
is an Scope
b f af
expression with bound variables in b
,
and free variables in a
Instances
Bound (Scope b) Source #  
Functor f => Generic1 (Scope b f :: Type > Type) Source #  
Monad f => Monad (Scope b f) Source #  The monad permits substitution on free variables, while preserving bound variables 
Functor f => Functor (Scope b f) Source #  
Monad f => Applicative (Scope b f) Source #  
Foldable f => Foldable (Scope b f) Source # 

Defined in Bound.Simple fold :: Monoid m => Scope b f m > m # foldMap :: Monoid m => (a > m) > Scope b f a > m # foldMap' :: Monoid m => (a > m) > Scope b f a > m # foldr :: (a > b0 > b0) > b0 > Scope b f a > b0 # foldr' :: (a > b0 > b0) > b0 > Scope b f a > b0 # foldl :: (b0 > a > b0) > b0 > Scope b f a > b0 # foldl' :: (b0 > a > b0) > b0 > Scope b f a > b0 # foldr1 :: (a > a > a) > Scope b f a > a # foldl1 :: (a > a > a) > Scope b f a > a # toList :: Scope b f a > [a] # length :: Scope b f a > Int # elem :: Eq a => a > Scope b f a > Bool # maximum :: Ord a => Scope b f a > a # minimum :: Ord a => Scope b f a > a #  
Traversable f => Traversable (Scope b f) Source #  
(Functor f, Eq1 f, Eq b) => Eq1 (Scope b f) Source #  
(Functor f, Show1 f, Show b) => Show1 (Scope b f) Source #  
(Eq e, Functor m, Eq1 m, Eq a) => Eq (Scope e m a) Source #  
(Show e, Functor m, Show1 m, Show a) => Show (Scope e m a) Source #  
type Rep1 (Scope b f :: Type > Type) Source #  
Defined in Bound.Simple 
Instances
Eq2 Var Source #  
Show2 Var Source #  
Functor (Var b) Source #  
Foldable (Var b) Source #  
Defined in Bound.Simple fold :: Monoid m => Var b m > m # foldMap :: Monoid m => (a > m) > Var b a > m # foldMap' :: Monoid m => (a > m) > Var b a > m # foldr :: (a > b0 > b0) > b0 > Var b a > b0 # foldr' :: (a > b0 > b0) > b0 > Var b a > b0 # foldl :: (b0 > a > b0) > b0 > Var b a > b0 # foldl' :: (b0 > a > b0) > b0 > Var b a > b0 # foldr1 :: (a > a > a) > Var b a > a # foldl1 :: (a > a > a) > Var b a > a # elem :: Eq a => a > Var b a > Bool # maximum :: Ord a => Var b a > a # minimum :: Ord a => Var b a > a #  
Traversable (Var b) Source #  
Eq b => Eq1 (Var b) Source #  
Show b => Show1 (Var b) Source #  
(Eq b, Eq a) => Eq (Var b a) Source #  
(Show b, Show a) => Show (Var b a) Source #  
Abstraction
abstract :: Functor f => (a > Maybe b) > f a > Scope b f a Source #
Capture some free variables in an expression to yield
a Scope
with bound variables in b
>>>
:m + Data.List
>>>
abstract (`elemIndex` "bar") "barry"
Scope [B 0,B 1,B 2,B 2,F 'y']
abstract1 :: (Functor f, Eq a) => a > f a > Scope () f a Source #
Abstract over a single variable
>>>
abstract1 'x' "xyz"
Scope [B (),F 'y',F 'z']
Instantiation
instantiate :: Monad f => (b > f a) > Scope b f a > f a Source #
Enter a scope, instantiating all bound variables
>>>
:m + Data.List
>>>
instantiate (\x > [toEnum (97 + x)]) $ abstract (`elemIndex` "bar") "barry"
"abccy"
instantiate1 :: Monad f => f a > Scope n f a > f a Source #
Enter a Scope
that binds one variable, instantiating it
>>>
instantiate1 "x" $ Scope [B (),F 'y',F 'z']
"xyz"
bindings :: Foldable f => Scope b f a > [b] Source #
Return a list of occurences of the variables bound by this Scope
.
closed :: Traversable f => f a > Maybe (f b) Source #
If a term has no free variables, you can freely change the type of free variables it is parameterized on.
>>>
closed [12]
Nothing
>>>
closed ""
Just []
>>>
:t closed ""
closed "" :: Maybe [b]
substitute :: (Monad f, Eq a) => a > f a > f a > f a Source #
replaces the free variable substitute
a p wa
with p
in w
.
>>>
substitute "hello" ["goodnight","Gracie"] ["hello","!!!"]
["goodnight","Gracie","!!!"]
substituteVar :: (Functor f, Eq a) => a > a > f a > f a Source #
replaces a free variable substituteVar
a b wa
with another free variable b
in w
.
>>>
substituteVar "Alice" "Bob" ["Alice","Bob","Charlie"]
["Bob","Bob","Charlie"]
Predicates
isClosed :: Foldable f => f a > Bool Source #
A closed term has no free variables.
>>>
isClosed []
True
>>>
isClosed [1,2,3]
False
Utils
newtype Generically f a Source #
Generically  

Instances
(Generic1 f, GEq1 (Rep1 f)) => Eq1 (Generically f) Source #  
Defined in Data.Functor.Classes.Generic liftEq :: (a > b > Bool) > Generically f a > Generically f b > Bool #  
(Generic1 f, GEq1 (Rep1 f), GOrd1 (Rep1 f)) => Ord1 (Generically f) Source #  
Defined in Data.Functor.Classes.Generic liftCompare :: (a > b > Ordering) > Generically f a > Generically f b > Ordering #  
(Generic1 f, GShow1 (Rep1 f)) => Show1 (Generically f) Source #  
Defined in Data.Functor.Classes.Generic liftShowsPrec :: (Int > a > ShowS) > ([a] > ShowS) > Int > Generically f a > ShowS # liftShowList :: (Int > a > ShowS) > ([a] > ShowS) > [Generically f a] > ShowS # 