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

Safe HaskellNone



This module provides binding constructs using higher-order syntax and a function (reify) for translating to first-order syntax. Expressions constructed using the exported interface (specifically, not introducing Variables explicitly) are guaranteed to have well-behaved translation.



data Variable a Source



Equality Variable

equal does strict identifier comparison; i.e. no alpha equivalence.

exprHash assigns the same hash to all variables. This is a valid over-approximation that enables the following property:

alphaEq a b  ==>  exprHash a == exprHash b
ToTree Variable 
Render Variable 
Constrained Variable 
EvalBind Variable 
Optimize Variable 
(AlphaEq dom dom dom env, VarEqEnv env) => AlphaEq Variable Variable dom env 

data Let a whereSource

Let binding

Let is just an application operator with flipped argument order. The argument (a -> b) is preferably constructed by Lambda.


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


data HOLambda dom p pVar a whereSource

Higher-order lambda binding


HOLambda :: (p a, pVar a) => (ASTF (HODomain dom p pVar) a -> ASTF (HODomain dom p pVar) b) -> HOLambda dom p pVar (Full (a -> b)) 

type HODomain dom p pVar = (HOLambda dom p pVar :+: ((Variable :|| pVar) :+: dom)) :|| pSource

Adding support for higher-order abstract syntax to a domain

type FODomain dom p pVar = (CLambda pVar :+: ((Variable :|| pVar) :+: dom)) :|| pSource

Equivalent to HODomain (including type constraints), but using a first-order representation of binding

type CLambda pVar = SubConstr2 (->) Lambda pVar TopSource

Lambda with a constraint on the bound variable type

lambda :: (p (a -> b), p a, pVar a) => (ASTF (HODomain dom p pVar) a -> ASTF (HODomain dom p pVar) b) -> ASTF (HODomain dom p pVar) (a -> b)Source

Lambda binding

reifyM :: forall dom p pVar a. AST (HODomain dom p pVar) a -> State VarId (AST (FODomain dom p pVar) a)Source

reifyTop :: AST (HODomain dom p pVar) a -> AST (FODomain dom p pVar) aSource

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

reify :: (Syntactic a, Domain a ~ HODomain dom p pVar) => a -> ASTF (FODomain dom p pVar) (Internal a)Source

Reify an n-ary syntactic function