Language.Syntactic.Functional.WellScoped

Well-scoped terms

Documentation

class Ext ext orig where

Environment extension

Minimal complete definition

unext, diff

Methods

unext :: ext -> orig

Remove the extension of an environment

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

Return the amount by which an environment has been extended

Instances

(Ext env e, (~) * ext (a, env)) => Ext ext e

Methods

unext :: ext -> e

diff :: Num a => Proxy * ext -> Proxy * e -> a

Ext env env

Methods

unext :: env -> env

diff :: Num a => Proxy * env -> Proxy * env -> a

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

Lookup in an extended environment

data BindingWS sig where

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

Methods

rnf1 :: BindingWS a -> ()

Symbol BindingWS

Methods

symSig :: BindingWS sig -> SigRep sig

Eval BindingWS

Methods

evalSym :: BindingWS sig -> Denotation sig

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

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

Evaluation of open well-scoped terms

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

Evaluation of closed well-scoped terms

type family LiftReader env sig

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)

type LiftReader env (Full a) = Full (Reader env a)

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

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

type family UnReader a

Instances

type UnReader (Reader e a)

type UnReader (Reader e a) = a

type family LowerReader sig

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)

type LowerReader (Full a) = Full (UnReader a)

type LowerReader ((:->) a sig)

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

data ReaderSym sym sig where

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)

Methods

evalSym :: ReaderSym sym sig -> Denotation sig

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

Well-scoped AST

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

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

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)