Safe Haskell	None
Language	Haskell2010

Control.Monad.Foil.Example

Description

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

Synopsis

data Expr (n :: S) where
- VarE :: forall (n :: S). Name n -> Expr n
- AppE :: forall (n :: S). Expr n -> Expr n -> Expr n
- LamE :: forall (n :: S) (l :: S). NameBinder n l -> Expr l -> Expr n
substitute :: forall (o :: S) (i :: S). Distinct o => Scope o -> Substitution Expr i o -> Expr i -> Expr o
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 Expr (n :: S) where Source #

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

Constructors

VarE :: forall (n :: S). Name n -> Expr n	Variables are names in scope `n`: \(x\)
AppE :: forall (n :: S). Expr n -> Expr n -> Expr n	Application of one term to another: \((t_1, t_2)\)
LamE :: forall (n :: S) (l :: S). NameBinder n l -> Expr l -> Expr n	\(\lambda\)-abstraction introduces a binder and a term in an extended scope: \(\lambda x. t\)

Instances details

InjectName Expr Source #
Instance details Defined in Control.Monad.Foil.Example Methods injectName :: forall (n :: S). Name n -> Expr n Source #
Sinkable Expr Source #	This instance serves as a proof that sinking of `Expr` is safe.
Instance details Defined in Control.Monad.Foil.Example Methods sinkabilityProof :: forall (n :: S) (l :: S). (Name n -> Name l) -> Expr n -> Expr l Source #
RelMonad Name Expr Source #	`Expr` is a monad relative to `Name`.
Instance details Defined in Control.Monad.Foil.Example Methods rreturn :: forall (a :: S). Name a -> Expr a Source # rbind :: forall (b :: S) (a :: S). Distinct b => Scope b -> Expr a -> (Name a -> Expr b) -> Expr b Source #
Show (Expr n) Source #	Use `ppExpr` to show \(\lambda\)-terms.
Instance details Defined in Control.Monad.Foil.Example Methods showsPrec :: Int -> Expr n -> ShowS # show :: Expr n -> String # showList :: [Expr n] -> ShowS #
NFData (Expr l) Source #
Instance details Defined in Control.Monad.Foil.Example Methods rnf :: Expr l -> () #

substitute :: forall (o :: S) (i :: S). Distinct o => Scope o -> Substitution Expr i o -> Expr i -> Expr o Source #

Substitution for untyped \(\lambda\)-terms. The foil helps implement this function without forgetting scope extensions and renaming.

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