Control.Monad.Free.Foil.Example

Example implementation of untyped \(\lambda\)-calculus with the foil.

Documentation

>>> import Control.Monad.Foil

data ExprF scope term

Untyped \(\lambda\)-terms in scope n.

Constructors

AppF term term

Application of one term to another: \((t_1, t_2)\)

LamF scope

\(\lambda\)-abstraction introduces a binder and a term in an extended scope: \(\lambda x. t\)

Instances

Bifunctor ExprF

Defined in Control.Monad.Free.Foil.Example

Methods

bimap :: (a -> b) -> (c -> d) -> ExprF a c -> ExprF b d

first :: (a -> b) -> ExprF a c -> ExprF b c

second :: (b -> c) -> ExprF a b -> ExprF a c

Functor (ExprF scope)

Defined in Control.Monad.Free.Foil.Example

Methods

fmap :: (a -> b) -> ExprF scope a -> ExprF scope b

(<$) :: a -> ExprF scope b -> ExprF scope a

Show (Expr n)

Use ppExpr to show \(\lambda\)-terms.

Defined in Control.Monad.Free.Foil.Example

Methods

showsPrec :: Int -> Expr n -> ShowS

show :: Expr n -> String

showList :: [Expr n] -> ShowS

pattern AppE :: AST binder ExprF n -> AST binder ExprF n -> AST binder ExprF n

pattern LamE :: () => binder n l -> AST binder ExprF l -> AST binder ExprF n

type Expr = AST NameBinder ExprF

whnf :: forall (n :: S). Distinct n => Scope n -> Expr n -> Expr n

Compute weak head normal form (WHNF) of a \(\lambda\)-term.

>>> whnf emptyScope (AppE (churchN 2) (churchN 2))
λx1. (λx0. λx1. (x0 (x0 x1)) (λx0. λx1. (x0 (x0 x1)) x1))

whnf' :: Expr 'VoidS -> Expr 'VoidS

Compute weak head normal form (WHNF) of a closed \(\lambda\)-term.

>>> whnf' (AppE (churchN 2) (churchN 2))
λx1. (λx0. λx1. (x0 (x0 x1)) (λx0. λx1. (x0 (x0 x1)) x1))

nf :: forall (n :: S). Distinct n => Scope n -> Expr n -> Expr n

Compute normal form (NF) of a \(\lambda\)-term.

>>> nf emptyScope (AppE (churchN 2) (churchN 2))
λx1. λx2. (x1 (x1 (x1 (x1 x2))))

nf' :: Expr 'VoidS -> Expr 'VoidS

Compute normal form (NF) of a closed \(\lambda\)-term.

>>> nf' (AppE (churchN 2) (churchN 2))
λx1. λx2. (x1 (x1 (x1 (x1 x2))))

ppName :: forall (n :: S). Name n -> String

Pretty print a name.

ppExpr :: forall (n :: S). Expr n -> String

Pretty-print a \(\lambda\)-term.

>>> ppExpr (churchN 3)
"\955x0. \955x1. (x0 (x0 (x0 x1)))"

lam :: forall (n :: S). Distinct n => Scope n -> (forall (l :: S). DExt n l => Scope l -> NameBinder n l -> Expr l) -> Expr n

A helper for constructing \(\lambda\)-abstractions.

churchN :: Int -> Expr 'VoidS

Church-encoding of a natural number \(n\).

>>> churchN 0
λx0. λx1. x1

>>> churchN 3
λx0. λx1. (x0 (x0 (x0 x1)))