Language.Syntactic.Constructs.Binding.HigherOrder

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.

Documentation

data Variable a

Variables

Instances

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

(Constrained (HODomain dom p), Sat (HODomain dom p) (Internal (a -> b)), Syntactic a (HODomain dom p), Syntactic b (HODomain dom p), p (Internal a), p (Internal a -> Internal b)) => Syntactic (a -> b) (HODomain dom p)

(Constrained (HODomain dom Typeable), Sat (HODomain dom Typeable) (Internal (Mon dom m a)), Syntactic a (HODomain dom Typeable), InjectC (MONAD m) dom (m (Internal a)), Monad m, Typeable1 m, Typeable (Internal a)) => Syntactic (Mon dom m a) (HODomain dom Typeable)

data Let a where

Let binding

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

Constructors

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

Instances

Equality Let

ToTree Let

Render Let

Eval Let

Constrained Let

EvalBind Let

Optimize Let

AlphaEq dom dom dom env => AlphaEq Let Let dom env

data HOLambda dom p a where

Higher-order lambda binding

Constructors

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

Instances

Constrained (HOLambda dom p)

(Constrained (HODomain dom p), Sat (HODomain dom p) (Internal (a -> b)), Syntactic a (HODomain dom p), Syntactic b (HODomain dom p), p (Internal a), p (Internal a -> Internal b)) => Syntactic (a -> b) (HODomain dom p)

(Constrained (HODomain dom Typeable), Sat (HODomain dom Typeable) (Internal (Mon dom m a)), Syntactic a (HODomain dom Typeable), InjectC (MONAD m) dom (m (Internal a)), Monad m, Typeable1 m, Typeable (Internal a)) => Syntactic (Mon dom m a) (HODomain dom Typeable)

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

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

Lambda binding

reifyM :: AST (HODomain dom p) a -> State VarId (AST ((Lambda :+: (Variable :+: dom)) :|| p) a)

reifyTop :: AST (HODomain dom p) a -> AST ((Lambda :+: (Variable :+: dom)) :|| p) a

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

reify :: Syntactic a (HODomain dom p) => a -> ASTF ((Lambda :+: (Variable :+: dom)) :|| p) (Internal a)

Reify an n-ary syntactic function