Language.Syntactic.Features.Binding

General binding constructs

Variables

newtype VarId

Variable identifier

Constructors

VarId

Fields

varInteger :: Integer

Instances

Enum VarId

Eq VarId

Integral VarId

Num VarId

Ord VarId

Real VarId

Show VarId

Ix VarId

showVar :: VarId -> String

data Variable ctx a where

Variables

Constructors

Variable :: (Typeable a, Sat ctx a) => VarId -> Variable ctx (Full a)

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

prjVariable :: (Variable ctx) :<: sup => Proxy ctx -> sup a -> Maybe (Variable ctx a)

Partial Variable projection with explicit context

Lambda binding

data Lambda ctx a where

Lambda binding

Constructors

Lambda :: (Typeable a, Sat ctx a) => VarId -> Lambda ctx (b :-> Full (a -> b))

Instances

WitnessCons (Lambda ctx)

ExprEq (Lambda ctx)

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

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

alphaEq a b  ==>  exprHash a == exprHash b

ToTree (Lambda ctx)

Render (Lambda ctx)

PartialEval dom ctx dom => PartialEval (Lambda ctx) ctx dom

prjLambda :: (Lambda ctx) :<: sup => Proxy ctx -> sup a -> Maybe (Lambda ctx a)

Partial Lambda projection with explicit context

class NAry ctx a dom | a -> dom where

The class of n-ary binding functions

Associated Types

type NAryEval a

Methods

bindN :: Proxy ctx -> (forall b c. (Typeable b, Typeable c, Sat ctx b) => (ASTF dom b -> ASTF dom c) -> ASTF dom (b -> c)) -> a -> ASTF dom (NAryEval a)

N-ary binding by nested use of the supplied binder

Instances

(Typeable a, Sat ctx a, NAry ctx b dom, Typeable (NAryEval b)) => NAry ctx (ASTF dom a -> b) dom

Sat ctx a => NAry ctx (ASTF dom a) dom

Let binding

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

prjLet :: (Let ctxa ctxb) :<: sup => Proxy ctxa -> Proxy ctxb -> sup a -> Maybe (Let ctxa ctxb a)

Partial Let projection with explicit context

Interpretation

alphaEqM :: ((Lambda ctx) :<: dom, (Variable ctx) :<: dom) => Proxy ctx -> (forall a b. AST dom a -> AST dom b -> Reader [(VarId, VarId)] Bool) -> forall a b. AST dom a -> AST dom b -> Reader [(VarId, VarId)] Bool

Alpha equivalence in an environment of variable equivalences. The supplied equivalence function gets called when the argument expressions are not both Variables, both Lambdas or both :$:.

alphaEq :: ((Lambda ctx) :<: dom, (Variable ctx) :<: dom, ExprEq dom) => Proxy ctx -> AST dom a -> AST dom b -> Bool

Alpha-equivalence on lambda expressions. Free variables are taken to be equivalent if they have the same identifier.

evalLambdaM :: (Eval dom, MonadReader [(VarId, Dynamic)] m) => ASTF (Lambda ctx :+: (Variable ctx :+: dom)) a -> m a

Evaluation of possibly open lambda expressions

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

Evaluation of closed lambda expressions