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

StringTree Variable

Defined in Language.Syntactic.Constructs.Binding

Methods

stringTreeSym :: [Tree String] -> Variable a -> Tree String

Render Variable

Defined in Language.Syntactic.Constructs.Binding

Methods

renderSym :: Variable sig -> String

renderArgs :: [String] -> Variable sig -> String

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

Defined in Language.Syntactic.Constructs.Binding

Methods

equal :: Variable a -> Variable b -> Bool

exprHash :: Variable a -> Hash

Constrained Variable

Defined in Language.Syntactic.Constructs.Binding

Associated Types

type Sat Variable :: * -> Constraint

Methods

exprDict :: Variable a -> Dict (Sat Variable (DenResult a))

EvalBind Variable

Defined in Language.Syntactic.Constructs.Binding

Methods

evalBindSym :: (EvalBind dom, ConstrainedBy dom Typeable, Typeable (DenResult sig)) => Variable sig -> Args (AST dom) sig -> Reader [(VarId, Dynamic)] (DenResult sig)

Optimize Variable

Defined in Language.Syntactic.Constructs.Binding.Optimize

Methods

optimizeSym :: Optimize' dom => ConstFolder dom -> (Variable sig -> AST dom sig) -> Variable sig -> Args (AST dom) sig -> Writer (Set VarId) (ASTF dom (DenResult sig))

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

Defined in Language.Syntactic.Constructs.Binding

Methods

alphaEqSym :: Variable a -> Args (AST dom) a -> Variable b -> Args (AST dom) b -> Reader env Bool

IsHODomain (HODomain dom p pVar) p pVar

Defined in Language.Syntactic.Constructs.Binding.HigherOrder

Methods

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

type Sat Variable

Defined in Language.Syntactic.Constructs.Binding

type Sat Variable = Top

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

StringTree Let

Defined in Language.Syntactic.Constructs.Binding

Methods

stringTreeSym :: [Tree String] -> Let a -> Tree String

Render Let

Defined in Language.Syntactic.Constructs.Binding

Methods

renderSym :: Let sig -> String

renderArgs :: [String] -> Let sig -> String

Eval Let

Defined in Language.Syntactic.Constructs.Binding

Methods

evaluate :: Let a -> Denotation a

Equality Let

Defined in Language.Syntactic.Constructs.Binding

Methods

equal :: Let a -> Let b -> Bool

exprHash :: Let a -> Hash

Constrained Let

Defined in Language.Syntactic.Constructs.Binding

Associated Types

type Sat Let :: * -> Constraint

Methods

exprDict :: Let a -> Dict (Sat Let (DenResult a))

EvalBind Let

Defined in Language.Syntactic.Constructs.Binding

Methods

evalBindSym :: (EvalBind dom, ConstrainedBy dom Typeable, Typeable (DenResult sig)) => Let sig -> Args (AST dom) sig -> Reader [(VarId, Dynamic)] (DenResult sig)

Optimize Let

Defined in Language.Syntactic.Constructs.Binding.Optimize

Methods

optimizeSym :: Optimize' dom => ConstFolder dom -> (Let sig -> AST dom sig) -> Let sig -> Args (AST dom) sig -> Writer (Set VarId) (ASTF dom (DenResult sig))

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

Defined in Language.Syntactic.Constructs.Binding

Methods

alphaEqSym :: Let a -> Args (AST dom) a -> Let b -> Args (AST dom) b -> Reader env Bool

type Sat Let

Defined in Language.Syntactic.Constructs.Binding

type Sat Let = Top

data HOLambda dom p pVar a where

Higher-order lambda binding

Constructors

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

Instances

IsHODomain (HODomain dom p pVar) p pVar

Defined in Language.Syntactic.Constructs.Binding.HigherOrder

Methods

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

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

Adding support for higher-order abstract syntax to a domain

type FODomain dom p pVar = (CLambda pVar :+: ((Variable :|| pVar) :+: dom)) :|| p

Equivalent to HODomain (including type constraints), but using a first-order representation of binding

type CLambda pVar = SubConstr2 (->) Lambda pVar Top

Lambda with a constraint on the bound variable type

class IsHODomain dom p pVar | dom -> p pVar where

An abstraction of HODomain

Minimal complete definition

lambda

Methods

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

Instances

IsHODomain (HODomain dom p pVar) p pVar

Defined in Language.Syntactic.Constructs.Binding.HigherOrder

Methods

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

reifyM :: forall dom p pVar m a. MonadState VarId m => AST (HODomain dom p pVar) a -> m (AST (FODomain dom p pVar) a)

reifyTop :: AST (HODomain dom p pVar) a -> AST (FODomain dom p pVar) a

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

reify :: (Syntactic a, Domain a ~ HODomain dom p pVar) => a -> ASTF (FODomain dom p pVar) (Internal a)

Reify an n-ary syntactic function

Orphan instances

(Syntactic a, Domain a ~ dom, Syntactic b, Domain b ~ dom, IsHODomain dom p pVar, p (Internal a -> Internal b), p (Internal a), pVar (Internal a)) => Syntactic (a -> b)

Associated Types

type Domain (a -> b) :: * -> *

type Internal (a -> b) :: *

Methods

desugar :: (a -> b) -> ASTF (Domain (a -> b)) (Internal (a -> b))

sugar :: ASTF (Domain (a -> b)) (Internal (a -> b)) -> a -> b