Safe Haskell	None
Language	Haskell2010

Language.LambdaPi.Impl.FreeFoilTH

Contents

Generated code
User-defined code
Orphan instances

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 $\alpha$-equivalence checks (see alphaEquiv and alphaEquivRefreshed) as well as $\alpha$-normalization (see refreshAST).
Conversion helpers (see convertToAST and convertFromAST).

The following is generated using Template Haskell:

Convenient pattern synonyms.
ZipMatch instances (enabling general $\alpha$-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 binder (Term'Sig a) n
pattern Second :: a -> AST binder (Term'Sig a) n -> AST binder (Term'Sig a) n
pattern First :: a -> AST binder (Term'Sig a) n -> AST binder (Term'Sig a) n
pattern Pair :: a -> AST binder (Term'Sig a) n -> AST binder (Term'Sig a) n -> AST binder (Term'Sig a) n
pattern Product :: a -> AST binder (Term'Sig a) n -> AST binder (Term'Sig a) n -> AST binder (Term'Sig a) n
pattern App :: a -> AST binder (Term'Sig a) n -> AST binder (Term'Sig a) n -> AST binder (Term'Sig a) n
pattern Lam :: () => a -> binder n l1 -> AST binder (Term'Sig a) l1 -> AST binder (Term'Sig a) n
pattern Pi :: () => a -> AST binder (Term'Sig a) n -> binder n l2 -> AST binder (Term'Sig a) l2 -> AST binder (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
data FoilPattern' a (n :: S) (l :: S) where
- FoilPatternWildcard :: forall a (n :: S). a -> FoilPattern' a n n
- FoilPatternVar :: forall a (n :: S) (l :: S). a -> NameBinder n l -> FoilPattern' a n l
- FoilPatternPair :: forall a (n :: S) (n2 :: S) (l :: S). a -> FoilPattern' a n n2 -> FoilPattern' a n2 l -> FoilPattern' a n l
toFoilPattern' :: forall (n :: S) a r. Distinct n => Scope n -> Map VarIdent (Name n) -> Pattern' a -> (forall (l :: S). DExt n l => FoilPattern' a n l -> Map VarIdent (Name l) -> r) -> r
fromFoilPattern' :: forall a (n :: S) (l :: S). (Int -> VarIdent) -> FoilPattern' a n l -> Pattern' a
type Term' a = AST (FoilPattern' a) (Term'Sig a)
type Term = Term' BNFC'Position
type FoilPattern = FoilPattern' BNFC'Position
toTerm' :: forall (n :: S) a. Distinct n => Scope n -> Map VarIdent (Name n) -> Term' a -> Term' a n
toTerm'Closed :: Term' a -> Term' a 'VoidS
fromTerm' :: forall a (n :: S). Term' a n -> Term' a
matchPattern :: forall (n :: S) (l :: S). FoilPattern n l -> Term n -> Substitution Term l n
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 #
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 #
IsString (AST FoilPattern (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 FoilPattern (Term'Sig BNFC'Position) 'VoidS #
Show (AST (FoilPattern' a) (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 (FoilPattern' a) (Term'Sig a) 'VoidS -> ShowS # show :: AST (FoilPattern' a) (Term'Sig a) 'VoidS -> String # showList :: [AST (FoilPattern' a) (Term'Sig a) 'VoidS] -> ShowS #

Pattern synonyms

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

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

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

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

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

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

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

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

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

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

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

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

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

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

pattern Pi :: () => a -> AST binder (Term'Sig a) n -> binder n l2 -> AST binder (Term'Sig a) l2 -> AST binder (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 mkConvertToSig. 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 mkConvertFromSig. Perform one step of converting Term', peeling off one node of type Term'Sig.

Scope-safe patterns

data FoilPattern' a (n :: S) (l :: S) where Source #

Generated with mkFoilPattern. A scope-safe version of Pattern'.

Constructors

FoilPatternWildcard :: forall a (n :: S). a -> FoilPattern' a n n	Corresponds to `PatternWildcard`.
FoilPatternVar :: forall a (n :: S) (l :: S). a -> NameBinder n l -> FoilPattern' a n l	Corresponds to `PatternVar`.
FoilPatternPair :: forall a (n :: S) (n2 :: S) (l :: S). a -> FoilPattern' a n n2 -> FoilPattern' a n2 l -> FoilPattern' a n l	Corresponds to `PatternPair`.

Instances

Instances details

CoSinkable (FoilPattern' a) Source #
Instance details Defined in Language.LambdaPi.Impl.FreeFoilTH Methods coSinkabilityProof :: forall (n :: S) (n' :: S) (l :: S) r. (Name n -> Name n') -> FoilPattern' a n l -> (forall (l' :: S). (Name l -> Name l') -> FoilPattern' a 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 -> FoilPattern' a n l -> (forall (o' :: S). DExt o o' => f n l o o' -> FoilPattern' a o o' -> r) -> r #
UnifiableInPattern a => UnifiablePattern (FoilPattern' a) Source #
Instance details Defined in Language.LambdaPi.Impl.FreeFoilTH Methods unifyPatterns :: forall (n :: S) (l :: S) (r :: S). Distinct n => FoilPattern' a n l -> FoilPattern' a n r -> UnifyNameBinders (FoilPattern' a) n l r #
IsString (AST FoilPattern (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 FoilPattern (Term'Sig BNFC'Position) 'VoidS #
Show (AST (FoilPattern' a) (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 (FoilPattern' a) (Term'Sig a) 'VoidS -> ShowS # show :: AST (FoilPattern' a) (Term'Sig a) 'VoidS -> String # showList :: [AST (FoilPattern' a) (Term'Sig a) 'VoidS] -> ShowS #

toFoilPattern' :: forall (n :: S) a r. Distinct n => Scope n -> Map VarIdent (Name n) -> Pattern' a -> (forall (l :: S). DExt n l => FoilPattern' a n l -> Map VarIdent (Name l) -> r) -> r Source #

Generated with mkToFoilPattern. Convert a raw pattern into a scope-safe pattern.

fromFoilPattern' :: forall a (n :: S) (l :: S). (Int -> VarIdent) -> FoilPattern' a n l -> Pattern' a Source #

Generated with mkFromFoilPattern. Convert a scope-safe pattern into a raw pattern.

User-defined code

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

Generic annotated scope-safe $\lambda\Pi$-terms with patterns.

type Term = Term' BNFC'Position Source #

Scode-safe $\lambda\Pi$-terms annotated with source code position.

type FoilPattern = FoilPattern' BNFC'Position Source #

Scope-safe patterns annotated with source code position.

Conversion helpers

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

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

toTerm'Closed :: Term' a -> Term' a 'VoidS Source #

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

fromTerm' :: forall a (n :: S). Term' 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

matchPattern :: forall (n :: S) (l :: S). FoilPattern n l -> Term n -> Substitution Term l n Source #

Match a pattern against an term.

whnf :: forall (n :: S). Distinct n => Scope n -> Term n -> Term 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" :: 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

$\lambda\Pi$-interpreter

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.

Orphan instances

UnifiableInPattern BNFC'Position Source #	Ignoring location information when unifying patterns.
Instance details Methods unifyInPattern :: BNFC'Position -> BNFC'Position -> Bool #

Documentation

Generated code

Signature

Instances

Pattern synonyms

Conversion helpers

Scope-safe patterns

Instances

User-defined code

Conversion helpers

Evaluation

\(\lambda\Pi\)-interpreter

Orphan instances