Safe Haskell	None
Language	Haskell2010

Language.LambdaPi.Impl.Foil

Contents

Scope-safe AST
Pretty-printing
Substitution
Conversion
- From raw to foil
- From foil to raw
Evaluation
\(\alpha\)-equivalence
Interpreter
Example terms

Description

Foil implementation of the \(\lambda\Pi\)-calculus (with pairs).

The following is implemented manually in this module:

Scope-safe AST for \(\lambda\Pi\)-terms.
Correct capture-avoiding substitution (see substitute).
Conversion between scope-safe and raw term representation (the latter is generated via BNFC), see toFoilTerm and fromFoilTerm.
Helper functions for patterns. See extendScopePattern and withRefreshedPattern.
\(\alpha\)-equivalence checks (alphaEquiv and alphaEquivRefreshed) and \(\alpha\)-normalization helpers (refreshExpr).
Computation of weak head normal form (WHNF) and normal form (NF), see whnf and nf.
Entry point, gluing everything together. See defaultMain.

This implementation supports (nested) patterns for pairs.

This is a baseline implementation, see other examples for partial automation:

Language.LambdaPi.Impl.FreeFoil allows to reuse generalized substitution and \(\alpha\)-equivalence (and, in theory, more complicated algorithms).
Language.LambdaPi.Impl.FoilTH works well with patterns and generates conversion functions and helpers for patterns.
Language.LambdaPi.Impl.FreeFoilTH combines the benefits of the above, when it is possible to generate the signature automatically.

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). Pattern n l -> Expr l -> Expr n
- PiE :: forall (n :: S) (l :: S). Pattern n l -> Expr n -> Expr l -> Expr n
- PairE :: forall (n :: S). Expr n -> Expr n -> Expr n
- FirstE :: forall (n :: S). Expr n -> Expr n
- SecondE :: forall (n :: S). Expr n -> Expr n
- ProductE :: forall (n :: S). Expr n -> Expr n -> Expr n
- UniverseE :: forall (n :: S). Expr n
data Pattern (n :: S) (l :: S) where
- PatternWildcard :: forall (n :: S). Pattern n n
- PatternVar :: forall (n :: S) (l :: S). NameBinder n l -> Pattern n l
- PatternPair :: forall (n :: S) (i :: S) (l :: S). Pattern n i -> Pattern i l -> Pattern n l
ppName :: forall (n :: S). Name n -> String
ppExpr :: forall (n :: S). Expr n -> String
ppPattern :: forall (n :: S) (l :: S). Pattern n l -> String
printExpr :: Expr 'VoidS -> String
substitute :: forall (o :: S) (i :: S). Distinct o => Scope o -> Substitution Expr i o -> Expr i -> Expr o
substituteRefresh :: forall (o :: S) (i :: S). Distinct o => Scope o -> Substitution Expr i o -> Expr i -> Expr o
toFoilPattern :: forall (n :: S) r. Distinct n => Scope n -> Map VarIdent (Name n) -> Pattern -> (forall (l :: S). DExt n l => Pattern n l -> Map VarIdent (Name l) -> r) -> r
toFoilTerm :: forall (n :: S). Distinct n => Scope n -> Map VarIdent (Name n) -> Term -> Expr n
toFoilTermClosed :: Term -> Expr 'VoidS
fromFoilPattern :: forall (n :: S) (l :: S) r. [VarIdent] -> NameMap n VarIdent -> Pattern n l -> ([VarIdent] -> NameMap l VarIdent -> Pattern -> r) -> r
fromFoilTerm :: forall (n :: S). [VarIdent] -> NameMap n VarIdent -> Expr n -> Term
fromFoilTermClosed :: [VarIdent] -> Expr 'VoidS -> Term
fromFoilPattern' :: forall (n :: S) (l :: S). Pattern n l -> Pattern
fromFoilTerm' :: forall (n :: S). Expr n -> Term
matchPattern :: forall (n :: S) (l :: S). Pattern n l -> Expr n -> Substitution Expr l n
whnf :: forall (n :: S). Distinct n => Scope n -> Expr n -> Expr n
refreshExpr :: forall (n :: S). Distinct n => Scope n -> Expr n -> Expr n
alphaEquivRefreshed :: forall (n :: S). Distinct n => Scope n -> Expr n -> Expr n -> Bool
unsafeEqPattern :: forall (n :: S) (l :: S) (n' :: S) (l' :: S). Pattern n l -> Pattern n' l' -> Bool
unsafeEqExpr :: forall (n :: S) (l :: S). Expr n -> Expr l -> Bool
alphaEquiv :: forall (n :: S). Distinct n => Scope n -> Expr n -> Expr n -> Bool
interpretCommand :: Command -> IO ()
interpretProgram :: Program -> IO ()
defaultMain :: IO ()
lam :: forall (n :: S). Distinct n => Scope n -> (forall (l :: S). DExt n l => Scope l -> NameBinder n l -> Expr l) -> Expr n
identity :: Expr 'VoidS
churchN :: Int -> Expr 'VoidS

Documentation

>>> :set -XOverloadedStrings
>>> :set -XDataKinds
>>> import Control.Monad.Foil

Scope-safe AST

data Expr (n :: S) where Source #

Type of scope-safe \(\lambda\Pi\)-terms with pairs.

Constructors

VarE :: forall (n :: S). Name n -> Expr n	Variables: \(x\)
AppE :: forall (n :: S). Expr n -> Expr n -> Expr n	Application: \((t_1 \; t_2)\)
LamE :: forall (n :: S) (l :: S). Pattern n l -> Expr l -> Expr n	Abstraction (with patterns): \(\lambda p. t\)
PiE :: forall (n :: S) (l :: S). Pattern n l -> Expr n -> Expr l -> Expr n	\(\prod\)-types (with patterns): \(\prod_{p : T_1} T_2\)
PairE :: forall (n :: S). Expr n -> Expr n -> Expr n	Pair of terms: \(\langle t_1, t_2 \rangle\)
FirstE :: forall (n :: S). Expr n -> Expr n	First projection: \(\pi_1(t)\)
SecondE :: forall (n :: S). Expr n -> Expr n	Second projection: \(\pi_2(t)\)
ProductE :: forall (n :: S). Expr n -> Expr n -> Expr n	Product type (non-dependent): \(T_1 \times T_2\)
UniverseE :: forall (n :: S). Expr n	Universe (type of types): \(\mathcal{U}\)

Instances

Instances details

InjectName Expr Source #
Instance details Defined in Language.LambdaPi.Impl.Foil Methods injectName :: forall (n :: S). Name n -> Expr n #
Sinkable Expr Source #
Instance details Defined in Language.LambdaPi.Impl.Foil Methods sinkabilityProof :: forall (n :: S) (l :: S). (Name n -> Name l) -> Expr n -> Expr l #
RelMonad Name Expr Source #
Instance details Defined in Language.LambdaPi.Impl.Foil Methods rreturn :: forall (a :: S). Name a -> Expr a # rbind :: forall (b :: S) (a :: S). Distinct b => Scope b -> Expr a -> (Name a -> Expr b) -> Expr b #
IsString (Expr 'VoidS) Source #
Instance details Defined in Language.LambdaPi.Impl.Foil Methods fromString :: String -> Expr 'VoidS #
Show (Expr 'VoidS) Source #
Instance details Defined in Language.LambdaPi.Impl.Foil Methods showsPrec :: Int -> Expr 'VoidS -> ShowS # show :: Expr 'VoidS -> String # showList :: [Expr 'VoidS] -> ShowS #

data Pattern (n :: S) (l :: S) where Source #

Patterns.

Constructors

PatternWildcard :: forall (n :: S). Pattern n n	Wildcard pattern: \(_\)
PatternVar :: forall (n :: S) (l :: S). NameBinder n l -> Pattern n l	Variable pattern: \(x\)
PatternPair :: forall (n :: S) (i :: S) (l :: S). Pattern n i -> Pattern i l -> Pattern n l	Pair pattern: \((p_1, p_2)\)

Instances

Instances details

CoSinkable Pattern Source #
Instance details Defined in Language.LambdaPi.Impl.Foil Methods coSinkabilityProof :: forall (n :: S) (n' :: S) (l :: S) r. (Name n -> Name n') -> Pattern n l -> (forall (l' :: S). (Name l -> Name l') -> Pattern n' l' -> r) -> r # withPattern :: forall (o :: S) f (n :: S) (l :: S) r. Distinct o => (forall (x :: S) (y :: S) (z :: S) r'. Distinct z => Scope z -> NameBinder x y -> (forall (z' :: S). DExt z z' => f x y z z' -> NameBinder z z' -> r') -> r') -> (forall (x :: S) (z :: S) (z' :: S). DExt z z' => f x x z z') -> (forall (x :: S) (y :: S) (y' :: S) (z :: S) (z' :: S) (z'' :: S). (DExt z z', DExt z' z'') => f x y z z' -> f y y' z' z'' -> f x y' z z'') -> Scope o -> Pattern n l -> (forall (o' :: S). DExt o o' => f n l o o' -> Pattern o o' -> r) -> r #
UnifiablePattern Pattern Source #
Instance details Defined in Language.LambdaPi.Impl.Foil Methods unifyPatterns :: forall (n :: S) (l :: S) (r :: S). Distinct n => Pattern n l -> Pattern n r -> UnifyNameBinders Pattern n l r #

Pretty-printing

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

Default way to print a name using its internal Id.

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

Pretty-print a \(\lambda\Pi\)-term directly (without converting to raw term).

>>> ppExpr identity
"\955x0. x0"
>>> ppExpr (churchN 2)
"\955x0. \955x1. x0 (x0 (x1))"

ppPattern :: forall (n :: S) (l :: S). Pattern n l -> String Source #

Pretty-print a pattern in a \(\lambda\Pi\)-term (without converting to raw pattern)..

printExpr :: Expr 'VoidS -> String Source #

Pretty-print a closed scode-safe \(\lambda\Pi\)-term using BNFC-generated printer (via Term).

Substitution

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

Perform substitution in a \(\lambda\Pi\)-term.

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

Perform substitution in a \(\lambda\Pi\)-term and normalize binders in the process.

Conversion

From raw to foil

toFoilPattern Source #

Arguments

:: forall (n :: S) r. Distinct n
=> Scope n	Outer scope (outside of pattern binding).
-> Map VarIdent (Name n)	Mapping for variable names (to be extended with pattern).
-> Pattern	Raw pattern.
-> (forall (l :: S). DExt n l => Pattern n l -> Map VarIdent (Name l) -> r)	A continuation, accepting a scope-safe pattern and an updated variable mapping.
-> r

Convert a raw pattern into a scope-safe one.

toFoilTerm Source #

Arguments

:: forall (n :: S). Distinct n
=> Scope n	Target scope.
-> Map VarIdent (Name n)	Mapping for variable names (to be extended with pattern).
-> Term	A raw term.
-> Expr n

Convert a raw term into a scope-safe \(\lambda\Pi\)-term.

toFoilTermClosed :: Term -> Expr 'VoidS Source #

Convert a raw term into a closed scope-safe term.

From foil to raw

fromFoilPattern Source #

Arguments

:: forall (n :: S) (l :: S) r. [VarIdent]	A stream of fresh variable identifiers.
-> NameMap n VarIdent	A total mapping for names in scope `n`.
-> Pattern n l	A scope-safe pattern that extends scope `n` into scope `l`.
-> ([VarIdent] -> NameMap l VarIdent -> Pattern -> r)	A continutation, accepting (smaller) stream of fresh variable identifiers, a mapping for the inner scope, and a raw pattern.
-> r

Convert a scope-safe pattern into a raw pattern.

fromFoilTerm Source #

Arguments

:: forall (n :: S). [VarIdent]	A stream of fresh variable identifiers.
-> NameMap n VarIdent	A total mapping for names in scope `n`.
-> Expr n	A scope safe term in scope `n`.
-> Term

Convert a scope-safe term into a raw term.

fromFoilTermClosed Source #

Arguments

:: [VarIdent]	A stream of fresh variable identifiers.
-> Expr 'VoidS	A scope safe term in scope `n`.
-> Term

Convert a closed scope-safe term into a raw term.

fromFoilPattern' Source #

Arguments

:: forall (n :: S) (l :: S). Pattern n l	A scope-safe pattern that extends scope `n` into scope `l`.
-> Pattern

Convert a scope-safe pattern into a raw pattern converting raw identifiers directly into VarIdent

fromFoilTerm' Source #

Arguments

:: forall (n :: S). Expr n	A scope safe term in scope `n`.
-> Term

Convert a scope-safe term into a raw term converting raw identifiers directly into VarIdent.

Evaluation

matchPattern :: forall (n :: S) (l :: S). Pattern n l -> Expr n -> Substitution Expr l n Source #

Match a pattern against an expression.

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

Compute weak head normal form (WHNF).

>>> whnf emptyScope "(λx.(λ_.x)(λy.x))(λy.λz.z)"
λ x0 . λ x1 . x1

>>> whnf emptyScope "(λs.λz.s(s(z)))(λs.λz.s(s(z)))"
λ x1 . (λ x0 . λ x1 . x0 (x0 x1)) ((λ x0 . λ x1 . x0 (x0 x1)) x1)

Note that during computation bound variables can become unordered in the sense that binders may easily repeat or decrease. For example, in the following expression, inner binder has lower index that the outer one:

>>> whnf emptyScope "(λx.λy.x)(λx.x)"
λ x1 . λ x0 . x0

At the same time, without substitution, we get regular, increasing binder indices:

>>> "λx.λy.y" :: Expr VoidS
λ x0 . λ x1 . x1

To compare terms for \(\alpha\)-equivalence, we may use alphaEquiv:

>>> alphaEquiv emptyScope (whnf emptyScope "(λx.λy.x)(λx.x)") "λx.λy.y"
True

We may also normalize binders using refreshExpr:

>>> refreshExpr emptyScope (whnf emptyScope "(λx.λy.x)(λx.x)")
λ x0 . λ x1 . x1

\(\alpha\)-equivalence

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

Normalize all binder identifiers in an expression.

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

\(\alpha\)-equivalence check for two terms in one scope via normalization of bound identifiers (via refreshExpr).

This function may perform some unnecessary changes of bound variables when the binders are the same on both sides.

unsafeEqPattern :: forall (n :: S) (l :: S) (n' :: S) (l' :: S). Pattern n l -> Pattern n' l' -> Bool Source #

Unsafely check for equality of two Patterns.

This does not include \(\alpha\)-equivalence!

unsafeEqExpr :: forall (n :: S) (l :: S). Expr n -> Expr l -> Bool Source #

Unsafely check for equality of two Exprs.

This does not include \(\alpha\)-equivalence!

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

\(\alpha\)-equivalence check for two terms in one scope via unification of bound variables (via unifyNameBinders).

Compared to alphaEquivRefreshed, this function might skip unnecessary changes of bound variables when both binders in two matching scoped terms coincide.

Interpreter

interpretCommand :: Command -> IO () Source #

Interpret a \(\lambda\Pi\) command.

interpretProgram :: Program -> IO () Source #

Interpret a \(\lambda\Pi\) program.

defaultMain :: IO () Source #

Default interpreter program. Reads a \(\lambda\Pi\) program from the standard input and runs the commands.

Example terms

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.

identity :: Expr 'VoidS Source #

An identity function as a \(\lambda\)-term:

>>> identity
λ x0 . x0

churchN :: Int -> Expr 'VoidS Source #

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

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

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