syntactic-3.8: Generic representation and manipulation of abstract syntax

Safe HaskellNone
LanguageHaskell2010

Language.Syntactic.Functional.WellScoped

Description

Well-scoped terms

Synopsis

Documentation

class Ext ext orig where Source #

Environment extension

Methods

unext :: ext -> orig Source #

Remove the extension of an environment

diff :: Num a => Proxy ext -> Proxy orig -> a Source #

Return the amount by which an environment has been extended

Instances
(Ext env e, ext ~ (a, env)) => Ext ext e Source # 
Instance details

Defined in Language.Syntactic.Functional.WellScoped

Methods

unext :: ext -> e Source #

diff :: Num a => Proxy ext -> Proxy e -> a Source #

Ext env env Source # 
Instance details

Defined in Language.Syntactic.Functional.WellScoped

Methods

unext :: env -> env Source #

diff :: Num a => Proxy env -> Proxy env -> a Source #

lookEnv :: forall env a e. Ext env (a, e) => Proxy e -> Reader env a Source #

Lookup in an extended environment

data BindingWS sig where Source #

Well-scoped variable binding

Well-scoped terms are introduced to be able to evaluate without type casting. The implementation is inspired by "Typing Dynamic Typing" (Baars and Swierstra, ICFP 2002, http://doi.acm.org/10.1145/581478.581494) where expressions are represented as (essentially) Reader env a after "compilation". However, a major difference is that "Typing Dynamic Typing" starts from an untyped term, and thus needs (safe) dynamic type casting during compilation. In contrast, the denotational semantics of BindingWS (the Eval instance) uses no type casting.

Constructors

VarWS :: Ext env (a, e) => Proxy e -> BindingWS (Full (Reader env a)) 
LamWS :: BindingWS (Reader (a, e) b :-> Full (Reader e (a -> b))) 
Instances
NFData1 BindingWS Source # 
Instance details

Defined in Language.Syntactic.Functional.WellScoped

Methods

rnf1 :: BindingWS a -> () Source #

Symbol BindingWS Source # 
Instance details

Defined in Language.Syntactic.Functional.WellScoped

Methods

symSig :: BindingWS sig -> SigRep sig Source #

Eval BindingWS Source # 
Instance details

Defined in Language.Syntactic.Functional.WellScoped

Methods

evalSym :: BindingWS sig -> Denotation sig Source #

lamWS :: forall a e sym b. BindingWS :<: sym => ((forall env. Ext env (a, e) => ASTF sym (Reader env a)) -> ASTF sym (Reader (a, e) b)) -> ASTF sym (Reader e (a -> b)) Source #

Higher-order interface for well-scoped variable binding

Inspired by Conor McBride's "I am not a number, I am a classy hack" (http://mazzo.li/epilogue/index.html%3Fp=773.html).

evalOpenWS :: Eval s => env -> ASTF s (Reader env a) -> a Source #

Evaluation of open well-scoped terms

evalClosedWS :: Eval s => ASTF s (Reader () a) -> a Source #

Evaluation of closed well-scoped terms

type family LiftReader env sig Source #

Mapping from a symbol signature

a :-> b :-> Full c

to

Reader env a :-> Reader env b :-> Full (Reader env c)
Instances
type LiftReader env (Full a) Source # 
Instance details

Defined in Language.Syntactic.Functional.WellScoped

type LiftReader env (Full a) = Full (Reader env a)
type LiftReader env (a :-> sig) Source # 
Instance details

Defined in Language.Syntactic.Functional.WellScoped

type LiftReader env (a :-> sig) = Reader env a :-> LiftReader env sig

type family UnReader a Source #

Instances
type UnReader (Reader e a) Source # 
Instance details

Defined in Language.Syntactic.Functional.WellScoped

type UnReader (Reader e a) = a

type family LowerReader sig Source #

Mapping from a symbol signature

Reader e a :-> Reader e b :-> Full (Reader e c)

to

a :-> b :-> Full c
Instances
type LowerReader (Full a) Source # 
Instance details

Defined in Language.Syntactic.Functional.WellScoped

type LowerReader (Full a) = Full (UnReader a)
type LowerReader (a :-> sig) Source # 
Instance details

Defined in Language.Syntactic.Functional.WellScoped

type LowerReader (a :-> sig) = UnReader a :-> LowerReader sig

data ReaderSym sym sig where Source #

Wrap a symbol to give it a LiftReader signature

Constructors

ReaderSym :: (Signature sig, Denotation (LiftReader env sig) ~ DenotationM (Reader env) sig, LowerReader (LiftReader env sig) ~ sig) => Proxy env -> sym sig -> ReaderSym sym (LiftReader env sig) 
Instances
Eval sym => Eval (ReaderSym sym) Source # 
Instance details

Defined in Language.Syntactic.Functional.WellScoped

Methods

evalSym :: ReaderSym sym sig -> Denotation sig Source #

type WS sym env a = ASTF (BindingWS :+: ReaderSym sym) (Reader env a) Source #

Well-scoped AST

fromWS :: WS sym env a -> ASTF (Binding :+: sym) a Source #

Convert the representation of variables and binders from BindingWS to Binding. The latter is easier to analyze, has a Render instance, etc.

smartWS :: forall sig sig' bsym f sub sup env a. (Signature sig, Signature sig', sub :<: sup, bsym ~ (BindingWS :+: ReaderSym sup), f ~ SmartFun bsym sig', sig' ~ SmartSig f, bsym ~ SmartSym f, sig' ~ LiftReader env sig, Denotation (LiftReader env sig) ~ DenotationM (Reader env) sig, LowerReader (LiftReader env sig) ~ sig, Reader env a ~ DenResult sig') => sub sig -> f Source #

Make a smart constructor for well-scoped terms. smartWS has any type of the form:

smartWS :: (sub :<: sup, bsym ~ (BindingWS :+: ReaderSym sup))
    => sub (a :-> b :-> ... :-> Full x)
    -> ASTF bsym (Reader env a) -> ASTF bsym (Reader env b) -> ... -> ASTF bsym (Reader env x)