Language.Syntactic.Features.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

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)

PartialEval dom ctx dom => PartialEval (Variable ctx) ctx dom

evalLambda :: Eval dom => ASTF (Lambda ctx :+: (Variable ctx :+: dom)) a -> a

Evaluation of closed lambda expressions

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

WitnessSat (Let ctxa ctxb)

WitnessCons (Let ctxa ctxb)

ExprEq (Let ctxa ctxb)

ToTree (Let ctxa ctxb)

Render (Let ctxa ctxb)

Eval (Let ctxa ctxb)

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

data HOLambda ctx dom a where

Higher-order lambda binding

Constructors

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

Instances

WitnessCons (HOLambda ctx dom)

type HOAST ctx dom = AST (HOLambda ctx dom :+: (Variable ctx :+: dom))

type HOASTF ctx dom a = HOAST ctx dom (Full a)

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

Lambda binding

lambdaN :: forall ctx dom a. NAry ctx a (HOLambda ctx dom :+: (Variable ctx :+: dom)) => a -> HOASTF ctx dom (NAryEval a)

N-ary lambda binding

letBindCtx :: forall ctxa ctxb dom a b. (Typeable a, Typeable b, (Let ctxa ctxb) :<: dom, Sat ctxa a, Sat ctxb b) => Proxy ctxb -> HOASTF ctxa dom a -> (HOASTF ctxa dom a -> HOASTF ctxa dom b) -> HOASTF ctxa dom b

Let binding with explicit context

letBind :: (Typeable a, Typeable b, (Let Poly Poly) :<: dom) => HOASTF Poly dom a -> (HOASTF Poly dom a -> HOASTF Poly dom b) -> HOASTF Poly dom b

Let binding

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

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

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

class (SyntacticN a internal, NAry ctx internal (HOLambda ctx dom :+: (Variable ctx :+: dom)), Typeable (NAryEval internal)) => Reifiable ctx a dom internal | a -> dom internal

Convenient class alias for n-ary syntactic functions

Instances

(SyntacticN a internal, NAry ctx internal (:+: (HOLambda ctx dom) (:+: (Variable ctx) dom)), Typeable (NAryEval internal)) => Reifiable ctx a dom internal

reifyCtx :: Reifiable ctx a dom internal => Proxy ctx -> a -> ASTF (Lambda ctx :+: (Variable ctx :+: dom)) (NAryEval internal)

Reifying an n-ary syntactic function with explicit context

reify :: Reifiable Poly a dom internal => a -> ASTF (Lambda Poly :+: (Variable Poly :+: dom)) (NAryEval internal)

Reifying an n-ary syntactic function