syntactic-0.3: Generic abstract syntax, and utilities for embedded languages



This module provides binding constructs using higher-order syntax and a function for translating back to first-order syntax. Expressions constructed using the exported interface are guaranteed to have a well-behaved translation.



data Variable a Source


evalLambda :: Eval dom => ASTF (Lambda :+: (Variable :+: dom)) a -> aSource

Evaluation of closed Lambda expressions

data Let a whereSource

Let binding


Let :: Let (a :-> ((a -> b) :-> Full b)) 

data HOLambda dom a whereSource

Higher-order lambda binding


HOLambda :: (Typeable a, Typeable b) => (HOAST dom (Full a) -> HOAST dom (Full b)) -> HOLambda dom (Full (a -> b)) 

type HOAST dom = AST (HOLambda dom :+: (Variable :+: dom))Source

lambda :: (Typeable a, Typeable b) => (HOAST dom (Full a) -> HOAST dom (Full b)) -> HOAST dom (Full (a -> b))Source

Lambda binding

lambdaN :: NAry a (HOLambda dom :+: (Variable :+: dom)) => a -> HOAST dom (Full (NAryEval a))Source

N-ary lambda binding

let_ :: (Typeable a, Typeable b, Let :<: dom) => HOAST dom (Full a) -> (HOAST dom (Full a) -> HOAST dom (Full b)) -> HOAST dom (Full b)Source

Let binding

reifyHOAST :: Typeable a => HOAST dom a -> AST (Lambda :+: (Variable :+: dom)) aSource

Translating expressions with higher-order binding to corresponding expressions using first-order binding

class (SyntacticN a internal, NAry internal (HOLambda dom :+: (Variable :+: dom)), Typeable (NAryEval internal)) => Reifiable a dom internal | a -> dom internalSource

Convenient class alias for n-ary syntactic functions


(SyntacticN a internal, NAry internal (:+: (HOLambda dom) (:+: Variable dom)), Typeable (NAryEval internal)) => Reifiable a dom internal 

reify :: Reifiable a dom internal => a -> ASTF (Lambda :+: (Variable :+: dom)) (NAryEval internal)Source

Reifying an n-ary syntactic function