Bound.Simple

Scope is to be used inside of the definition of binders.

A lightweight implementation of bound. Provides much of the functionality of Bound.Scope.Simple, without the large dependency footprint.

Example

The whnf function in this example shows how to beta-reduce 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 thanks to DerivingVia. This works on most recent versions of GHC (>= 8.6.1).

{--}
{--}
{--}

import Bound.Simple (Scope, Bound(..), abstract1, instantiate1)
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 = lam x (V x) :@ V y
  print term         -- Lam (Scope (V (B ()))) :@ V y
  print $ whnf term  -- V y

Documentation

class Bound t where

Minimal complete definition

Nothing

Methods

(>>>=) :: Monad f => t f a -> (a -> f c) -> t f c

Perform substitution

If t is an instance of MonadTrans and you are compiling on GHC >= 7.4, then this gets the default definition:

m >>>= f = m >>= lift . f

default (>>>=) :: (MonadTrans t, Monad f, Monad (t f)) => t f a -> (a -> f c) -> t f c

Instances

Bound (Scope b)

Defined in Bound.Simple

Methods

(>>>=) :: Monad f => Scope b f a -> (a -> f c) -> Scope b f c

data Scope b f a

Scope b f a is an f expression with bound variables in b, and free variables in a

Instances

Bound (Scope b)

Defined in Bound.Simple

Methods

(>>>=) :: Monad f => Scope b f a -> (a -> f c) -> Scope b f c

Functor f => Generic1 (Scope b f :: Type -> Type)

Defined in Bound.Simple

Associated Types

type Rep1 (Scope b f) :: k -> Type

Methods

from1 :: forall (a :: k). Scope b f a -> Rep1 (Scope b f) a

to1 :: forall (a :: k). Rep1 (Scope b f) a -> Scope b f a

Monad f => Monad (Scope b f)

The monad permits substitution on free variables, while preserving bound variables

Defined in Bound.Simple

Methods

(>>=) :: Scope b f a -> (a -> Scope b f b0) -> Scope b f b0

(>>) :: Scope b f a -> Scope b f b0 -> Scope b f b0

return :: a -> Scope b f a

Functor f => Functor (Scope b f)

Defined in Bound.Simple

Methods

fmap :: (a -> b0) -> Scope b f a -> Scope b f b0

(<$) :: a -> Scope b f b0 -> Scope b f a

Monad f => Applicative (Scope b f)

Defined in Bound.Simple

Methods

pure :: a -> Scope b f a

(<*>) :: Scope b f (a -> b0) -> Scope b f a -> Scope b f b0

liftA2 :: (a -> b0 -> c) -> Scope b f a -> Scope b f b0 -> Scope b f c

(*>) :: Scope b f a -> Scope b f b0 -> Scope b f b0

(<*) :: Scope b f a -> Scope b f b0 -> Scope b f a

Foldable f => Foldable (Scope b f)

toList is provides a list (with duplicates) of the free variables

Defined in Bound.Simple

Methods

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]

null :: Scope b f a -> Bool

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

sum :: Num a => Scope b f a -> a

product :: Num a => Scope b f a -> a

Traversable f => Traversable (Scope b f)

Defined in Bound.Simple

Methods

traverse :: Applicative f0 => (a -> f0 b0) -> Scope b f a -> f0 (Scope b f b0)

sequenceA :: Applicative f0 => Scope b f (f0 a) -> f0 (Scope b f a)

mapM :: Monad m => (a -> m b0) -> Scope b f a -> m (Scope b f b0)

sequence :: Monad m => Scope b f (m a) -> m (Scope b f a)

(Functor f, Eq1 f, Eq b) => Eq1 (Scope b f)

Defined in Bound.Simple

Methods

liftEq :: (a -> b0 -> Bool) -> Scope b f a -> Scope b f b0 -> Bool

(Functor f, Show1 f, Show b) => Show1 (Scope b f)

Defined in Bound.Simple

Methods

liftShowsPrec :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> Scope b f a -> ShowS

liftShowList :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> [Scope b f a] -> ShowS

(Eq e, Functor m, Eq1 m, Eq a) => Eq (Scope e m a)

Defined in Bound.Simple

Methods

(==) :: Scope e m a -> Scope e m a -> Bool

(/=) :: Scope e m a -> Scope e m a -> Bool

(Show e, Functor m, Show1 m, Show a) => Show (Scope e m a)

Defined in Bound.Simple

Methods

showsPrec :: Int -> Scope e m a -> ShowS

show :: Scope e m a -> String

showList :: [Scope e m a] -> ShowS

type Rep1 (Scope b f :: Type -> Type)

Defined in Bound.Simple

type Rep1 (Scope b f :: Type -> Type) = D1 ('MetaData "Scope" "Bound.Simple" "bound-simple-0.1.0.0-8WxpELcM4nh6dCmAaAmaLC" 'True) (C1 ('MetaCons "Scope" 'PrefixI 'True) (S1 ('MetaSel ('Just "unscope") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (f :.: Rec1 (Var b))))

toScope :: f (Var b a) -> Scope b f a

toScope is just another name for Scope

fromScope :: Scope b f a -> f (Var b a)

fromScope is just another name for unscope

data Var b a

Instances

Eq2 Var

Defined in Bound.Simple

Methods

liftEq2 :: (a -> b -> Bool) -> (c -> d -> Bool) -> Var a c -> Var b d -> Bool

Show2 Var

Defined in Bound.Simple

Methods

liftShowsPrec2 :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> (Int -> b -> ShowS) -> ([b] -> ShowS) -> Int -> Var a b -> ShowS

liftShowList2 :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> (Int -> b -> ShowS) -> ([b] -> ShowS) -> [Var a b] -> ShowS

Functor (Var b)

Defined in Bound.Simple

Methods

fmap :: (a -> b0) -> Var b a -> Var b b0

(<$) :: a -> Var b b0 -> Var b a

Foldable (Var b)

Defined in Bound.Simple

Methods

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

toList :: Var b a -> [a]

null :: Var b a -> Bool

length :: Var b a -> Int

elem :: Eq a => a -> Var b a -> Bool

maximum :: Ord a => Var b a -> a

minimum :: Ord a => Var b a -> a

sum :: Num a => Var b a -> a

product :: Num a => Var b a -> a

Traversable (Var b)

Defined in Bound.Simple

Methods

traverse :: Applicative f => (a -> f b0) -> Var b a -> f (Var b b0)

sequenceA :: Applicative f => Var b (f a) -> f (Var b a)

mapM :: Monad m => (a -> m b0) -> Var b a -> m (Var b b0)

sequence :: Monad m => Var b (m a) -> m (Var b a)

Eq b => Eq1 (Var b)

Defined in Bound.Simple

Methods

liftEq :: (a -> b0 -> Bool) -> Var b a -> Var b b0 -> Bool

Show b => Show1 (Var b)

Defined in Bound.Simple

Methods

liftShowsPrec :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> Var b a -> ShowS

liftShowList :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> [Var b a] -> ShowS

(Eq b, Eq a) => Eq (Var b a)

Defined in Bound.Simple

Methods

(==) :: Var b a -> Var b a -> Bool

(/=) :: Var b a -> Var b a -> Bool

(Show b, Show a) => Show (Var b a)

Defined in Bound.Simple

Methods

showsPrec :: Int -> Var b a -> ShowS

show :: Var b a -> String

showList :: [Var b a] -> ShowS

Abstraction

abstract :: Functor f => (a -> Maybe b) -> f a -> Scope b f a

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

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

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

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]

Return a list of occurences of the variables bound by this Scope.

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)

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

substitute a p w replaces the free variable a with p in w.

>>> substitute "hello" ["goodnight","Gracie"] ["hello","!!!"]
["goodnight","Gracie","!!!"]

substituteVar :: (Functor f, Eq a) => a -> a -> f a -> f a

substituteVar a b w replaces a free variable a with another free variable b in w.

>>> substituteVar "Alice" "Bob" ["Alice","Bob","Charlie"]
["Bob","Bob","Charlie"]

Predicates

isClosed :: Foldable f => f a -> Bool

A closed term has no free variables.

>>> isClosed []
True

>>> isClosed [1,2,3]
False

Utils

newtype Generically f a

Used with the DerivingVia extension to provide fast derivations for Eq1, Show1, and Ord1.

Constructors

Generically

Fields

• unGenerically :: f a

Instances

(Generic1 f, GEq1 (Rep1 f)) => Eq1 (Generically f)

Defined in Data.Functor.Classes.Generic

Methods

liftEq :: (a -> b -> Bool) -> Generically f a -> Generically f b -> Bool

(Generic1 f, GEq1 (Rep1 f), GOrd1 (Rep1 f)) => Ord1 (Generically f)

Defined in Data.Functor.Classes.Generic

Methods

liftCompare :: (a -> b -> Ordering) -> Generically f a -> Generically f b -> Ordering

(Generic1 f, GShow1 (Rep1 f)) => Show1 (Generically f)

Defined in Data.Functor.Classes.Generic

Methods

liftShowsPrec :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> Generically f a -> ShowS

liftShowList :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> [Generically f a] -> ShowS