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)

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)

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