syntactic-0.1: 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 => AST (Lambda :+: (Variable :+: dom)) (Full 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, NAryDom 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

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

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