syntactic-3.6.1: Generic representation and manipulation of abstract syntax

Safe HaskellNone



Well-scoped terms



class Ext ext orig where Source

Environment extension


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


(Ext env e, (~) * ext (a, env)) => Ext ext e Source 
Ext env env 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, 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.


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

Higher-order interface for well-scoped variable binding

Inspired by Conor McBride's "I am not a number, I am a classy hack" (

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


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 UnReader a Source


type UnReader (Reader e a) = a Source 

type family LowerReader sig Source

Mapping from a symbol signature

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


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) 


Eval sym => Eval (ReaderSym sym) 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)