Safe Haskell	None
Language	Haskell2010

Language.Syntactic.Functional.WellScoped

Description

Well-scoped terms

Synopsis

Documentation

class Ext ext orig where Source #

Environment extension

Minimal complete definition

unext, diff

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 #
Methods unext :: ext -> e Source # diff :: Num a => Proxy * ext -> Proxy * e -> a Source #
Ext env env Source #
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 #
Methods liftRnf :: (a -> ()) -> BindingWS a -> () #
Symbol BindingWS Source #
Methods symSig :: BindingWS sig -> SigRep sig Source #
Eval BindingWS Source #
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 #
type LiftReader env (Full a) = Full (Reader env a)
type LiftReader env ((:->) a sig) Source #
type LiftReader env ((:->) a sig) = (:->) (Reader env a) (LiftReader env sig)

type family UnReader a Source #

Instances

type UnReader (Reader e a) Source #
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 #
type LowerReader (Full a) = Full (UnReader a)
type LowerReader ((:->) a sig) Source #
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 #
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)