Safe Haskell	None
Language	Haskell2010

Language.LambdaPi.Impl.FreeFoil

Description

Free foil implementation of the $\lambda\Pi$-calculus (with pairs).

Free foil provides general definitions or implementations for the following:

Freely generated (from a simple signature) scope-safe AST.
Correct capture-avoiding substitution (see substitute).
Correct α-equivalence checks (see alphaEquiv and alphaEquivRefreshed) as well as α-normalization (see refreshAST).
Conversion helpers (see convertToAST and convertFromAST).

The following is implemented manually in this module:

Convenient pattern synonyms.
ZipMatch instances (enabling general α-equivalence).
Conversion between scope-safe and raw term representation (the latter is generated via BNFC), see toLambdaPi and fromLambdaPi.
Computation of weak head normal form (WHNF), see whnf.
Entry point, gluing everything together. See defaultMain.

Note: free foil does not (easily) support patterns at the moment, so only wildcard patterns and variable patterns are handled in this implementation.

See Language.LambdaPi.Impl.FreeFoilTH for a variation of this with more automation via Template Haskell.

Synopsis

data LambdaPiF scope term
- = AppF term term
- | LamF scope
- | PiF term scope
- | UniverseF
data PairF scope term
- = PairF term term
- | FirstF term
- | SecondF term
- | ProductF term term
type (:+:) = Sum :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type
type LambdaPi (n :: S) = AST (LambdaPiF :+: PairF) n
pattern App :: LambdaPi n -> LambdaPi n -> LambdaPi n
pattern Lam :: () => NameBinder n l -> LambdaPi l -> LambdaPi n
pattern Pi :: () => NameBinder n l -> LambdaPi n -> LambdaPi l -> LambdaPi n
pattern Pair :: LambdaPi n -> LambdaPi n -> LambdaPi n
pattern First :: LambdaPi n -> LambdaPi n
pattern Second :: LambdaPi n -> LambdaPi n
pattern Product :: LambdaPi n -> LambdaPi n -> LambdaPi n
pattern Universe :: LambdaPi n
whnf :: forall (n :: S). Distinct n => Scope n -> LambdaPi n -> LambdaPi n
toLambdaPiLam :: forall (n :: S). Distinct n => Scope n -> Map VarIdent (Name n) -> Pattern -> ScopedTerm -> LambdaPi n
toLambdaPiPi :: forall (n :: S). Distinct n => Scope n -> Map VarIdent (Name n) -> Pattern -> Term -> ScopedTerm -> LambdaPi n
toLambdaPi :: forall (n :: S). Distinct n => Scope n -> Map VarIdent (Name n) -> Term -> LambdaPi n
toLambdaPiClosed :: Term -> LambdaPi 'VoidS
fromLambdaPi :: forall (n :: S). [VarIdent] -> NameMap n VarIdent -> LambdaPi n -> Term
fromLambdaPi' :: forall (n :: S). LambdaPi n -> Term
ppLambdaPi :: LambdaPi 'VoidS -> String
interpretCommand :: Command -> IO ()
interpretProgram :: Program -> IO ()
defaultMain :: IO ()

Documentation

>>> import qualified Control.Monad.Foil as Foil
>>> import Control.Monad.Free.Foil
>>> :set -XOverloadedStrings
>>> :set -XDataKinds

data LambdaPiF scope term Source #

The signature Bifunctor for the $\lambda\Pi$.

Constructors

AppF term term	Application: $(t_1 \; t_2)$
LamF scope	Abstraction: $\lambda x. t$
PiF term scope	Dependent function type: $\prod_{x : T_1} T_2$
UniverseF	Universe (type of types): $\mathcal{U}$

Instances

Instances details

Bifoldable LambdaPiF Source #
Instance details Defined in Language.LambdaPi.Impl.FreeFoil Methods bifold :: Monoid m => LambdaPiF m m -> m # bifoldMap :: Monoid m => (a -> m) -> (b -> m) -> LambdaPiF a b -> m # bifoldr :: (a -> c -> c) -> (b -> c -> c) -> c -> LambdaPiF a b -> c # bifoldl :: (c -> a -> c) -> (c -> b -> c) -> c -> LambdaPiF a b -> c #
Bifunctor LambdaPiF Source #
Instance details Defined in Language.LambdaPi.Impl.FreeFoil Methods bimap :: (a -> b) -> (c -> d) -> LambdaPiF a c -> LambdaPiF b d # first :: (a -> b) -> LambdaPiF a c -> LambdaPiF b c # second :: (b -> c) -> LambdaPiF a b -> LambdaPiF a c #
Bitraversable LambdaPiF Source #
Instance details Defined in Language.LambdaPi.Impl.FreeFoil Methods bitraverse :: Applicative f => (a -> f c) -> (b -> f d) -> LambdaPiF a b -> f (LambdaPiF c d) #
ZipMatch LambdaPiF Source #
Instance details Defined in Language.LambdaPi.Impl.FreeFoil Methods zipMatch :: LambdaPiF scope term -> LambdaPiF scope' term' -> Maybe (LambdaPiF (scope, scope') (term, term')) #
Foldable (LambdaPiF scope) Source #
Instance details Defined in Language.LambdaPi.Impl.FreeFoil Methods fold :: Monoid m => LambdaPiF scope m -> m # foldMap :: Monoid m => (a -> m) -> LambdaPiF scope a -> m # foldMap' :: Monoid m => (a -> m) -> LambdaPiF scope a -> m # foldr :: (a -> b -> b) -> b -> LambdaPiF scope a -> b # foldr' :: (a -> b -> b) -> b -> LambdaPiF scope a -> b # foldl :: (b -> a -> b) -> b -> LambdaPiF scope a -> b # foldl' :: (b -> a -> b) -> b -> LambdaPiF scope a -> b # foldr1 :: (a -> a -> a) -> LambdaPiF scope a -> a # foldl1 :: (a -> a -> a) -> LambdaPiF scope a -> a # toList :: LambdaPiF scope a -> [a] # null :: LambdaPiF scope a -> Bool # length :: LambdaPiF scope a -> Int # elem :: Eq a => a -> LambdaPiF scope a -> Bool # maximum :: Ord a => LambdaPiF scope a -> a # minimum :: Ord a => LambdaPiF scope a -> a # sum :: Num a => LambdaPiF scope a -> a # product :: Num a => LambdaPiF scope a -> a #
IsString (LambdaPi 'VoidS) Source #	$\lambda\Pi$-terms can be (unsafely) parsed from a `String` via `Term`.
Instance details Defined in Language.LambdaPi.Impl.FreeFoil Methods fromString :: String -> LambdaPi 'VoidS #
Traversable (LambdaPiF scope) Source #
Instance details Defined in Language.LambdaPi.Impl.FreeFoil Methods traverse :: Applicative f => (a -> f b) -> LambdaPiF scope a -> f (LambdaPiF scope b) # sequenceA :: Applicative f => LambdaPiF scope (f a) -> f (LambdaPiF scope a) # mapM :: Monad m => (a -> m b) -> LambdaPiF scope a -> m (LambdaPiF scope b) # sequence :: Monad m => LambdaPiF scope (m a) -> m (LambdaPiF scope a) #
Functor (LambdaPiF scope) Source #
Instance details Defined in Language.LambdaPi.Impl.FreeFoil Methods fmap :: (a -> b) -> LambdaPiF scope a -> LambdaPiF scope b # (<$) :: a -> LambdaPiF scope b -> LambdaPiF scope a #
Show (LambdaPi 'VoidS) Source #	$\lambda\Pi$-terms are pretty-printed using BNFC-generated printer via `Term`.
Instance details Defined in Language.LambdaPi.Impl.FreeFoil Methods showsPrec :: Int -> LambdaPi 'VoidS -> ShowS # show :: LambdaPi 'VoidS -> String # showList :: [LambdaPi 'VoidS] -> ShowS #
(Show term, Show scope) => Show (LambdaPiF scope term) Source #
Instance details Defined in Language.LambdaPi.Impl.FreeFoil Methods showsPrec :: Int -> LambdaPiF scope term -> ShowS # show :: LambdaPiF scope term -> String # showList :: [LambdaPiF scope term] -> ShowS #
(Eq term, Eq scope) => Eq (LambdaPiF scope term) Source #
Instance details Defined in Language.LambdaPi.Impl.FreeFoil Methods (==) :: LambdaPiF scope term -> LambdaPiF scope term -> Bool # (/=) :: LambdaPiF scope term -> LambdaPiF scope term -> Bool #

data PairF scope term Source #

The signature Bifunctor for pairs.

Constructors

PairF term term	Pair: $\langle t_1, t_2 \rangle$
FirstF term	First projection: $\pi_1(t)$
SecondF term	Second projection: $\pi_2(t)$
ProductF term term	Product type (non-dependent): $T_1 \times T_2$

Instances

Instances details

Bifoldable PairF Source #
Instance details Defined in Language.LambdaPi.Impl.FreeFoil Methods bifold :: Monoid m => PairF m m -> m # bifoldMap :: Monoid m => (a -> m) -> (b -> m) -> PairF a b -> m # bifoldr :: (a -> c -> c) -> (b -> c -> c) -> c -> PairF a b -> c # bifoldl :: (c -> a -> c) -> (c -> b -> c) -> c -> PairF a b -> c #
Bifunctor PairF Source #
Instance details Defined in Language.LambdaPi.Impl.FreeFoil Methods bimap :: (a -> b) -> (c -> d) -> PairF a c -> PairF b d # first :: (a -> b) -> PairF a c -> PairF b c # second :: (b -> c) -> PairF a b -> PairF a c #
Bitraversable PairF Source #
Instance details Defined in Language.LambdaPi.Impl.FreeFoil Methods bitraverse :: Applicative f => (a -> f c) -> (b -> f d) -> PairF a b -> f (PairF c d) #
ZipMatch PairF Source #
Instance details Defined in Language.LambdaPi.Impl.FreeFoil Methods zipMatch :: PairF scope term -> PairF scope' term' -> Maybe (PairF (scope, scope') (term, term')) #
Foldable (PairF scope) Source #
Instance details Defined in Language.LambdaPi.Impl.FreeFoil Methods fold :: Monoid m => PairF scope m -> m # foldMap :: Monoid m => (a -> m) -> PairF scope a -> m # foldMap' :: Monoid m => (a -> m) -> PairF scope a -> m # foldr :: (a -> b -> b) -> b -> PairF scope a -> b # foldr' :: (a -> b -> b) -> b -> PairF scope a -> b # foldl :: (b -> a -> b) -> b -> PairF scope a -> b # foldl' :: (b -> a -> b) -> b -> PairF scope a -> b # foldr1 :: (a -> a -> a) -> PairF scope a -> a # foldl1 :: (a -> a -> a) -> PairF scope a -> a # toList :: PairF scope a -> [a] # null :: PairF scope a -> Bool # length :: PairF scope a -> Int # elem :: Eq a => a -> PairF scope a -> Bool # maximum :: Ord a => PairF scope a -> a # minimum :: Ord a => PairF scope a -> a # sum :: Num a => PairF scope a -> a # product :: Num a => PairF scope a -> a #
IsString (LambdaPi 'VoidS) Source #	$\lambda\Pi$-terms can be (unsafely) parsed from a `String` via `Term`.
Instance details Defined in Language.LambdaPi.Impl.FreeFoil Methods fromString :: String -> LambdaPi 'VoidS #
Traversable (PairF scope) Source #
Instance details Defined in Language.LambdaPi.Impl.FreeFoil Methods traverse :: Applicative f => (a -> f b) -> PairF scope a -> f (PairF scope b) # sequenceA :: Applicative f => PairF scope (f a) -> f (PairF scope a) # mapM :: Monad m => (a -> m b) -> PairF scope a -> m (PairF scope b) # sequence :: Monad m => PairF scope (m a) -> m (PairF scope a) #
Functor (PairF scope) Source #
Instance details Defined in Language.LambdaPi.Impl.FreeFoil Methods fmap :: (a -> b) -> PairF scope a -> PairF scope b # (<$) :: a -> PairF scope b -> PairF scope a #
Show (LambdaPi 'VoidS) Source #	$\lambda\Pi$-terms are pretty-printed using BNFC-generated printer via `Term`.
Instance details Defined in Language.LambdaPi.Impl.FreeFoil Methods showsPrec :: Int -> LambdaPi 'VoidS -> ShowS # show :: LambdaPi 'VoidS -> String # showList :: [LambdaPi 'VoidS] -> ShowS #
Show term => Show (PairF scope term) Source #
Instance details Defined in Language.LambdaPi.Impl.FreeFoil Methods showsPrec :: Int -> PairF scope term -> ShowS # show :: PairF scope term -> String # showList :: [PairF scope term] -> ShowS #
Eq term => Eq (PairF scope term) Source #
Instance details Defined in Language.LambdaPi.Impl.FreeFoil Methods (==) :: PairF scope term -> PairF scope term -> Bool # (/=) :: PairF scope term -> PairF scope term -> Bool #

type (:+:) = Sum :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type Source #

Sum of signature bifunctors.

type LambdaPi (n :: S) = AST (LambdaPiF :+: PairF) n Source #

$\lambda\Pi$-terms in scope n, freely generated from the sum of signatures LambdaPiF and PairF.

pattern App :: LambdaPi n -> LambdaPi n -> LambdaPi n Source #

pattern Lam :: () => NameBinder n l -> LambdaPi l -> LambdaPi n Source #

pattern Pi :: () => NameBinder n l -> LambdaPi n -> LambdaPi l -> LambdaPi n Source #

pattern Pair :: LambdaPi n -> LambdaPi n -> LambdaPi n Source #

pattern First :: LambdaPi n -> LambdaPi n Source #

pattern Second :: LambdaPi n -> LambdaPi n Source #

pattern Product :: LambdaPi n -> LambdaPi n -> LambdaPi n Source #

pattern Universe :: LambdaPi n Source #

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

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

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

>>> whnf Foil.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 Foil.emptyScope "(λx.λy.x)(λx.x)"
λ x1 . λ x0 . x0

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

>>> "λx.λy.y" :: LambdaPi Foil.VoidS
λ x0 . λ x1 . x1

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

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

We may also normalize binders using refreshAST:

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

toLambdaPiLam Source #

Arguments

:: forall (n :: S). Distinct n
=> Scope n	Target scope of the $\lambda\Pi$-term.
-> Map VarIdent (Name n)	Mapping for the free variables in the raw term.
-> Pattern	Raw pattern (argument) of the $\lambda$-abstraction.
-> ScopedTerm	Raw body of the $\lambda$-abstraction.
-> LambdaPi n

Convert a raw $\lambda$-abstraction into a scope-safe $\lambda\Pi$-term.

toLambdaPiPi Source #

Arguments

:: forall (n :: S). Distinct n
=> Scope n	Target scope of the $\lambda\Pi$-term.
-> Map VarIdent (Name n)	Mapping for the free variables in the raw term.
-> Pattern	Raw argument pattern of the $\Pi$-type.
-> Term	Raw argument type of the $\Pi$-type.
-> ScopedTerm	Raw body (result type family) of the $\Pi$-type.
-> LambdaPi n

Convert a raw $\Pi$-type into a scope-safe $\lambda\Pi$-term.

toLambdaPi Source #

Arguments

:: forall (n :: S). Distinct n
=> Scope n	Target scope of the $\lambda\Pi$-term.
-> Map VarIdent (Name n)	Mapping for the free variables in the raw term.
-> Term	Raw expression or type.
-> LambdaPi n

Convert a raw expression into a scope-safe $\lambda\Pi$-term.

toLambdaPiClosed :: Term -> LambdaPi 'VoidS Source #

Convert a raw expression into a closed scope-safe $\lambda\Pi$-term.

fromLambdaPi Source #

Arguments

:: forall (n :: S). [VarIdent]	Stream of fresh raw identifiers.
-> NameMap n VarIdent	A total map for all names in scope `n`.
-> LambdaPi n	A scope-safe $\lambda\Pi$-term.
-> Term

Convert back from a scope-safe $\lambda\Pi$-term into a raw expression or type.

fromLambdaPi' Source #

Arguments

:: forall (n :: S). LambdaPi n	A scope-safe $\lambda\Pi$-term.
-> Term

Convert back from a scope-safe $\lambda\Pi$-term into a raw expression or type.

In contrast to fromLambdaPi, this function uses the raw foil identifiers (integers) to generate names for the variables. This makes them transparent when printing.

ppLambdaPi :: LambdaPi 'VoidS -> String Source #

Pretty-print a closed $\lambda\Pi$-term.

interpretCommand :: Command -> IO () Source #

Interpret a λΠ command.

interpretProgram :: Program -> IO () Source #

Interpret a λΠ program.

defaultMain :: IO () Source #

A $\lambda\Pi$ interpreter implemented via the free foil.

AppF term term	Application: \((t_1 \; t_2)\)
LamF scope	Abstraction: \(\lambda x. t\)
PiF term scope	Dependent function type: \(\prod_{x : T_1} T_2\)
UniverseF	Universe (type of types): \(\mathcal{U}\)

PairF term term	Pair: \(\langle t_1, t_2 \rangle\)
FirstF term	First projection: \(\pi_1(t)\)
SecondF term	Second projection: \(\pi_2(t)\)
ProductF term term	Product type (non-dependent): \(T_1 \times T_2\)

:: forall (n :: S). Distinct n
=> Scope n	Target scope of the \(\lambda\Pi\)-term.
-> Map VarIdent (Name n)	Mapping for the free variables in the raw term.
-> Pattern	Raw pattern (argument) of the \(\lambda\)-abstraction.
-> ScopedTerm	Raw body of the \(\lambda\)-abstraction.
-> LambdaPi n

:: forall (n :: S). LambdaPi n	A scope-safe \(\lambda\Pi\)-term.
-> Term