Safe Haskell | None |
---|---|
Language | Haskell2010 |
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 \(\alpha\)-equivalence checks (see
alphaEquiv
andalphaEquivRefreshed
) as well as \(\alpha\)-normalization (seerefreshAST
). - Conversion helpers (see
convertToAST
andconvertFromAST
).
The following is implemented manually in this module:
- Convenient pattern synonyms.
ZipMatch
instances (enabling general \(\alpha\)-equivalence).- Conversion between scope-safe and raw term representation (the latter is generated via BNFC), see
toLambdaPi
andfromLambdaPi
. - 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
- data PairF scope term
- type (:+:) = Sum :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type
- type LambdaPi (n :: S) = AST NameBinder (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\).
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
Bifoldable LambdaPiF Source # | |
Bifunctor LambdaPiF Source # | |
Bitraversable LambdaPiF Source # | |
Defined in Language.LambdaPi.Impl.FreeFoil bitraverse :: Applicative f => (a -> f c) -> (b -> f d) -> LambdaPiF a b -> f (LambdaPiF c d) # | |
ZipMatch LambdaPiF Source # | |
Foldable (LambdaPiF scope) Source # | |
Defined in Language.LambdaPi.Impl.FreeFoil 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 # | |
IsString (LambdaPi 'VoidS) Source # | \(\lambda\Pi\)-terms can be (unsafely) parsed from a |
Defined in Language.LambdaPi.Impl.FreeFoil fromString :: String -> LambdaPi 'VoidS # | |
Traversable (LambdaPiF scope) Source # | |
Defined in Language.LambdaPi.Impl.FreeFoil 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 # | |
Show (LambdaPi 'VoidS) Source # | \(\lambda\Pi\)-terms are pretty-printed using BNFC-generated printer via |
(Show term, Show scope) => Show (LambdaPiF scope term) Source # | |
(Eq term, Eq scope) => Eq (LambdaPiF scope term) Source # | |
data PairF scope term Source #
The signature Bifunctor
for pairs.
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
Bifoldable PairF Source # | |
Bifunctor PairF Source # | |
Bitraversable PairF Source # | |
Defined in Language.LambdaPi.Impl.FreeFoil bitraverse :: Applicative f => (a -> f c) -> (b -> f d) -> PairF a b -> f (PairF c d) # | |
ZipMatch PairF Source # | |
Foldable (PairF scope) Source # | |
Defined in Language.LambdaPi.Impl.FreeFoil 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 # | |
IsString (LambdaPi 'VoidS) Source # | \(\lambda\Pi\)-terms can be (unsafely) parsed from a |
Defined in Language.LambdaPi.Impl.FreeFoil fromString :: String -> LambdaPi 'VoidS # | |
Traversable (PairF scope) Source # | |
Defined in Language.LambdaPi.Impl.FreeFoil | |
Functor (PairF scope) Source # | |
Show (LambdaPi 'VoidS) Source # | \(\lambda\Pi\)-terms are pretty-printed using BNFC-generated printer via |
Show term => Show (PairF scope term) Source # | |
Eq term => Eq (PairF scope term) Source # | |
type (:+:) = Sum :: (Type -> Type -> Type) -> (Type -> Type -> Type) -> Type -> Type -> Type Source #
Sum of signature bifunctors.
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
:: 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.
:: 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.
:: 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.
:: forall (n :: S). [VarIdent] | Stream of fresh raw identifiers. |
-> NameMap n VarIdent | A total map for all names in scope |
-> LambdaPi n | A scope-safe \(\lambda\Pi\)-term. |
-> Term |
Convert back from a scope-safe \(\lambda\Pi\)-term into a raw expression or type.
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.
interpretCommand :: Command -> IO () Source #
Interpret a \(\lambda\Pi\) command.
interpretProgram :: Program -> IO () Source #
Interpret a \(\lambda\Pi\) program.
defaultMain :: IO () Source #
A \(\lambda\Pi\) interpreter implemented via the free foil.