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
- 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
- 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\) |
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))
whnf' :: Expr 'VoidS -> Expr 'VoidS Source #
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))))
nf' :: Expr 'VoidS -> Expr 'VoidS Source #
Compute normal form (NF) of a closed \(\lambda\)-term.
>>>
nf' (AppE (churchN 2) (churchN 2))
λx1. λx2. (x1 (x1 (x1 (x1 x2))))
ppExpr :: forall (n :: S). Expr n -> String Source #
Pretty-print a \(\lambda\)-term.
>>>
ppExpr (churchN 3)
"\955x0. \955x1. (x0 (x0 (x0 x1)))"