free-foil-0.2.0: Efficient Type-Safe Capture-Avoiding Substitution for Free (Scoped Monads)
Safe HaskellNone
LanguageHaskell2010

Control.Monad.Foil

Description

Main definitions of the foil that can be reused for specific implementations.

The original description of this approach is described in the IFL 2022 paper by Maclaurin, Radul, and Paszke «The Foil: Capture-Avoiding Substitution With No Sharp Edges». This module also introduces CoSinkable class, generalizing handling of patterns, as described in «Free Foil: Generating Efficient and Scope-Safe Abstract Syntax».

Since the representation of scopes and substitutions is either IntMap or IntSet, many of the operations have a worst-case complexity of \(O(\min(n,W))\). This means that the operation can become linear in the size of the scope \(n\) with a maximum of \(W\) — the number of bits in an Int (32 or 64).

Synopsis

Safe scopes, names, and binders

data S Source #

S is a data kind of scope indices.

Constructors

VoidS

VoidS is the only explicit scope available to the users, representing an empty scope. All other scopes are represented with type variables, bound in rank-2 polymophic functions like withFreshBinder.

Instances

Instances details
(SinkableK f, ExtractRenamingK i, ExtractRenamingK j) => GSinkableK (Field ((('Kon f :: Atom k (S -> S -> Type)) ':@: 'Var i) ':@: 'Var j) :: LoT k -> Type) Source # 
Instance details

Defined in Control.Monad.Foil.Internal

Methods

gsinkabilityProofK :: forall (as :: LoT k) (bs :: LoT k) r. RenamingsK as bs -> Field ((('Kon f :: Atom k (S -> S -> Type)) ':@: 'Var i) ':@: 'Var j) as -> (forall (cs :: LoT k). RenamingsK as cs -> Field ((('Kon f :: Atom k (S -> S -> Type)) ':@: 'Var i) ':@: 'Var j) cs -> r) -> r Source #

(SinkableK f, ExtractRenamingK i) => GSinkableK (Field (('Kon f :: Atom k (S -> Type)) ':@: 'Var i) :: LoT k -> Type) Source # 
Instance details

Defined in Control.Monad.Foil.Internal

Methods

gsinkabilityProofK :: forall (as :: LoT k) (bs :: LoT k) r. RenamingsK as bs -> Field (('Kon f :: Atom k (S -> Type)) ':@: 'Var i) as -> (forall (cs :: LoT k). RenamingsK as cs -> Field (('Kon f :: Atom k (S -> Type)) ':@: 'Var i) cs -> r) -> r Source #

GSinkableK f => GSinkableK (Exists S f :: LoT k -> Type) Source # 
Instance details

Defined in Control.Monad.Foil.Internal

Methods

gsinkabilityProofK :: forall (as :: LoT k) (bs :: LoT k) r. RenamingsK as bs -> Exists S f as -> (forall (cs :: LoT k). RenamingsK as cs -> Exists S f cs -> r) -> r Source #

HasNameBinders f => GHasNameBinders (Field ((('Kon f :: Atom d (S -> S -> Type)) ':@: 'Var i) ':@: 'Var j) :: LoT d -> Type) Source # 
Instance details

Defined in Control.Monad.Foil.Internal

Methods

ggetNameBindersRaw :: forall (as :: LoT d). Field ((('Kon f :: Atom d (S -> S -> Type)) ':@: 'Var i) ':@: 'Var j) as -> [RawName] Source #

greallyUnsafeSetNameBindersRaw :: forall (as :: LoT d) (bs :: LoT d). Field ((('Kon f :: Atom d (S -> S -> Type)) ':@: 'Var i) ':@: 'Var j) as -> [RawName] -> (Field ((('Kon f :: Atom d (S -> S -> Type)) ':@: 'Var i) ':@: 'Var j) bs, [RawName]) Source #

SinkableK NameBinder Source # 
Instance details

Defined in Control.Monad.Foil.Internal

Methods

sinkabilityProofK :: forall (as :: LoT (S -> S -> Type)) (bs :: LoT (S -> S -> Type)) r. RenamingsK as bs -> (NameBinder :@@: as) -> (forall (cs :: LoT (S -> S -> Type)). RenamingsK as cs -> (NameBinder :@@: cs) -> r) -> r Source #

SinkableK NameBinderList Source # 
Instance details

Defined in Control.Monad.Foil.Internal

Methods

sinkabilityProofK :: forall (as :: LoT (S -> S -> Type)) (bs :: LoT (S -> S -> Type)) r. RenamingsK as bs -> (NameBinderList :@@: as) -> (forall (cs :: LoT (S -> S -> Type)). RenamingsK as cs -> (NameBinderList :@@: cs) -> r) -> r Source #

SinkableK NameBinders Source # 
Instance details

Defined in Control.Monad.Foil.Internal

Methods

sinkabilityProofK :: forall (as :: LoT (S -> S -> Type)) (bs :: LoT (S -> S -> Type)) r. RenamingsK as bs -> (NameBinders :@@: as) -> (forall (cs :: LoT (S -> S -> Type)). RenamingsK as cs -> (NameBinders :@@: cs) -> r) -> r Source #

SinkableK U2 Source # 
Instance details

Defined in Control.Monad.Foil.Internal

Methods

sinkabilityProofK :: forall (as :: LoT (S -> S -> Type)) (bs :: LoT (S -> S -> Type)) r. RenamingsK as bs -> (U2 :@@: as) -> (forall (cs :: LoT (S -> S -> Type)). RenamingsK as cs -> (U2 :@@: cs) -> r) -> r Source #

SinkableK V2 Source # 
Instance details

Defined in Control.Monad.Foil.Internal

Methods

sinkabilityProofK :: forall (as :: LoT (S -> S -> Type)) (bs :: LoT (S -> S -> Type)) r. RenamingsK as bs -> (V2 :@@: as) -> (forall (cs :: LoT (S -> S -> Type)). RenamingsK as cs -> (V2 :@@: cs) -> r) -> r Source #

GenericK NameBinderList Source # 
Instance details

Defined in Control.Monad.Foil.Internal

Associated Types

type RepK NameBinderList 
Instance details

Defined in Control.Monad.Foil.Internal

type RepK NameBinderList = (((Var0 :: Atom (S -> S -> Type) S) :~~: (Var1 :: Atom (S -> S -> Type) S)) :=>: (U1 :: LoT (S -> S -> Type) -> Type)) :+: Exists S (Field ((NameBinder :$: (Var1 :: Atom (S -> S -> S -> Type) S)) ':@: (Var0 :: Atom (S -> S -> S -> Type) S)) :*: Field ((NameBinderList :$: (Var0 :: Atom (S -> S -> S -> Type) S)) ':@: (Var2 :: Atom (S -> S -> S -> Type) S)))

Methods

fromK :: forall (x :: LoT (S -> S -> Type)). (NameBinderList :@@: x) -> RepK NameBinderList x #

toK :: forall (x :: LoT (S -> S -> Type)). RepK NameBinderList x -> NameBinderList :@@: x #

GenericK U2 Source # 
Instance details

Defined in Control.Monad.Foil.Internal

Associated Types

type RepK U2 
Instance details

Defined in Control.Monad.Foil.Internal

type RepK U2 = ((Var0 :: Atom (S -> S -> Type) S) :~~: (Var1 :: Atom (S -> S -> Type) S)) :=>: (U1 :: LoT (S -> S -> Type) -> Type)

Methods

fromK :: forall (x :: LoT (S -> S -> Type)). (U2 :@@: x) -> RepK U2 x #

toK :: forall (x :: LoT (S -> S -> Type)). RepK U2 x -> U2 :@@: x #

GenericK V2 Source # 
Instance details

Defined in Control.Monad.Foil.Internal

Associated Types

type RepK V2 
Instance details

Defined in Control.Monad.Foil.Internal

type RepK V2 = V1 :: LoT (S -> S -> Type) -> Type

Methods

fromK :: forall (x :: LoT (S -> S -> Type)). (V2 :@@: x) -> RepK V2 x #

toK :: forall (x :: LoT (S -> S -> Type)). RepK V2 x -> V2 :@@: x #

ExtractRenamingK ('VZ :: TyVar (S -> xs) S) Source # 
Instance details

Defined in Control.Monad.Foil.Internal

Methods

extractRenamingK :: forall (as :: LoT (S -> xs)) (bs :: LoT (S -> xs)). RenamingsK as bs -> Name (Interpret ('Var ('VZ :: TyVar (S -> xs) S)) as) -> Name (Interpret ('Var ('VZ :: TyVar (S -> xs) S)) bs) Source #

putBackRenamingK :: forall (c :: S) (as :: LoT (S -> xs)) (bs :: LoT (S -> xs)). (Name (Interpret ('Var ('VZ :: TyVar (S -> xs) S)) as) -> Name c) -> RenamingsK as bs -> RenamingsK as (PutBackLoT ('VZ :: TyVar (S -> xs) S) c bs) Source #

SinkableK (f a) => GSinkableK (Field ((('Kon f :: Atom (S -> xs) (k1 -> S -> Type)) ':@: ('Kon a :: Atom (S -> xs) k1)) ':@: (Var0 :: Atom (S -> xs) S)) :: LoT (S -> xs) -> Type) Source # 
Instance details

Defined in Control.Monad.Foil.Internal

Methods

gsinkabilityProofK :: forall (as :: LoT (S -> xs)) (bs :: LoT (S -> xs)) r. RenamingsK as bs -> Field ((('Kon f :: Atom (S -> xs) (k1 -> S -> Type)) ':@: ('Kon a :: Atom (S -> xs) k1)) ':@: (Var0 :: Atom (S -> xs) S)) as -> (forall (cs :: LoT (S -> xs)). RenamingsK as cs -> Field ((('Kon f :: Atom (S -> xs) (k1 -> S -> Type)) ':@: ('Kon a :: Atom (S -> xs) k1)) ':@: (Var0 :: Atom (S -> xs) S)) cs -> r) -> r Source #

SinkableK (f a b) => GSinkableK (Field (((('Kon f :: Atom (S -> xs) (k2 -> k3 -> S -> Type)) ':@: ('Kon a :: Atom (S -> xs) k2)) ':@: ('Kon b :: Atom (S -> xs) k3)) ':@: (Var0 :: Atom (S -> xs) S)) :: LoT (S -> xs) -> Type) Source # 
Instance details

Defined in Control.Monad.Foil.Internal

Methods

gsinkabilityProofK :: forall (as :: LoT (S -> xs)) (bs :: LoT (S -> xs)) r. RenamingsK as bs -> Field (((('Kon f :: Atom (S -> xs) (k2 -> k3 -> S -> Type)) ':@: ('Kon a :: Atom (S -> xs) k2)) ':@: ('Kon b :: Atom (S -> xs) k3)) ':@: (Var0 :: Atom (S -> xs) S)) as -> (forall (cs :: LoT (S -> xs)). RenamingsK as cs -> Field (((('Kon f :: Atom (S -> xs) (k2 -> k3 -> S -> Type)) ':@: ('Kon a :: Atom (S -> xs) k2)) ':@: ('Kon b :: Atom (S -> xs) k3)) ':@: (Var0 :: Atom (S -> xs) S)) cs -> r) -> r Source #

GenericK (AST binder sig :: S -> Type) Source # 
Instance details

Defined in Control.Monad.Free.Foil

Associated Types

type RepK (AST binder sig :: S -> Type) 
Instance details

Defined in Control.Monad.Free.Foil

type RepK (AST binder sig :: S -> Type) = Field (Name :$: (Var0 :: Atom (S -> Type) S)) :+: Field ((sig :$: (((('Kon ScopedAST :: Atom (S -> Type) ((S -> S -> Type) -> (Type -> Type -> Type) -> S -> Type)) ':@: ('Kon binder :: Atom (S -> Type) (S -> S -> Type))) ':@: ('Kon sig :: Atom (S -> Type) (Type -> Type -> Type))) ':@: (Var0 :: Atom (S -> Type) S))) ':@: (((('Kon AST :: Atom (S -> Type) ((S -> S -> Type) -> (Type -> Type -> Type) -> S -> Type)) ':@: ('Kon binder :: Atom (S -> Type) (S -> S -> Type))) ':@: ('Kon sig :: Atom (S -> Type) (Type -> Type -> Type))) ':@: (Var0 :: Atom (S -> Type) S)))

Methods

fromK :: forall (x :: LoT (S -> Type)). (AST binder sig :@@: x) -> RepK (AST binder sig) x #

toK :: forall (x :: LoT (S -> Type)). RepK (AST binder sig) x -> AST binder sig :@@: x #

GenericK (ScopedAST binder sig :: S -> Type) Source # 
Instance details

Defined in Control.Monad.Free.Foil

Associated Types

type RepK (ScopedAST binder sig :: S -> Type) 
Instance details

Defined in Control.Monad.Free.Foil

type RepK (ScopedAST binder sig :: S -> Type) = Exists S (Field ((('Kon binder :: Atom (S -> S -> Type) (S -> S -> Type)) ':@: (Var1 :: Atom (S -> S -> Type) S)) ':@: (Var0 :: Atom (S -> S -> Type) S)) :*: Field (((('Kon AST :: Atom (S -> S -> Type) ((S -> S -> Type) -> (Type -> Type -> Type) -> S -> Type)) ':@: ('Kon binder :: Atom (S -> S -> Type) (S -> S -> Type))) ':@: ('Kon sig :: Atom (S -> S -> Type) (Type -> Type -> Type))) ':@: (Var0 :: Atom (S -> S -> Type) S)))

Methods

fromK :: forall (x :: LoT (S -> Type)). (ScopedAST binder sig :@@: x) -> RepK (ScopedAST binder sig) x #

toK :: forall (x :: LoT (S -> Type)). RepK (ScopedAST binder sig) x -> ScopedAST binder sig :@@: x #

ExtractRenamingK x2 => ExtractRenamingK ('VS x2 :: TyVar (x1 -> xs) S) Source # 
Instance details

Defined in Control.Monad.Foil.Internal

Methods

extractRenamingK :: forall (as :: LoT (x1 -> xs)) (bs :: LoT (x1 -> xs)). RenamingsK as bs -> Name (Interpret ('Var ('VS x2 :: TyVar (x1 -> xs) S)) as) -> Name (Interpret ('Var ('VS x2 :: TyVar (x1 -> xs) S)) bs) Source #

putBackRenamingK :: forall (c :: S) (as :: LoT (x1 -> xs)) (bs :: LoT (x1 -> xs)). (Name (Interpret ('Var ('VS x2 :: TyVar (x1 -> xs) S)) as) -> Name c) -> RenamingsK as bs -> RenamingsK as (PutBackLoT ('VS x2 :: TyVar (x1 -> xs) S) c bs) Source #

type RepK NameBinderList Source # 
Instance details

Defined in Control.Monad.Foil.Internal

type RepK NameBinderList = (((Var0 :: Atom (S -> S -> Type) S) :~~: (Var1 :: Atom (S -> S -> Type) S)) :=>: (U1 :: LoT (S -> S -> Type) -> Type)) :+: Exists S (Field ((NameBinder :$: (Var1 :: Atom (S -> S -> S -> Type) S)) ':@: (Var0 :: Atom (S -> S -> S -> Type) S)) :*: Field ((NameBinderList :$: (Var0 :: Atom (S -> S -> S -> Type) S)) ':@: (Var2 :: Atom (S -> S -> S -> Type) S)))
type RepK U2 Source # 
Instance details

Defined in Control.Monad.Foil.Internal

type RepK U2 = ((Var0 :: Atom (S -> S -> Type) S) :~~: (Var1 :: Atom (S -> S -> Type) S)) :=>: (U1 :: LoT (S -> S -> Type) -> Type)
type RepK V2 Source # 
Instance details

Defined in Control.Monad.Foil.Internal

type RepK V2 = V1 :: LoT (S -> S -> Type) -> Type
type RepK (AST binder sig :: S -> Type) Source # 
Instance details

Defined in Control.Monad.Free.Foil

type RepK (AST binder sig :: S -> Type) = Field (Name :$: (Var0 :: Atom (S -> Type) S)) :+: Field ((sig :$: (((('Kon ScopedAST :: Atom (S -> Type) ((S -> S -> Type) -> (Type -> Type -> Type) -> S -> Type)) ':@: ('Kon binder :: Atom (S -> Type) (S -> S -> Type))) ':@: ('Kon sig :: Atom (S -> Type) (Type -> Type -> Type))) ':@: (Var0 :: Atom (S -> Type) S))) ':@: (((('Kon AST :: Atom (S -> Type) ((S -> S -> Type) -> (Type -> Type -> Type) -> S -> Type)) ':@: ('Kon binder :: Atom (S -> Type) (S -> S -> Type))) ':@: ('Kon sig :: Atom (S -> Type) (Type -> Type -> Type))) ':@: (Var0 :: Atom (S -> Type) S)))
type RepK (ScopedAST binder sig :: S -> Type) Source # 
Instance details

Defined in Control.Monad.Free.Foil

type RepK (ScopedAST binder sig :: S -> Type) = Exists S (Field ((('Kon binder :: Atom (S -> S -> Type) (S -> S -> Type)) ':@: (Var1 :: Atom (S -> S -> Type) S)) ':@: (Var0 :: Atom (S -> S -> Type) S)) :*: Field (((('Kon AST :: Atom (S -> S -> Type) ((S -> S -> Type) -> (Type -> Type -> Type) -> S -> Type)) ':@: ('Kon binder :: Atom (S -> S -> Type) (S -> S -> Type))) ':@: ('Kon sig :: Atom (S -> S -> Type) (Type -> Type -> Type))) ':@: (Var0 :: Atom (S -> S -> Type) S)))

data Scope (n :: S) Source #

A safe scope, indexed by a type-level scope index n.

Instances

Instances details
NFData (Scope n) Source # 
Instance details

Defined in Control.Monad.Foil.Internal

Methods

rnf :: Scope n -> () #

data Name (n :: S) Source #

A name in a safe scope, indexed by a type-level scope index n.

Instances

Instances details
Sinkable Name Source #

Sinking a Name is as simple as applying the renaming.

Instance details

Defined in Control.Monad.Foil.Internal

Methods

sinkabilityProof :: forall (n :: S) (l :: S). (Name n -> Name l) -> Name n -> Name l Source #

SinkableK Name Source # 
Instance details

Defined in Control.Monad.Foil.Internal

Methods

sinkabilityProofK :: forall (as :: LoT (S -> Type)) (bs :: LoT (S -> Type)) r. RenamingsK as bs -> (Name :@@: as) -> (forall (cs :: LoT (S -> Type)). RenamingsK as cs -> (Name :@@: cs) -> r) -> r Source #

RelMonad Name Expr Source #

Expr is a monad relative to Name.

Instance details

Defined in Control.Monad.Foil.Example

Methods

rreturn :: forall (a :: S). Name a -> Expr a Source #

rbind :: forall (b :: S) (a :: S). Distinct b => Scope b -> Expr a -> (Name a -> Expr b) -> Expr b Source #

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

AST sig is a monad relative to Name.

Instance details

Defined in Control.Monad.Free.Foil

Methods

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

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

Show (Name n) Source # 
Instance details

Defined in Control.Monad.Foil.Internal

Methods

showsPrec :: Int -> Name n -> ShowS #

show :: Name n -> String #

showList :: [Name n] -> ShowS #

NFData (Name n) Source # 
Instance details

Defined in Control.Monad.Foil.Internal

Methods

rnf :: Name n -> () #

Eq (Name n) Source # 
Instance details

Defined in Control.Monad.Foil.Internal

Methods

(==) :: Name n -> Name n -> Bool #

(/=) :: Name n -> Name n -> Bool #

Ord (Name n) Source # 
Instance details

Defined in Control.Monad.Foil.Internal

Methods

compare :: Name n -> Name n -> Ordering #

(<) :: Name n -> Name n -> Bool #

(<=) :: Name n -> Name n -> Bool #

(>) :: Name n -> Name n -> Bool #

(>=) :: Name n -> Name n -> Bool #

max :: Name n -> Name n -> Name n #

min :: Name n -> Name n -> Name n #

data NameBinder (n :: S) (l :: S) Source #

A name binder is a name that extends scope n to a (larger) scope l.

Instances

Instances details
CoSinkable NameBinder Source # 
Instance details

Defined in Control.Monad.Foil.Internal

Methods

coSinkabilityProof :: forall (n :: S) (n' :: S) (l :: S) r. (Name n -> Name n') -> NameBinder n l -> (forall (l' :: S). (Name l -> Name l') -> NameBinder n' l' -> r) -> r Source #

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 -> NameBinder n l -> (forall (o' :: S). DExt o o' => f n l o o' -> NameBinder o o' -> r) -> r Source #

HasNameBinders NameBinder Source # 
Instance details

Defined in Control.Monad.Foil.Internal

Methods

getNameBinders :: forall (n :: S) (l :: S). NameBinder n l -> NameBinders n l Source #

unsafeSetNameBinders :: forall (n :: S) (l :: S) (l' :: S). NameBinder n l -> NameBinders n l' -> NameBinder n l' Source #

getNameBindersRaw :: forall (n :: S) (l :: S). NameBinder n l -> [RawName] Source #

reallyUnsafeSetNameBindersRaw :: forall (n :: S) (l :: S) (l' :: S). NameBinder n l -> [RawName] -> (NameBinder n l', [RawName]) Source #

UnifiablePattern NameBinder Source # 
Instance details

Defined in Control.Monad.Foil.Internal

Methods

unifyPatterns :: forall (n :: S) (l :: S) (r :: S). Distinct n => NameBinder n l -> NameBinder n r -> UnifyNameBinders NameBinder n l r Source #

Show (Expr n) Source #

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

Instance details

Defined in Control.Monad.Free.Foil.Example

Methods

showsPrec :: Int -> Expr n -> ShowS #

show :: Expr n -> String #

showList :: [Expr n] -> ShowS #

Show (NameBinder n l) Source # 
Instance details

Defined in Control.Monad.Foil.Internal

Methods

showsPrec :: Int -> NameBinder n l -> ShowS #

show :: NameBinder n l -> String #

showList :: [NameBinder n l] -> ShowS #

NFData (NameBinder n l) Source # 
Instance details

Defined in Control.Monad.Foil.Internal

Methods

rnf :: NameBinder n l -> () #

Eq (NameBinder n l) Source # 
Instance details

Defined in Control.Monad.Foil.Internal

Methods

(==) :: NameBinder n l -> NameBinder n l -> Bool #

(/=) :: NameBinder n l -> NameBinder n l -> Bool #

Ord (NameBinder n l) Source # 
Instance details

Defined in Control.Monad.Foil.Internal

Methods

compare :: NameBinder n l -> NameBinder n l -> Ordering #

(<) :: NameBinder n l -> NameBinder n l -> Bool #

(<=) :: NameBinder n l -> NameBinder n l -> Bool #

(>) :: NameBinder n l -> NameBinder n l -> Bool #

(>=) :: NameBinder n l -> NameBinder n l -> Bool #

max :: NameBinder n l -> NameBinder n l -> NameBinder n l #

min :: NameBinder n l -> NameBinder n l -> NameBinder n l #

SinkableK NameBinder Source # 
Instance details

Defined in Control.Monad.Foil.Internal

Methods

sinkabilityProofK :: forall (as :: LoT (S -> S -> Type)) (bs :: LoT (S -> S -> Type)) r. RenamingsK as bs -> (NameBinder :@@: as) -> (forall (cs :: LoT (S -> S -> Type)). RenamingsK as cs -> (NameBinder :@@: cs) -> r) -> r Source #

emptyScope :: Scope 'VoidS Source #

An empty scope (without any names).

extendScope :: forall (n :: S) (l :: S). NameBinder n l -> Scope n -> Scope l Source #

\(O(\min(n,W))\). Extend a scope with one name (safely). Note that as long as the foil is used as intended, the name binder is guaranteed to introduce a name that does not appear in the initial scope.

extendScopePattern :: forall (n :: S) pattern (l :: S). (Distinct n, CoSinkable pattern) => pattern n l -> Scope n -> Scope l Source #

Extend scope with variables inside a pattern. This is a more flexible version of extendScope.

member :: forall (l :: S) (n :: S). Name l -> Scope n -> Bool Source #

A runtime check for potential name capture.

nameOf :: forall (n :: S) (l :: S). NameBinder n l -> Name l Source #

Extract name from a name binder.

namesOfPattern :: forall pattern (n :: S) (l :: S). (Distinct n, CoSinkable pattern) => pattern n l -> [Name l] Source #

Extract names from a pattern. This is a more flexible version of namesOf.

nameId :: forall (l :: S). Name l -> Id Source #

Convert Name into an identifier. This may be useful for printing and debugging.

withFreshBinder :: forall (n :: S) r. Scope n -> (forall (l :: S). NameBinder n l -> r) -> r Source #

Allocate a fresh binder for a given scope.

withFresh :: forall (n :: S) r. Distinct n => Scope n -> (forall (l :: S). DExt n l => NameBinder n l -> r) -> r Source #

Safely produce a fresh name binder with respect to a given scope.

withFreshPattern Source #

Arguments

:: forall (o :: S) pattern (e :: S -> Type) (n :: S) (l :: S) r. (Distinct o, CoSinkable pattern, Sinkable e, InjectName e) 
=> Scope o

Ambient scope.

-> pattern n l

Pattern to refresh (if it clashes with the ambient scope).

-> (forall (o' :: S). DExt o o' => (Substitution e n o -> Substitution e l o') -> pattern o o' -> r)

Continuation, accepting the refreshed pattern.

-> r 

Rename a given pattern into a fresh version of it to extend a given scope.

This is similar to withRefreshPattern, except here renaming always takes place.

withRefreshed Source #

Arguments

:: forall (o :: S) (i :: S) r. Distinct o 
=> Scope o

Ambient scope.

-> Name i

Name to refresh (if it clashes with the ambient scope).

-> (forall (o' :: S). DExt o o' => NameBinder o o' -> r)

Continuation, accepting the refreshed name.

-> r 

Safely rename (if necessary) a given name to extend a given scope. This is similar to withFresh, except if the name does not clash with the scope, it can be used immediately, without renaming.

withRefreshedPattern Source #

Arguments

:: forall (o :: S) pattern (e :: S -> Type) (n :: S) (l :: S) r. (Distinct o, CoSinkable pattern, Sinkable e, InjectName e) 
=> Scope o

Ambient scope.

-> pattern n l

Pattern to refresh (if it clashes with the ambient scope).

-> (forall (o' :: S). DExt o o' => (Substitution e n o -> Substitution e l o') -> pattern o o' -> r)

Continuation, accepting the refreshed pattern.

-> r 

Safely rename (if necessary) a given pattern to extend a given scope. This is similar to withFreshPattern, except if a name in the pattern does not clash with the scope, it can be used immediately, without renaming.

This is a more general version of withRefreshed.

withRefreshedPattern' :: forall pattern (o :: S) e (n :: S) (l :: S) r. (CoSinkable pattern, Distinct o, InjectName e, Sinkable e) => Scope o -> pattern n l -> (forall (o' :: S). DExt o o' => ((Name n -> e o) -> Name l -> e o') -> pattern o o' -> r) -> r Source #

Refresh (if needed) bound variables introduced in a pattern.

This is a version of withRefreshedPattern that uses functional renamings instead of Substitution.

unsinkName :: forall (n :: S) (l :: S). NameBinder n l -> Name l -> Maybe (Name n) Source #

Try coercing the name back to the (smaller) scope, given a binder that extends that scope.

unsinkNamePattern :: forall pattern (n :: S) (l :: S). (Distinct n, CoSinkable pattern) => pattern n l -> Name l -> Maybe (Name n) Source #

Check if a name in the extended context is introduced in a pattern or comes from the outer scope n.

This is a generalization of unsinkName.

Safe (co)sinking and renaming

class SinkableK (f :: S -> k) where Source #

Minimal complete definition

Nothing

Methods

sinkabilityProofK :: forall (as :: LoT (S -> k)) (bs :: LoT (S -> k)) r. RenamingsK as bs -> (f :@@: as) -> (forall (cs :: LoT (S -> k)). RenamingsK as cs -> (f :@@: cs) -> r) -> r Source #

default sinkabilityProofK :: forall (as :: LoT (S -> k)) (bs :: LoT (S -> k)) r. (GenericK f, GSinkableK (RepK f)) => RenamingsK as bs -> (f :@@: as) -> (forall (cs :: LoT (S -> k)). RenamingsK as cs -> (f :@@: cs) -> r) -> r Source #

Instances

Instances details
SinkableK Name Source # 
Instance details

Defined in Control.Monad.Foil.Internal

Methods

sinkabilityProofK :: forall (as :: LoT (S -> Type)) (bs :: LoT (S -> Type)) r. RenamingsK as bs -> (Name :@@: as) -> (forall (cs :: LoT (S -> Type)). RenamingsK as cs -> (Name :@@: cs) -> r) -> r Source #

(Bifunctor sig, CoSinkable binder, SinkableK binder) => SinkableK (AST binder sig :: S -> Type) Source # 
Instance details

Defined in Control.Monad.Free.Foil

Methods

sinkabilityProofK :: forall (as :: LoT (S -> Type)) (bs :: LoT (S -> Type)) r. RenamingsK as bs -> (AST binder sig :@@: as) -> (forall (cs :: LoT (S -> Type)). RenamingsK as cs -> (AST binder sig :@@: cs) -> r) -> r Source #

(Bifunctor sig, CoSinkable binder, SinkableK binder) => SinkableK (ScopedAST binder sig :: S -> Type) Source # 
Instance details

Defined in Control.Monad.Free.Foil

Methods

sinkabilityProofK :: forall (as :: LoT (S -> Type)) (bs :: LoT (S -> Type)) r. RenamingsK as bs -> (ScopedAST binder sig :@@: as) -> (forall (cs :: LoT (S -> Type)). RenamingsK as cs -> (ScopedAST binder sig :@@: cs) -> r) -> r Source #

SinkableK NameBinder Source # 
Instance details

Defined in Control.Monad.Foil.Internal

Methods

sinkabilityProofK :: forall (as :: LoT (S -> S -> Type)) (bs :: LoT (S -> S -> Type)) r. RenamingsK as bs -> (NameBinder :@@: as) -> (forall (cs :: LoT (S -> S -> Type)). RenamingsK as cs -> (NameBinder :@@: cs) -> r) -> r Source #

SinkableK NameBinderList Source # 
Instance details

Defined in Control.Monad.Foil.Internal

Methods

sinkabilityProofK :: forall (as :: LoT (S -> S -> Type)) (bs :: LoT (S -> S -> Type)) r. RenamingsK as bs -> (NameBinderList :@@: as) -> (forall (cs :: LoT (S -> S -> Type)). RenamingsK as cs -> (NameBinderList :@@: cs) -> r) -> r Source #

SinkableK NameBinders Source # 
Instance details

Defined in Control.Monad.Foil.Internal

Methods

sinkabilityProofK :: forall (as :: LoT (S -> S -> Type)) (bs :: LoT (S -> S -> Type)) r. RenamingsK as bs -> (NameBinders :@@: as) -> (forall (cs :: LoT (S -> S -> Type)). RenamingsK as cs -> (NameBinders :@@: cs) -> r) -> r Source #

SinkableK U2 Source # 
Instance details

Defined in Control.Monad.Foil.Internal

Methods

sinkabilityProofK :: forall (as :: LoT (S -> S -> Type)) (bs :: LoT (S -> S -> Type)) r. RenamingsK as bs -> (U2 :@@: as) -> (forall (cs :: LoT (S -> S -> Type)). RenamingsK as cs -> (U2 :@@: cs) -> r) -> r Source #

SinkableK V2 Source # 
Instance details

Defined in Control.Monad.Foil.Internal

Methods

sinkabilityProofK :: forall (as :: LoT (S -> S -> Type)) (bs :: LoT (S -> S -> Type)) r. RenamingsK as bs -> (V2 :@@: as) -> (forall (cs :: LoT (S -> S -> Type)). RenamingsK as cs -> (V2 :@@: cs) -> r) -> r Source #

class Sinkable (e :: S -> Type) where Source #

Sinking an expression from scope n into a (usualy extended) scope l, given the renaming (injection from scope n to scope l).

Minimal complete definition

Nothing

Methods

sinkabilityProof Source #

Arguments

:: forall (n :: S) (l :: S). (Name n -> Name l)

Map names from scope n to a (possibly larger) scope l.

-> e n

Expression with free variables in scope n.

-> e l 

An implementation of this method that typechecks proves to the compiler that the expression is indeed Sinkable. However, instead of this implementation, sink should be used at all call sites for efficiency.

default sinkabilityProof :: forall (n :: S) (l :: S). (GenericK e, GSinkableK (RepK e)) => (Name n -> Name l) -> e n -> e l Source #

Instances

Instances details
Sinkable Expr Source #

This instance serves as a proof that sinking of Expr is safe.

Instance details

Defined in Control.Monad.Foil.Example

Methods

sinkabilityProof :: forall (n :: S) (l :: S). (Name n -> Name l) -> Expr n -> Expr l Source #

Sinkable Name Source #

Sinking a Name is as simple as applying the renaming.

Instance details

Defined in Control.Monad.Foil.Internal

Methods

sinkabilityProof :: forall (n :: S) (l :: S). (Name n -> Name l) -> Name n -> Name l Source #

Sinkable e => Sinkable (Substitution e i) Source #

Substitutions are sinkable as long as corresponding expressions are.

Instance details

Defined in Control.Monad.Foil.Internal

Methods

sinkabilityProof :: forall (n :: S) (l :: S). (Name n -> Name l) -> Substitution e i n -> Substitution e i l Source #

(Bifunctor sig, CoSinkable binder, SinkableK binder) => Sinkable (AST binder sig) Source # 
Instance details

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 Source #

(Bifunctor sig, CoSinkable binder, SinkableK binder) => Sinkable (ScopedAST binder sig) Source # 
Instance details

Defined in Control.Monad.Free.Foil

Methods

sinkabilityProof :: forall (n :: S) (l :: S). (Name n -> Name l) -> ScopedAST binder sig n -> ScopedAST binder sig l Source #

class CoSinkable (pattern :: S -> S -> Type) where Source #

CoSinkable is to patterns (generalized binders) what Sinkable is to expressions.

See Section 2.3 of «Free Foil: Generating Efficient and Scope-Safe Abstract Syntax» for more details.

Minimal complete definition

Nothing

Methods

coSinkabilityProof Source #

Arguments

:: forall (n :: S) (n' :: S) (l :: S) r. (Name n -> Name n')

Map names from scope n to a (possibly larger) scope n'.

-> pattern n l

A pattern that extends scope n to another scope l.

-> (forall (l' :: S). (Name l -> Name l') -> pattern n' l' -> r)

A continuation, accepting an extended renaming from l to l' (which itself extends n') and a (possibly refreshed) pattern that extends n' to l'.

-> r 

An implementation of this method that typechecks proves to the compiler that the pattern is indeed CoSinkable. However, instead of this implementation, extendRenaming should be used at all call sites for efficiency.

default coSinkabilityProof :: forall (n :: S) (n' :: S) (l :: S) r. (GenericK pattern, GSinkableK (RepK pattern)) => (Name n -> Name n') -> pattern n l -> (forall (l' :: S). (Name l -> Name l') -> pattern n' l' -> r) -> r Source #

withPattern Source #

Arguments

:: 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')

Processing of a single NameBinder, this will be applied to each binder in a pattern.

-> (forall (x :: S) (z :: S) (z' :: S). DExt z z' => f x x z z')

Result in case no binders are present. This can be seen as scope-indexed mempty.

-> (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'')

Composition of results for nested binders/patterns. This can be seen as scope-indexed mappend.

-> Scope o

Ambient scope.

-> pattern n l

Pattern to process.

-> (forall (o' :: S). DExt o o' => f n l o o' -> pattern o o' -> r)

Continuation, accepting result for the entire pattern and a (possibly refreshed) pattern.

-> r 

Generalized processing of a pattern.

You can see withPattern as a CPS-style traversal over the binders in a pattern.

default withPattern :: forall (o :: S) f (n :: S) (l :: S) r. (Distinct o, GenericK pattern, GValidNameBinders pattern (RepK pattern), GHasNameBinders (RepK pattern)) => (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 -> pattern n l -> (forall (o' :: S). DExt o o' => f n l o o' -> pattern o o' -> r) -> r Source #

Instances

Instances details
CoSinkable NameBinder Source # 
Instance details

Defined in Control.Monad.Foil.Internal

Methods

coSinkabilityProof :: forall (n :: S) (n' :: S) (l :: S) r. (Name n -> Name n') -> NameBinder n l -> (forall (l' :: S). (Name l -> Name l') -> NameBinder n' l' -> r) -> r Source #

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 -> NameBinder n l -> (forall (o' :: S). DExt o o' => f n l o o' -> NameBinder o o' -> r) -> r Source #

CoSinkable NameBinderList Source # 
Instance details

Defined in Control.Monad.Foil.Internal

Methods

coSinkabilityProof :: forall (n :: S) (n' :: S) (l :: S) r. (Name n -> Name n') -> NameBinderList n l -> (forall (l' :: S). (Name l -> Name l') -> NameBinderList n' l' -> r) -> r Source #

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 -> NameBinderList n l -> (forall (o' :: S). DExt o o' => f n l o o' -> NameBinderList o o' -> r) -> r Source #

CoSinkable NameBinders Source # 
Instance details

Defined in Control.Monad.Foil.Internal

Methods

coSinkabilityProof :: forall (n :: S) (n' :: S) (l :: S) r. (Name n -> Name n') -> NameBinders n l -> (forall (l' :: S). (Name l -> Name l') -> NameBinders n' l' -> r) -> r Source #

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 -> NameBinders n l -> (forall (o' :: S). DExt o o' => f n l o o' -> NameBinders o o' -> r) -> r Source #

CoSinkable U2 Source # 
Instance details

Defined in Control.Monad.Foil.Internal

Methods

coSinkabilityProof :: forall (n :: S) (n' :: S) (l :: S) r. (Name n -> Name n') -> U2 n l -> (forall (l' :: S). (Name l -> Name l') -> U2 n' l' -> r) -> r Source #

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 -> U2 n l -> (forall (o' :: S). DExt o o' => f n l o o' -> U2 o o' -> r) -> r Source #

CoSinkable V2 Source # 
Instance details

Defined in Control.Monad.Foil.Internal

Methods

coSinkabilityProof :: forall (n :: S) (n' :: S) (l :: S) r. (Name n -> Name n') -> V2 n l -> (forall (l' :: S). (Name l -> Name l') -> V2 n' l' -> r) -> r Source #

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 -> V2 n l -> (forall (o' :: S). DExt o o' => f n l o o' -> V2 o o' -> r) -> r Source #

class HasNameBinders (f :: S -> S -> Type) where Source #

If HasNameBinders f, then f n l is expected to act as a binder, introducing into scope n some local variables, extending it to scope l. This class allows to extract and modify the set of binders.

Minimal complete definition

Nothing

Methods

getNameBinders :: forall (n :: S) (l :: S). f n l -> NameBinders n l Source #

Extract a set of binders from a pattern.

Instances

Instances details
HasNameBinders NameBinder Source # 
Instance details

Defined in Control.Monad.Foil.Internal

Methods

getNameBinders :: forall (n :: S) (l :: S). NameBinder n l -> NameBinders n l Source #

unsafeSetNameBinders :: forall (n :: S) (l :: S) (l' :: S). NameBinder n l -> NameBinders n l' -> NameBinder n l' Source #

getNameBindersRaw :: forall (n :: S) (l :: S). NameBinder n l -> [RawName] Source #

reallyUnsafeSetNameBindersRaw :: forall (n :: S) (l :: S) (l' :: S). NameBinder n l -> [RawName] -> (NameBinder n l', [RawName]) Source #

HasNameBinders NameBinderList Source # 
Instance details

Defined in Control.Monad.Foil.Internal

Methods

getNameBinders :: forall (n :: S) (l :: S). NameBinderList n l -> NameBinders n l Source #

unsafeSetNameBinders :: forall (n :: S) (l :: S) (l' :: S). NameBinderList n l -> NameBinders n l' -> NameBinderList n l' Source #

getNameBindersRaw :: forall (n :: S) (l :: S). NameBinderList n l -> [RawName] Source #

reallyUnsafeSetNameBindersRaw :: forall (n :: S) (l :: S) (l' :: S). NameBinderList n l -> [RawName] -> (NameBinderList n l', [RawName]) Source #

sink :: forall e (n :: S) (l :: S). (Sinkable e, DExt n l) => e n -> e l Source #

Efficient version of sinkabilityProof. In fact, once sinkabilityProof typechecks, it is safe to sink by coercion. See Section 3.5 in «The Foil: Capture-Avoiding Substitution With No Sharp Edges» for the details.

extendRenaming Source #

Arguments

:: forall pattern (n :: S) (n' :: S) (l :: S) r. CoSinkable pattern 
=> (Name n -> Name n')

Map names from scope n to a (possibly larger) scope n'.

-> pattern n l

A pattern that extends scope n to another scope l.

-> (forall (l' :: S). (Name l -> Name l') -> pattern n' l' -> r)

A continuation, accepting an extended renaming from l to l' (which itself extends n') and a (possibly refreshed) pattern that extends n' to l'.

-> r 

Extend renaming when going under a CoSinkable pattern (generalized binder). Note that the scope under pattern is independent of the codomain of the renaming.

This function is used to go under binders when implementing sinkabilityProof and is both a generalization of extendRenamingNameBinder and an efficient implementation of coSinkabilityProof.

extendNameBinderRenaming Source #

Arguments

:: forall pattern (i :: S) (n :: S) (n' :: S) (l :: S) r. CoSinkable pattern 
=> (NameBinder i n -> NameBinder i n')

Map names from scope n to a (possibly larger) scope n'.

-> pattern n l

A pattern that extends scope n to another scope l.

-> (forall (l' :: S). (NameBinder n' l -> NameBinder n' l') -> pattern n' l' -> r)

A continuation, accepting an extended renaming from l to l' (which itself extends n') and a (possibly refreshed) pattern that extends n' to l'.

-> r 

Extend renaming of binders when going under a CoSinkable pattern (generalized binder). Note that the scope under pattern is independent of the codomain of the renaming.

composeNameBinderRenamings Source #

Arguments

:: forall (n :: S) (i :: S) (i' :: S) (l :: S) (l' :: S). (NameBinder n i -> NameBinder n i')

Rename binders extending scope n from i to i'.

-> (NameBinder i' l -> NameBinder i' l')

Rename binders extending scope i' from l to l'.

-> NameBinder n l 
-> NameBinder n l' 

Safely compose renamings of name binders. The underlying implementation is

fromNameBinderRenaming :: forall (n :: S) (l :: S) (l' :: S). (NameBinder n l -> NameBinder n l') -> Name l -> Name l' Source #

Convert renaming of name binders into renaming of names in the inner scopes.

extendRenamingNameBinder Source #

Arguments

:: forall (n :: S) (n' :: S) (l :: S) r. (Name n -> Name n')

Map names from scope n to a (possibly larger) scope n'.

-> NameBinder n l

A name binder that extends scope n to another scope l.

-> (forall (l' :: S). (Name l -> Name l') -> NameBinder n' l' -> r)

A continuation, accepting an extended renaming from l to l' (which itself extends n') and a (possibly refreshed) binder that extends n' to l'.

-> r 

Extend renaming when going under a NameBinder. Note that the scope under binder is independent of the codomain of the renaming.

Semantically, this function may need to rename the binder (resulting in the new scope l'), to make sure it does not clash with scope n'. However, as it turns out, the foil makes it safe to implement this function as a coercion. See Appendix A in «The Foil: Capture-Avoiding Substitution With No Sharp Edges» for the details.

This function is used to go under binders when implementing sinkabilityProof. A generalization of this function is extendRenaming (which is an efficient version of coSinkabilityProof).

Safe substitutions

data Substitution (e :: S -> Type) (i :: S) (o :: S) Source #

A substitution is a mapping from names in scope i to expressions e o in scope o.

Instances

Instances details
Sinkable e => Sinkable (Substitution e i) Source #

Substitutions are sinkable as long as corresponding expressions are.

Instance details

Defined in Control.Monad.Foil.Internal

Methods

sinkabilityProof :: forall (n :: S) (l :: S). (Name n -> Name l) -> Substitution e i n -> Substitution e i l Source #

lookupSubst :: forall e (i :: S) (o :: S). InjectName e => Substitution e i o -> Name i -> e o Source #

Apply substitution to a given name.

identitySubst :: forall (e :: S -> Type) (i :: S). InjectName e => Substitution e i i Source #

Identity substitution maps all names to expresion-variables.

voidSubst :: forall (e :: S -> Type) (n :: S). Substitution e 'VoidS n Source #

An empty substitution from an empty scope.

addSubst :: forall e (i :: S) (o :: S) (i' :: S). Substitution e i o -> NameBinder i i' -> e o -> Substitution e i' o Source #

Extend substitution with a particular mapping.

addSubstPattern :: forall binder e (i :: S) (o :: S) (i' :: S). CoSinkable binder => Substitution e i o -> binder i i' -> [e o] -> Substitution e i' o Source #

addSubstList :: forall e (i :: S) (o :: S) (i' :: S). Substitution e i o -> NameBinderList i i' -> [e o] -> Substitution e i' o Source #

addRename :: forall (e :: S -> Type) (i :: S) (o :: S) (i' :: S). InjectName e => Substitution e i o -> NameBinder i i' -> Name o -> Substitution e i' o Source #

Add variable renaming to a substitution. This includes the performance optimization of eliding names mapped to themselves.

Unification of binders

data UnifyNameBinders (pattern :: S -> S -> Type) (n :: S) (l :: S) (r :: S) where Source #

Unification result for two binders, extending some common scope to scopes l and r respectively.

Due to the implementation of the foil, we can often rename binders efficiently, by renaming binders only in one of the two unified terms.

Constructors

SameNameBinders

Binders are the same, proving that type parameters l and r are in fact equivalent.

Fields

  • :: forall (n :: S) (l :: S) (pattern :: S -> S -> Type). NameBinders n l

    Unordered set of binders in the unified pattern (from any of the original patterns).

  • -> UnifyNameBinders pattern n l l
     
RenameLeftNameBinder

It is possible to safely rename the left binder to match the right one.

Fields

RenameRightNameBinder

It is possible to safely rename the right binder to match the left one.

Fields

RenameBothBinders

It is necessary to rename both binders.

Fields

NotUnifiable :: forall (pattern :: S -> S -> Type) (n :: S) (l :: S) (r :: S). UnifyNameBinders pattern n l r

Cannot unify to (sub)patterns.

unifyNameBinders Source #

Arguments

:: forall (i :: S) (l :: S) (r :: S) (pattern :: S -> S -> Type). Distinct i 
=> NameBinder i l

Left pattern.

-> NameBinder i r

Right pattern.

-> UnifyNameBinders pattern i l r 

Unify binders either by asserting that they are the same, or by providing a safe renaming function to convert one binder to another.

andThenUnifyPatterns Source #

Arguments

:: forall pattern (l :: S) (l' :: S) (n :: S) (r :: S) (r' :: S). (UnifiablePattern pattern, Distinct l, Distinct l') 
=> UnifyNameBinders pattern n l l'

Unifying action for some outer patterns.

-> (pattern l r, pattern l' r')

Two nested patterns (cannot be unified directly since they extend different scopes).

-> UnifyNameBinders pattern n r r' 

Chain unification of nested patterns.

andThenUnifyNameBinders Source #

Arguments

:: forall (pattern :: S -> S -> Type) (l :: S) (l' :: S) (n :: S) (r :: S) (r' :: S). (UnifiablePattern pattern, Distinct l, Distinct l') 
=> UnifyNameBinders pattern n l l'

Unifying action for some outer patterns.

-> (NameBinder l r, NameBinder l' r')

Two nested binders (cannot be unified directly since they extend different scopes).

-> UnifyNameBinders pattern n r r' 

Chain unification of nested patterns with NameBinders.

class CoSinkable pattern => UnifiablePattern (pattern :: S -> S -> Type) where Source #

A pattern type is unifiable if it is possible to match two patterns and decide how to rename binders.

Minimal complete definition

Nothing

Methods

unifyPatterns :: forall (n :: S) (l :: S) (r :: S). Distinct n => pattern n l -> pattern n r -> UnifyNameBinders pattern n l r Source #

Unify two patterns and decide which binders need to be renamed.

default unifyPatterns :: forall (n :: S) (l :: S) (r :: S). (CoSinkable pattern, Distinct n) => pattern n l -> pattern n r -> UnifyNameBinders pattern n l r Source #

Instances

Instances details
UnifiablePattern NameBinder Source # 
Instance details

Defined in Control.Monad.Foil.Internal

Methods

unifyPatterns :: forall (n :: S) (l :: S) (r :: S). Distinct n => NameBinder n l -> NameBinder n r -> UnifyNameBinders NameBinder n l r Source #

UnifiablePattern NameBinderList Source # 
Instance details

Defined in Control.Monad.Foil.Internal

Methods

unifyPatterns :: forall (n :: S) (l :: S) (r :: S). Distinct n => NameBinderList n l -> NameBinderList n r -> UnifyNameBinders NameBinderList n l r Source #

UnifiablePattern U2 Source # 
Instance details

Defined in Control.Monad.Foil.Internal

Methods

unifyPatterns :: forall (n :: S) (l :: S) (r :: S). Distinct n => U2 n l -> U2 n r -> UnifyNameBinders U2 n l r Source #

UnifiablePattern V2 Source # 
Instance details

Defined in Control.Monad.Foil.Internal

Methods

unifyPatterns :: forall (n :: S) (l :: S) (r :: S). Distinct n => V2 n l -> V2 n r -> UnifyNameBinders V2 n l r Source #

class UnifiableInPattern a where Source #

Unification of values in patterns. By default, Eq instance is used, but it may be useful to ignore some data in pattens (such as location annotations).

Minimal complete definition

Nothing

Methods

unifyInPattern :: a -> a -> Bool Source #

Unify non-binding components of a pattern.

default unifyInPattern :: Eq a => a -> a -> Bool Source #

data NameBinders (n :: S) (l :: S) Source #

An unordered collection of NameBinders, that together extend scope n to scope l.

For an ordered version see NameBinderList.

Instances

Instances details
CoSinkable NameBinders Source # 
Instance details

Defined in Control.Monad.Foil.Internal

Methods

coSinkabilityProof :: forall (n :: S) (n' :: S) (l :: S) r. (Name n -> Name n') -> NameBinders n l -> (forall (l' :: S). (Name l -> Name l') -> NameBinders n' l' -> r) -> r Source #

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 -> NameBinders n l -> (forall (o' :: S). DExt o o' => f n l o o' -> NameBinders o o' -> r) -> r Source #

SinkableK NameBinders Source # 
Instance details

Defined in Control.Monad.Foil.Internal

Methods

sinkabilityProofK :: forall (as :: LoT (S -> S -> Type)) (bs :: LoT (S -> S -> Type)) r. RenamingsK as bs -> (NameBinders :@@: as) -> (forall (cs :: LoT (S -> S -> Type)). RenamingsK as cs -> (NameBinders :@@: cs) -> r) -> r Source #

emptyNameBinders :: forall (n :: S). NameBinders n n Source #

An empty set of binders keeps the scope as is.

mergeNameBinders :: forall (n :: S) (i :: S) (l :: S). NameBinders n i -> NameBinders i l -> NameBinders n l Source #

Composition of sets of binders.

Eliminating impossible unification

data V2 (n :: S) (l :: S) Source #

An empty pattern type specifies zero possibilities for patterns.

This type can be used to specify that patterns are not possible.

Instances

Instances details
CoSinkable V2 Source # 
Instance details

Defined in Control.Monad.Foil.Internal

Methods

coSinkabilityProof :: forall (n :: S) (n' :: S) (l :: S) r. (Name n -> Name n') -> V2 n l -> (forall (l' :: S). (Name l -> Name l') -> V2 n' l' -> r) -> r Source #

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 -> V2 n l -> (forall (o' :: S). DExt o o' => f n l o o' -> V2 o o' -> r) -> r Source #

UnifiablePattern V2 Source # 
Instance details

Defined in Control.Monad.Foil.Internal

Methods

unifyPatterns :: forall (n :: S) (l :: S) (r :: S). Distinct n => V2 n l -> V2 n r -> UnifyNameBinders V2 n l r Source #

SinkableK V2 Source # 
Instance details

Defined in Control.Monad.Foil.Internal

Methods

sinkabilityProofK :: forall (as :: LoT (S -> S -> Type)) (bs :: LoT (S -> S -> Type)) r. RenamingsK as bs -> (V2 :@@: as) -> (forall (cs :: LoT (S -> S -> Type)). RenamingsK as cs -> (V2 :@@: cs) -> r) -> r Source #

GenericK V2 Source # 
Instance details

Defined in Control.Monad.Foil.Internal

Associated Types

type RepK V2 
Instance details

Defined in Control.Monad.Foil.Internal

type RepK V2 = V1 :: LoT (S -> S -> Type) -> Type

Methods

fromK :: forall (x :: LoT (S -> S -> Type)). (V2 :@@: x) -> RepK V2 x #

toK :: forall (x :: LoT (S -> S -> Type)). RepK V2 x -> V2 :@@: x #

type RepK V2 Source # 
Instance details

Defined in Control.Monad.Foil.Internal

type RepK V2 = V1 :: LoT (S -> S -> Type) -> Type

absurd2 :: forall (n :: S) (l :: S) a. V2 n l -> a Source #

Since V2 values logically don't exist, this witnesses the logical reasoning tool of "ex falso quodlibet".

Name maps

data NameMap (n :: S) a Source #

A total map from names in scope n to elements of type a.

Instances

Instances details
Foldable (NameMap n) Source # 
Instance details

Defined in Control.Monad.Foil.Internal

Methods

fold :: Monoid m => NameMap n m -> m #

foldMap :: Monoid m => (a -> m) -> NameMap n a -> m #

foldMap' :: Monoid m => (a -> m) -> NameMap n a -> m #

foldr :: (a -> b -> b) -> b -> NameMap n a -> b #

foldr' :: (a -> b -> b) -> b -> NameMap n a -> b #

foldl :: (b -> a -> b) -> b -> NameMap n a -> b #

foldl' :: (b -> a -> b) -> b -> NameMap n a -> b #

foldr1 :: (a -> a -> a) -> NameMap n a -> a #

foldl1 :: (a -> a -> a) -> NameMap n a -> a #

toList :: NameMap n a -> [a] #

null :: NameMap n a -> Bool #

length :: NameMap n a -> Int #

elem :: Eq a => a -> NameMap n a -> Bool #

maximum :: Ord a => NameMap n a -> a #

minimum :: Ord a => NameMap n a -> a #

sum :: Num a => NameMap n a -> a #

product :: Num a => NameMap n a -> a #

Traversable (NameMap n) Source # 
Instance details

Defined in Control.Monad.Foil.Internal

Methods

traverse :: Applicative f => (a -> f b) -> NameMap n a -> f (NameMap n b) #

sequenceA :: Applicative f => NameMap n (f a) -> f (NameMap n a) #

mapM :: Monad m => (a -> m b) -> NameMap n a -> m (NameMap n b) #

sequence :: Monad m => NameMap n (m a) -> m (NameMap n a) #

Functor (NameMap n) Source # 
Instance details

Defined in Control.Monad.Foil.Internal

Methods

fmap :: (a -> b) -> NameMap n a -> NameMap n b #

(<$) :: a -> NameMap n b -> NameMap n a #

emptyNameMap :: NameMap 'VoidS a Source #

An empty map belongs in the empty scope.

lookupName :: forall (n :: S) a. Name n -> NameMap n a -> a Source #

Looking up a name should always succeed.

Note that since Name is Sinkable, you can lookup a name from scope n in a NameMap for scope l whenever l extends n.

addNameBinder :: forall (n :: S) (l :: S) a. NameBinder n l -> a -> NameMap n a -> NameMap l a Source #

Extending a map with a single mapping.

Note that the scope parameter of the result differs from the initial map.

nameMapToSubstitution :: forall (i :: S) e (o :: S). NameMap i (e o) -> Substitution e i o Source #

Convert a NameMap of expressions into a Substitution.

addNameBinders :: forall binder (n :: S) (l :: S) a. CoSinkable binder => binder n l -> [a] -> NameMap n a -> NameMap l a Source #

Extend a map with multiple mappings (by repeatedly applying addNameBinder).

Note that the input list is expected to have at least the same number of elements as there are binders in the input pattern (generalized binder).

addNameBinderList :: forall (n :: S) (l :: S) a. NameBinderList n l -> [a] -> NameMap n a -> NameMap l a Source #

Extend a map with multiple mappings (by repeatedly applying addNameBinder).

Note that the input list is expected to have at least the same number of elements as there are binders in the input name binder list.

See also addNameBinders for a generalized version.

data NameBinderList (n :: S) (l :: S) where Source #

An ordered collection (list) of NameBinders, that together extend scope n to scope l.

For an unordered version see NameBinders.

Constructors

NameBinderListEmpty :: forall (n :: S). NameBinderList n n

An empty list of binders keeps the scope as is.

NameBinderListCons

A non-empty list of binders.

Fields

Instances

Instances details
CoSinkable NameBinderList Source # 
Instance details

Defined in Control.Monad.Foil.Internal

Methods

coSinkabilityProof :: forall (n :: S) (n' :: S) (l :: S) r. (Name n -> Name n') -> NameBinderList n l -> (forall (l' :: S). (Name l -> Name l') -> NameBinderList n' l' -> r) -> r Source #

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 -> NameBinderList n l -> (forall (o' :: S). DExt o o' => f n l o o' -> NameBinderList o o' -> r) -> r Source #

HasNameBinders NameBinderList Source # 
Instance details

Defined in Control.Monad.Foil.Internal

Methods

getNameBinders :: forall (n :: S) (l :: S). NameBinderList n l -> NameBinders n l Source #

unsafeSetNameBinders :: forall (n :: S) (l :: S) (l' :: S). NameBinderList n l -> NameBinders n l' -> NameBinderList n l' Source #

getNameBindersRaw :: forall (n :: S) (l :: S). NameBinderList n l -> [RawName] Source #

reallyUnsafeSetNameBindersRaw :: forall (n :: S) (l :: S) (l' :: S). NameBinderList n l -> [RawName] -> (NameBinderList n l', [RawName]) Source #

UnifiablePattern NameBinderList Source # 
Instance details

Defined in Control.Monad.Foil.Internal

Methods

unifyPatterns :: forall (n :: S) (l :: S) (r :: S). Distinct n => NameBinderList n l -> NameBinderList n r -> UnifyNameBinders NameBinderList n l r Source #

SinkableK NameBinderList Source # 
Instance details

Defined in Control.Monad.Foil.Internal

Methods

sinkabilityProofK :: forall (as :: LoT (S -> S -> Type)) (bs :: LoT (S -> S -> Type)) r. RenamingsK as bs -> (NameBinderList :@@: as) -> (forall (cs :: LoT (S -> S -> Type)). RenamingsK as cs -> (NameBinderList :@@: cs) -> r) -> r Source #

GenericK NameBinderList Source # 
Instance details

Defined in Control.Monad.Foil.Internal

Associated Types

type RepK NameBinderList 
Instance details

Defined in Control.Monad.Foil.Internal

type RepK NameBinderList = (((Var0 :: Atom (S -> S -> Type) S) :~~: (Var1 :: Atom (S -> S -> Type) S)) :=>: (U1 :: LoT (S -> S -> Type) -> Type)) :+: Exists S (Field ((NameBinder :$: (Var1 :: Atom (S -> S -> S -> Type) S)) ':@: (Var0 :: Atom (S -> S -> S -> Type) S)) :*: Field ((NameBinderList :$: (Var0 :: Atom (S -> S -> S -> Type) S)) ':@: (Var2 :: Atom (S -> S -> S -> Type) S)))

Methods

fromK :: forall (x :: LoT (S -> S -> Type)). (NameBinderList :@@: x) -> RepK NameBinderList x #

toK :: forall (x :: LoT (S -> S -> Type)). RepK NameBinderList x -> NameBinderList :@@: x #

type RepK NameBinderList Source # 
Instance details

Defined in Control.Monad.Foil.Internal

type RepK NameBinderList = (((Var0 :: Atom (S -> S -> Type) S) :~~: (Var1 :: Atom (S -> S -> Type) S)) :=>: (U1 :: LoT (S -> S -> Type) -> Type)) :+: Exists S (Field ((NameBinder :$: (Var1 :: Atom (S -> S -> S -> Type) S)) ':@: (Var0 :: Atom (S -> S -> S -> Type) S)) :*: Field ((NameBinderList :$: (Var0 :: Atom (S -> S -> S -> Type) S)) ':@: (Var2 :: Atom (S -> S -> S -> Type) S)))

Constraints

class (ExtEndo n => ExtEndo l) => Ext (n :: S) (l :: S) Source #

Some scopes are extensions of other scopes.

Important: this class exists to assist tracking scope extensions for type variables of kind S. Users of the foil are not supposed to implement any instances of Ext.

Instances

Instances details
(ExtEndo n => ExtEndo l) => Ext n l Source # 
Instance details

Defined in Control.Monad.Foil.Internal

data ExtEvidence (n :: S) (l :: S) where Source #

Evidence that scope l extends scope n.

Constructors

Ext :: forall (n :: S) (l :: S). Ext n l => ExtEvidence n l 

class Distinct (n :: S) Source #

Scopes with distinct names.

Important: this class exists to explicitly mark scopes with distinct names. Users of the foil are not supposed to implement any instances of Distinct.

Instances

Instances details
Distinct 'VoidS Source # 
Instance details

Defined in Control.Monad.Foil.Internal

data DistinctEvidence (n :: S) where Source #

Evidence that scope n contains distinct names.

Constructors

Distinct :: forall (n :: S). Distinct n => DistinctEvidence n 

assertDistinct :: forall (n :: S) pattern (l :: S). (Distinct n, CoSinkable pattern) => pattern n l -> DistinctEvidence l Source #

A distinct scope extended with a NameBinder is also distinct.

assertExt :: forall pattern (n :: S) (l :: S). CoSinkable pattern => pattern n l -> ExtEvidence n l Source #

A distinct scope extended with a NameBinder is also distinct.

type DExt (n :: S) (l :: S) = (Distinct l, Ext n l) Source #

Scope extensions with distinct names.

class InjectName (e :: S -> Type) where Source #

Instances of this typeclass possess the ability to inject names. Usually, this is a variable data constructor.

Methods

injectName :: forall (n :: S). Name n -> e n Source #

Inject names into expressions.

Instances

Instances details
InjectName Expr Source # 
Instance details

Defined in Control.Monad.Foil.Example

Methods

injectName :: forall (n :: S). Name n -> Expr n Source #

InjectName (AST binder sig) Source # 
Instance details

Defined in Control.Monad.Free.Foil

Methods

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