Safe Haskell	None
Language	Haskell2010

Language.Syntactic.Functional.WellScoped

Description

Well-scoped terms

Synopsis

class Ext ext orig where
- unext :: ext -> orig
- diff :: Num a => Proxy ext -> Proxy orig -> a
lookEnv :: forall env a e. Ext env (a, e) => Proxy e -> Reader env a
data BindingWS sig where
- VarWS :: Ext env (a, e) => Proxy e -> BindingWS (Full (Reader env a))
- LamWS :: BindingWS (Reader (a, e) b :-> Full (Reader e (a -> b)))
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))
evalOpenWS :: Eval s => env -> ASTF s (Reader env a) -> a
evalClosedWS :: Eval s => ASTF s (Reader () a) -> a
type family LiftReader env sig
type family UnReader a
type family LowerReader sig
data ReaderSym sym sig where
- 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)
type WS sym env a = ASTF (BindingWS :+: ReaderSym sym) (Reader env a)
fromWS :: WS sym env a -> ASTF (Binding :+: sym) a
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

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)