Bound.Simple

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. 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 = 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.2.0.0-4iD2bfDGGww6cAmTRQGquA" '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