Control.Monad.Free.Foil

This module defines a variation of free scoped (relative) monads relying on the foil for the scope-safe efficient handling of the binders.

See description of the approach in «Free Foil: Generating Efficient and Scope-Safe Abstract Syntax».

Documentation

data ScopedAST (binder :: S -> S -> Type) (sig :: Type -> Type -> Type) (n :: S) where

Scoped term under a (single) name binder.

Constructors

ScopedAST :: forall (binder :: S -> S -> Type) (n :: S) (l :: S) (sig :: Type -> Type -> Type). binder n l -> AST binder sig l -> ScopedAST binder sig n

Instances

(forall (x :: S) (y :: S). NFData (binder x y), forall (l :: S). NFData (AST binder sig l)) => NFData (ScopedAST binder sig n)

Defined in Control.Monad.Free.Foil

Methods

rnf :: ScopedAST binder sig n -> ()

data AST (binder :: S -> S -> Type) (sig :: Type -> Type -> Type) (n :: S) where

A term, generated by a signature Bifunctor sig, with (free) variables in scope n.

Constructors

Var :: forall (n :: S) (binder :: S -> S -> Type) (sig :: Type -> Type -> Type). Name n -> AST binder sig n

A (free) variable in scope n.

Node :: forall (sig :: Type -> Type -> Type) (binder :: S -> S -> Type) (n :: S). sig (ScopedAST binder sig n) (AST binder sig n) -> AST binder sig n

A non-variable syntactic construction specified by the signature Bifunctor sig.

Instances

(Bifunctor sig, CoSinkable binder) => RelMonad Name (AST binder sig)

AST sig is a monad relative to Name.

Defined in Control.Monad.Free.Foil

Methods

rreturn :: forall (a :: S). Name a -> AST binder sig a

rbind :: forall (b :: S) (a :: S). Distinct b => Scope b -> AST binder sig a -> (Name a -> AST binder sig b) -> AST binder sig b

Show (Expr n)

Use ppExpr to show \(\lambda\)-terms.

Defined in Control.Monad.Free.Foil.Example

Methods

showsPrec :: Int -> Expr n -> ShowS

show :: Expr n -> String

showList :: [Expr n] -> ShowS

InjectName (AST binder sig)

Defined in Control.Monad.Free.Foil

Methods

injectName :: forall (n :: S). Name n -> AST binder sig n

(Bifunctor sig, CoSinkable binder) => Sinkable (AST binder sig)

Defined in Control.Monad.Free.Foil

Methods

sinkabilityProof :: forall (n :: S) (l :: S). (Name n -> Name l) -> AST binder sig n -> AST binder sig l

Generic (AST binder sig n)

Defined in Control.Monad.Free.Foil

Associated Types

type Rep (AST binder sig n)

Defined in Control.Monad.Free.Foil

type Rep (AST binder sig n) = D1 ('MetaData "AST" "Control.Monad.Free.Foil" "free-foil-0.1.0-9dB5dihS08J3SaKaLaeFbG" 'False) (C1 ('MetaCons "Var" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Name n))) :+: C1 ('MetaCons "Node" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (sig (ScopedAST binder sig n) (AST binder sig n)))))

Methods

from :: AST binder sig n -> Rep (AST binder sig n) x

to :: Rep (AST binder sig n) x -> AST binder sig n

(forall (x :: S) (y :: S). NFData (binder x y), forall scope term. (NFData scope, NFData term) => NFData (sig scope term)) => NFData (AST binder sig n)

Defined in Control.Monad.Free.Foil

Methods

rnf :: AST binder sig n -> ()

type Rep (AST binder sig n)

Defined in Control.Monad.Free.Foil

type Rep (AST binder sig n) = D1 ('MetaData "AST" "Control.Monad.Free.Foil" "free-foil-0.1.0-9dB5dihS08J3SaKaLaeFbG" 'False) (C1 ('MetaCons "Var" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Name n))) :+: C1 ('MetaCons "Node" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (sig (ScopedAST binder sig n) (AST binder sig n)))))

Substitution

substitute :: forall (sig :: Type -> Type -> Type) (o :: S) (binder :: S -> S -> Type) (i :: S). (Bifunctor sig, Distinct o, CoSinkable binder) => Scope o -> Substitution (AST binder sig) i o -> AST binder sig i -> AST binder sig o

Substitution for free (scoped monads).

substituteRefreshed :: forall (sig :: Type -> Type -> Type) (o :: S) (binder :: S -> S -> Type) (i :: S). (Bifunctor sig, Distinct o, CoSinkable binder) => Scope o -> Substitution (AST binder sig) i o -> AST binder sig i -> AST binder sig o

Substitution for free (scoped monads).

This is a version of substitute that forces refreshing of all name binders, resulting in a term with normalized binders:

substituteRefreshed scope subst = refreshAST scope . subtitute scope subst

In general, substitute is more efficient since it does not always refresh binders.

\(\alpha\)-equivalence

refreshAST :: forall (sig :: Type -> Type -> Type) (n :: S) (binder :: S -> S -> Type). (Bifunctor sig, Distinct n, CoSinkable binder) => Scope n -> AST binder sig n -> AST binder sig n

Refresh (force) all binders in a term, minimizing the used indices.

refreshScopedAST :: forall (sig :: Type -> Type -> Type) (n :: S) (binder :: S -> S -> Type). (Bifunctor sig, Distinct n, CoSinkable binder) => Scope n -> ScopedAST binder sig n -> ScopedAST binder sig n

Similar to refreshAST, but for scoped terms.

alphaEquivRefreshed :: forall (sig :: Type -> Type -> Type) (n :: S) (binder :: S -> S -> Type). (Bifunctor sig, Bifoldable sig, ZipMatch sig, Distinct n, UnifiablePattern binder) => Scope n -> AST binder sig n -> AST binder sig n -> Bool

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

Compared to alphaEquiv, this function may perform some unnecessary changes of bound variables when the binders are the same on both sides.

alphaEquiv :: forall (sig :: Type -> Type -> Type) (n :: S) (binder :: S -> S -> Type). (Bifunctor sig, Bifoldable sig, ZipMatch sig, Distinct n, UnifiablePattern binder) => Scope n -> AST binder sig n -> AST binder sig n -> Bool

\(\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.

alphaEquivScoped :: forall (sig :: Type -> Type -> Type) (n :: S) (binder :: S -> S -> Type). (Bifunctor sig, Bifoldable sig, ZipMatch sig, Distinct n, UnifiablePattern binder) => Scope n -> ScopedAST binder sig n -> ScopedAST binder sig n -> Bool

Same as alphaEquiv but for scoped terms.

Unsafe equality checks

unsafeEqAST :: forall (sig :: Type -> Type -> Type) (binder :: S -> S -> Type) (n :: S) (l :: S). (Bifoldable sig, ZipMatch sig, UnifiablePattern binder, Distinct n, Distinct l) => AST binder sig n -> AST binder sig l -> Bool

Unsafe equality check for two terms. This check ignores the possibility that two terms might have different scope extensions under binders (which might happen due to substitution under a binder in absence of name conflicts).

unsafeEqScopedAST :: forall (sig :: Type -> Type -> Type) (binder :: S -> S -> Type) (n :: S) (l :: S). (Bifoldable sig, ZipMatch sig, UnifiablePattern binder, Distinct n, Distinct l) => ScopedAST binder sig n -> ScopedAST binder sig l -> Bool

A version of unsafeEqAST for scoped terms.

Syntactic matching (unification)

class ZipMatch (sig :: Type -> Type -> Type) where

Perform one-level matching for the two (non-variable) terms.

Methods

zipMatch

Arguments

:: sig scope term

Left non-variable term.

-> sig scope' term'

Right non-variable term.

-> Maybe (sig (scope, scope') (term, term'))

Instances

(ZipMatch f, ZipMatch g) => ZipMatch (Sum f g)

Defined in Control.Monad.Free.Foil

Methods

zipMatch :: Sum f g scope term -> Sum f g scope' term' -> Maybe (Sum f g (scope, scope') (term, term'))

Converting to and from free foil

Convert to free foil

convertToAST

Arguments

:: forall (n :: S) sig rawIdent binder rawTerm rawPattern rawScopedTerm. (Distinct n, Bifunctor sig, Ord rawIdent, CoSinkable binder)

=> (rawTerm -> Either rawIdent (sig (rawPattern, rawScopedTerm) rawTerm))

Unpeel one syntax node (or a variable) from a raw term.

-> (forall (x :: S) z. Distinct x => Scope x -> Map rawIdent (Name x) -> rawPattern -> (forall (y :: S). DExt x y => binder x y -> Map rawIdent (Name y) -> z) -> z)

Convert raw pattern into a scope-safe pattern.

-> (rawScopedTerm -> rawTerm)

Extract a term from a scoped term (or crash).

-> Scope n

Resulting scope of the constructed term.

-> Map rawIdent (Name n)

Known names of free variables in scope n.

-> rawTerm

Raw term.

-> AST binder sig n

Convert a raw term into a scope-safe term.

convertToScopedAST

Arguments

:: forall (n :: S) sig rawIdent binder rawTerm rawPattern rawScopedTerm. (Distinct n, Bifunctor sig, Ord rawIdent, CoSinkable binder)

=> (rawTerm -> Either rawIdent (sig (rawPattern, rawScopedTerm) rawTerm))

Unpeel one syntax node (or a variable) from a raw term.

-> (forall (x :: S) z. Distinct x => Scope x -> Map rawIdent (Name x) -> rawPattern -> (forall (y :: S). DExt x y => binder x y -> Map rawIdent (Name y) -> z) -> z)

Convert raw pattern into a scope-safe pattern.

-> (rawScopedTerm -> rawTerm)

Extract a term from a scoped term (or crash).

-> Scope n

Resulting scope of the constructed term.

-> Map rawIdent (Name n)

Known names of free variables in scope n.

-> (rawPattern, rawScopedTerm)

A pair of a pattern and a corresponding scoped term.

-> ScopedAST binder sig n

Same as convertToAST but for scoped terms.

Convert from free foil

convertFromAST

Arguments

:: forall sig rawPattern rawScopedTerm rawTerm rawIdent binder (n :: S). Bifunctor sig

=> (sig (rawPattern, rawScopedTerm) rawTerm -> rawTerm)

Peel back one layer of syntax.

-> (rawIdent -> rawTerm)

Convert identifier into a raw variable term.

-> (forall (x :: S) (y :: S). (Int -> rawIdent) -> binder x y -> rawPattern)

Convert scope-safe pattern into a raw pattern.

-> (rawTerm -> rawScopedTerm)

Wrap raw term into a scoped term.

-> (Int -> rawIdent)

Convert underlying integer identifier of a bound variable into a raw identifier.

-> AST binder sig n

Scope-safe term.

-> rawTerm

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

convertFromScopedAST

Arguments

:: forall sig rawPattern rawScopedTerm rawTerm rawIdent binder (n :: S). Bifunctor sig

=> (sig (rawPattern, rawScopedTerm) rawTerm -> rawTerm)

Peel back one layer of syntax.

-> (rawIdent -> rawTerm)

Convert identifier into a raw variable term.

-> (forall (x :: S) (y :: S). (Int -> rawIdent) -> binder x y -> rawPattern)

Convert scope-safe pattern into a raw pattern.

-> (rawTerm -> rawScopedTerm)

Wrap raw term into a scoped term.

-> (Int -> rawIdent)

Convert underlying integer identifier of a bound variable into a raw identifier.

-> ScopedAST binder sig n

Scope-safe scoped term.

-> (rawPattern, rawScopedTerm)

Same as convertFromAST but for scoped terms.