Safe Haskell	None
Language	Haskell2010

Language.LambdaPi.Impl.FreeFoilTH

Contents

Generated code
User-defined code

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 generated using Template Haskell:

Convenient pattern synonyms.
ZipMatch instances (enabling general α-equivalence).
Conversion between scope-safe and raw term representation.

The following is implemented manually in this module:

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.

Synopsis

data Term'Sig a scope term
- = PiSig a term scope
- | LamSig a scope
- | AppSig a term term
- | ProductSig a term term
- | PairSig a term term
- | FirstSig a term
- | SecondSig a term
- | UniverseSig a
pattern Universe :: a -> AST (Term'Sig a) n
pattern Second :: a -> AST (Term'Sig a) n -> AST (Term'Sig a) n
pattern First :: a -> AST (Term'Sig a) n -> AST (Term'Sig a) n
pattern Pair :: a -> AST (Term'Sig a) n -> AST (Term'Sig a) n -> AST (Term'Sig a) n
pattern Product :: a -> AST (Term'Sig a) n -> AST (Term'Sig a) n -> AST (Term'Sig a) n
pattern App :: a -> AST (Term'Sig a) n -> AST (Term'Sig a) n -> AST (Term'Sig a) n
pattern Lam :: () => a -> NameBinder n l1 -> AST (Term'Sig a) l1 -> AST (Term'Sig a) n
pattern Pi :: () => a -> AST (Term'Sig a) n -> NameBinder n l2 -> AST (Term'Sig a) l2 -> AST (Term'Sig a) n
convertToTerm'Sig :: Term' a -> Either VarIdent (Term'Sig a (Pattern' a, ScopedTerm' a) (Term' a))
getPattern'Binder :: Pattern' a -> Maybe VarIdent
getTerm'FromScopedTerm' :: ScopedTerm' a -> Term' a
convertFromTerm'Sig :: Term'Sig a (Pattern' a, ScopedTerm' a) (Term' a) -> Term' a
type Term' a = AST (Term'Sig a)
type Term = Term' BNFC'Position
toTerm' :: forall (n :: S) a. Distinct n => Scope n -> Map VarIdent (Name n) -> Term' a -> AST (Term'Sig a) n
toTerm'Closed :: Term' a -> AST (Term'Sig a) 'VoidS
fromTerm' :: forall a (n :: S). AST (Term'Sig a) n -> Term' a
whnf :: forall (n :: S). Distinct n => Scope n -> Term n -> Term n
interpretCommand :: Command -> IO ()
interpretProgram :: Program -> IO ()
defaultMain :: IO ()

Documentation

>>> :set -XOverloadedStrings
>>> :set -XDataKinds
>>> import qualified Control.Monad.Foil as Foil
>>> import Control.Monad.Free.Foil
>>> import Data.String (fromString)

Generated code

Signature

data Term'Sig a scope term Source #

Generated with mkSignature. A signature bifunctor, specifying the nodes of a syntax tree corresponding to Term'.

Constructors

PiSig a term scope	Corresponds to `Pi`.
LamSig a scope	Corresponds to `Lam`.
AppSig a term term	Corresponds to `App`.
ProductSig a term term	Corresponds to `Product`.
PairSig a term term	Corresponds to `Pair`.
FirstSig a term	Corresponds to `First`.
SecondSig a term	Corresponds to `Second`.
UniverseSig a	Corresponds to `Universe`.

Instances

Instances details

Bifoldable (Term'Sig a) Source #
Instance details Defined in Language.LambdaPi.Impl.FreeFoilTH Methods bifold :: Monoid m => Term'Sig a m m -> m # bifoldMap :: Monoid m => (a0 -> m) -> (b -> m) -> Term'Sig a a0 b -> m # bifoldr :: (a0 -> c -> c) -> (b -> c -> c) -> c -> Term'Sig a a0 b -> c # bifoldl :: (c -> a0 -> c) -> (c -> b -> c) -> c -> Term'Sig a a0 b -> c #
Bifunctor (Term'Sig a) Source #
Instance details Defined in Language.LambdaPi.Impl.FreeFoilTH Methods bimap :: (a0 -> b) -> (c -> d) -> Term'Sig a a0 c -> Term'Sig a b d # first :: (a0 -> b) -> Term'Sig a a0 c -> Term'Sig a b c # second :: (b -> c) -> Term'Sig a a0 b -> Term'Sig a a0 c #
Bitraversable (Term'Sig a) Source #
Instance details Defined in Language.LambdaPi.Impl.FreeFoilTH Methods bitraverse :: Applicative f => (a0 -> f c) -> (b -> f d) -> Term'Sig a a0 b -> f (Term'Sig a c d) #
ZipMatch (Term'Sig a) Source #
Instance details Defined in Language.LambdaPi.Impl.FreeFoilTH Methods zipMatch :: Term'Sig a scope term -> Term'Sig a scope' term' -> Maybe (Term'Sig a (scope, scope') (term, term')) #
Foldable (Term'Sig a scope) Source #
Instance details Defined in Language.LambdaPi.Impl.FreeFoilTH Methods fold :: Monoid m => Term'Sig a scope m -> m # foldMap :: Monoid m => (a0 -> m) -> Term'Sig a scope a0 -> m # foldMap' :: Monoid m => (a0 -> m) -> Term'Sig a scope a0 -> m # foldr :: (a0 -> b -> b) -> b -> Term'Sig a scope a0 -> b # foldr' :: (a0 -> b -> b) -> b -> Term'Sig a scope a0 -> b # foldl :: (b -> a0 -> b) -> b -> Term'Sig a scope a0 -> b # foldl' :: (b -> a0 -> b) -> b -> Term'Sig a scope a0 -> b # foldr1 :: (a0 -> a0 -> a0) -> Term'Sig a scope a0 -> a0 # foldl1 :: (a0 -> a0 -> a0) -> Term'Sig a scope a0 -> a0 # toList :: Term'Sig a scope a0 -> [a0] # null :: Term'Sig a scope a0 -> Bool # length :: Term'Sig a scope a0 -> Int # elem :: Eq a0 => a0 -> Term'Sig a scope a0 -> Bool # maximum :: Ord a0 => Term'Sig a scope a0 -> a0 # minimum :: Ord a0 => Term'Sig a scope a0 -> a0 # sum :: Num a0 => Term'Sig a scope a0 -> a0 # product :: Num a0 => Term'Sig a scope a0 -> a0 #
IsString (AST (Term'Sig BNFC'Position) 'VoidS) Source #	Parse scope-safe terms via raw representation. `>>>` `fromString "λx.λy.λx.x" :: Term Foil.VoidS`λ x0 . λ x1 . λ x2 . x2
Instance details Defined in Language.LambdaPi.Impl.FreeFoilTH Methods fromString :: String -> AST (Term'Sig BNFC'Position) 'VoidS #
Traversable (Term'Sig a scope) Source #
Instance details Defined in Language.LambdaPi.Impl.FreeFoilTH Methods traverse :: Applicative f => (a0 -> f b) -> Term'Sig a scope a0 -> f (Term'Sig a scope b) # sequenceA :: Applicative f => Term'Sig a scope (f a0) -> f (Term'Sig a scope a0) # mapM :: Monad m => (a0 -> m b) -> Term'Sig a scope a0 -> m (Term'Sig a scope b) # sequence :: Monad m => Term'Sig a scope (m a0) -> m (Term'Sig a scope a0) #
Functor (Term'Sig a scope) Source #
Instance details Defined in Language.LambdaPi.Impl.FreeFoilTH Methods fmap :: (a0 -> b) -> Term'Sig a scope a0 -> Term'Sig a scope b # (<$) :: a0 -> Term'Sig a scope b -> Term'Sig a scope a0 #
Show (AST (Term'Sig a) 'VoidS) Source #	Pretty-print scope-safe terms via raw representation.
Instance details Defined in Language.LambdaPi.Impl.FreeFoilTH Methods showsPrec :: Int -> AST (Term'Sig a) 'VoidS -> ShowS # show :: AST (Term'Sig a) 'VoidS -> String # showList :: [AST (Term'Sig a) 'VoidS] -> ShowS #

Pattern synonyms

pattern Universe :: a -> AST (Term'Sig a) n Source #

Generated with mkPatternSynonyms. Pattern synonym for an AST node of type UniverseSig.

pattern Second :: a -> AST (Term'Sig a) n -> AST (Term'Sig a) n Source #

Generated with mkPatternSynonyms. Pattern synonym for an AST node of type SecondSig.

pattern First :: a -> AST (Term'Sig a) n -> AST (Term'Sig a) n Source #

Generated with mkPatternSynonyms. Pattern synonym for an AST node of type FirstSig.

pattern Pair :: a -> AST (Term'Sig a) n -> AST (Term'Sig a) n -> AST (Term'Sig a) n Source #

Generated with mkPatternSynonyms. Pattern synonym for an AST node of type PairSig.

pattern Product :: a -> AST (Term'Sig a) n -> AST (Term'Sig a) n -> AST (Term'Sig a) n Source #

Generated with mkPatternSynonyms. Pattern synonym for an AST node of type ProductSig.

pattern App :: a -> AST (Term'Sig a) n -> AST (Term'Sig a) n -> AST (Term'Sig a) n Source #

Generated with mkPatternSynonyms. Pattern synonym for an AST node of type AppSig.

pattern Lam :: () => a -> NameBinder n l1 -> AST (Term'Sig a) l1 -> AST (Term'Sig a) n Source #

Generated with mkPatternSynonyms. Pattern synonym for an AST node of type LamSig.

pattern Pi :: () => a -> AST (Term'Sig a) n -> NameBinder n l2 -> AST (Term'Sig a) l2 -> AST (Term'Sig a) n Source #

Generated with mkPatternSynonyms. Pattern synonym for an AST node of type PiSig.

Conversion helpers

convertToTerm'Sig :: Term' a -> Either VarIdent (Term'Sig a (Pattern' a, ScopedTerm' a) (Term' a)) Source #

Generated with mkConvertToFreeFoil. Perform one step of converting Term', peeling off one node of type Term'Sig.

getPattern'Binder :: Pattern' a -> Maybe VarIdent Source #

Generated with mkGetPatternBinder. Extract at most one binder from a pattern or crash.

getTerm'FromScopedTerm' :: ScopedTerm' a -> Term' a Source #

Generated with mkGetScopedTerm. Extract scoped term or crash.

convertFromTerm'Sig :: Term'Sig a (Pattern' a, ScopedTerm' a) (Term' a) -> Term' a Source #

Generated with mkConvertToFreeFoil. Perform one step of converting Term', peeling off one node of type Term'Sig.

User-defined code

type Term' a = AST (Term'Sig a) Source #

type Term = Term' BNFC'Position Source #

Conversion helpers

toTerm' :: forall (n :: S) a. Distinct n => Scope n -> Map VarIdent (Name n) -> Term' a -> AST (Term'Sig a) n Source #

Convert Term' into a scope-safe term. This is a special case of convertToAST.

toTerm'Closed :: Term' a -> AST (Term'Sig a) 'VoidS Source #

Convert Term' into a closed scope-safe term. This is a special case of toTerm'.

fromTerm' :: forall a (n :: S). AST (Term'Sig a) n -> Term' a Source #

Convert a scope-safe representation back into Term'. This is a special case of convertFromAST.

VarIdent names are generated based on the raw identifiers in the underlying foil representation.

This function does not recover location information for variables, patterns, or scoped terms.

Evaluation

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

Compute weak head normal form (WHNF) of a λΠ-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" :: Term 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

Type checking

λΠ-interpreter

interpretCommand :: Command -> IO () Source #

Interpret a λΠ command.

interpretProgram :: Program -> IO () Source #

Interpret a λΠ program.

defaultMain :: IO () Source #

A λΠ interpreter implemented via the free foil.