Language.Syntactic.Constructs.Binding.HigherOrder

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

Documentation

data Variable ctx a

Variables

Instances

MaybeWitnessSat ctx1 (Variable ctx2)

MaybeWitnessSat ctx (Variable ctx)

WitnessSat (Variable ctx)

WitnessCons (Variable ctx)

ExprEq (Variable ctx)

exprEq 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 ctx)

Render (Variable ctx)

EvalBind (Variable ctx)

(:<: (Variable ctx) dom, Optimize dom ctx dom) => Optimize (Variable ctx) ctx dom

(AlphaEq dom dom dom env, VarEqEnv env) => AlphaEq (Variable ctx) (Variable ctx) dom env

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

(:<: (MONAD m) dom, Syntactic a (HODomain ctx dom), Monad m, Typeable1 m, Sat ctx (Internal a)) => Syntactic (Mon ctx dom m a) (HODomain ctx dom)

data Let ctxa ctxb a where

Let binding

A Let expression is really just an application of a lambda binding (the argument (a -> b) is preferably constructed by Lambda).

Constructors

Let :: (Sat ctxa a, Sat ctxb b) => Let ctxa ctxb (a :-> ((a -> b) :-> Full b))

Instances

MaybeWitnessSat ctx (Let ctxa ctxb)

MaybeWitnessSat ctxb (Let ctxa ctxb)

WitnessSat (Let ctxa ctxb)

WitnessCons (Let ctxa ctxb)

ExprEq (Let ctxa ctxb)

ToTree (Let ctxa ctxb)

Render (Let ctxa ctxb)

Eval (Let ctxa ctxb)

EvalBind (Let ctxa ctxb)

(:<: (Let ctxa ctxb) dom, Optimize dom ctx dom) => Optimize (Let ctxa ctxb) ctx dom

AlphaEq dom dom dom env => AlphaEq (Let ctxa ctxb) (Let ctxa ctxb) dom env

data HOLambda ctx dom a where

Higher-order lambda binding

Constructors

HOLambda :: (Typeable a, Typeable b, Sat ctx a) => (ASTF (HODomain ctx dom) a -> ASTF (HODomain ctx dom) b) -> HOLambda ctx dom (Full (a -> b))

Instances

MaybeWitnessSat ctx1 (HOLambda ctx2 dom)

WitnessCons (HOLambda ctx dom)

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

(:<: (MONAD m) dom, Syntactic a (HODomain ctx dom), Monad m, Typeable1 m, Sat ctx (Internal a)) => Syntactic (Mon ctx dom m a) (HODomain ctx dom)

type HODomain ctx dom = HOLambda ctx dom :+: (Variable ctx :+: dom)

lambda :: (Typeable a, Typeable b, Sat ctx a) => (ASTF (HODomain ctx dom) a -> ASTF (HODomain ctx dom) b) -> ASTF (HODomain ctx dom) (a -> b)

Lambda binding

reifyM :: forall ctx dom a. Typeable a => AST (HODomain ctx dom) a -> State VarId (AST (Lambda ctx :+: (Variable ctx :+: dom)) a)

reifyTop :: Typeable a => AST (HODomain ctx dom) a -> AST (Lambda ctx :+: (Variable ctx :+: dom)) a

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

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

Reifying an n-ary syntactic function