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
- evalLambda :: Eval dom => ASTF (Lambda :+: (Variable :+: dom)) a -> a
- data Let a where
- data HOLambda dom a where
- type HOAST dom = AST (HOLambda dom :+: (Variable :+: dom))
- lambda :: (Typeable a, Typeable b) => (HOAST dom (Full a) -> HOAST dom (Full b)) -> HOAST dom (Full (a -> b))
- lambdaN :: NAry a (HOLambda dom :+: (Variable :+: dom)) => a -> HOAST dom (Full (NAryEval a))
- letBind :: (Typeable a, Typeable b, Let :<: dom) => HOAST dom (Full a) -> (HOAST dom (Full a) -> HOAST dom (Full b)) -> HOAST dom (Full b)
- reifyM :: Typeable a => HOAST dom a -> State VarId (AST (Lambda :+: (Variable :+: dom)) a)
- reifyHOAST :: Typeable a => HOAST dom a -> AST (Lambda :+: (Variable :+: dom)) a
- class (SyntacticN a internal, NAry internal (HOLambda dom :+: (Variable :+: dom)), Typeable (NAryEval internal)) => Reifiable a dom internal | a -> dom internal
- reify :: Reifiable a dom internal => a -> ASTF (Lambda :+: (Variable :+: dom)) (NAryEval internal)
Documentation
Variables
evalLambda :: Eval dom => ASTF (Lambda :+: (Variable :+: dom)) a -> aSource
Evaluation of closed Lambda
expressions
Let binding
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
letBind :: (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