Safe Haskell	None
Language	Haskell2010

Control.Monad.Free.Foil.Example

Description

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

Synopsis

data ExprF scope term
- = AppF term term
- | LamF scope
pattern AppE :: AST ExprF n -> AST ExprF n -> AST ExprF n
pattern LamE :: () => NameBinder n l -> AST ExprF l -> AST ExprF n
type Expr = AST ExprF
whnf :: forall (n :: S). Distinct n => Scope n -> Expr n -> Expr n
whnf' :: Expr 'VoidS -> Expr 'VoidS
nf :: forall (n :: S). Distinct n => Scope n -> Expr n -> Expr n
nf' :: Expr 'VoidS -> Expr 'VoidS
ppName :: forall (n :: S). Name n -> String
ppExpr :: forall (n :: S). Expr n -> String
lam :: forall (n :: S). Distinct n => Scope n -> (forall (l :: S). DExt n l => Scope l -> NameBinder n l -> Expr l) -> Expr n
churchN :: Int -> Expr 'VoidS

Documentation

>>> import Control.Monad.Foil

data ExprF scope term Source #

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 details

Bifunctor ExprF Source #
Instance details 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) Source #
Instance details 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) Source #	Use `ppExpr` to show $\lambda$-terms.
Instance details Defined in Control.Monad.Free.Foil.Example Methods showsPrec :: Int -> Expr n -> ShowS # show :: Expr n -> String # showList :: [Expr n] -> ShowS #

pattern LamE :: () => NameBinder n l -> AST ExprF l -> AST ExprF n Source #

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

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))

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 Source #

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

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

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 Source #

Pretty print a name.

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

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 Source #

A helper for constructing $\lambda$-abstractions.

Church-encoding of a natural number $n$.

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

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

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\)