Safe Haskell | None |
---|---|
Language | Haskell2010 |
Well-scoped terms
- class Ext ext orig where
- lookEnv :: forall env a e. Ext env (a, e) => Proxy e -> Reader env a
- data BindingWS sig where
- 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
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)
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 Reader
env aBindingWS
(the Eval
instance)
uses no type casting.
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)
type LiftReader env (Full a) = Full (Reader env a) Source | |
type LiftReader env ((:->) a sig) = (:->) (Reader env a) (LiftReader env sig) Source |
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
type LowerReader (Full a) = Full (UnReader a) Source | |
type LowerReader ((:->) a sig) = (:->) (UnReader a) (LowerReader sig) Source |
data ReaderSym sym sig where Source
Wrap a symbol to give it a LiftReader
signature
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) |
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)