Language.Syntactic.Functional

Basics for implementing functional EDSLs

Syntactic constructs

newtype Name

Variable name

Constructors

Name Integer

Instances

Enum Name

Eq Name

Integral Name

Num Name

Ord Name

Real Name

Show Name

NFData Name

EvalEnv BindingT RunEnv

data Literal sig where

Literal

Constructors

Literal :: Show a => a -> Literal (Full a)

Instances

Symbol Literal

StringTree Literal

Render Literal

Equality Literal

Eval Literal

EvalEnv Literal env

data Construct sig where

Generic N-ary syntactic construct

Construct gives a quick way to introduce a syntactic construct by giving its name and semantic function.

Constructors

Construct :: Signature sig => String -> Denotation sig -> Construct sig

Instances

Symbol Construct

StringTree Construct

Render Construct

Equality Construct

Eval Construct

EvalEnv Construct env

data Binding sig where

Variables and binders

Constructors

Var :: Name -> Binding (Full a)

Lam :: Name -> Binding (b :-> Full (a -> b))

Instances

NFData1 Binding

Symbol Binding

StringTree Binding

Render Binding

Equality Binding

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

hash assigns the same hash to all variables and binders. This is a valid over-approximation that enables the following property:

alphaEq a b ==> hash a == hash b

BindingDomain Binding

maxLam :: Project Binding s => AST s a -> Name

Get the highest name bound by the first Lam binders at every path from the root. If the term has ordered binders [1], maxLam returns the highest name introduced in the whole term.

[1] Ordered binders means that the names of Lam nodes are decreasing along every path from the root.

lam_template

Arguments

:: Project Binding sym

=> (Name -> sym (Full a))

Variable symbol constructor

-> (Name -> ASTF sym b -> ASTF sym (a -> b))

Lambda constructor

-> (ASTF sym a -> ASTF sym b)

-> ASTF sym (a -> b)

Higher-order interface for variable binding for domains based on Binding

Assumptions:

• The body f does not inspect its argument.
• Applying f to a term with ordered binders results in a term with ordered binders [1].

[1] Ordered binders means that the names of Lam nodes are decreasing along every path from the root.

See "Using Circular Programs for Higher-Order Syntax" (ICFP 2013, http://www.cse.chalmers.se/~emax/documents/axelsson2013using.pdf).

lam :: Binding :<: sym => (ASTF sym a -> ASTF sym b) -> ASTF sym (a -> b)

Higher-order interface for variable binding

This function is lamT_template specialized to domains sym satisfying (Binding :<: sym).

fromDeBruijn :: Binding :<: sym => ASTF sym a -> ASTF sym a

Convert from a term with De Bruijn indexes to one with explicit names

In the argument term, variable Names are treated as De Bruijn indexes, and lambda Names are ignored. (Ideally, one should use a different type for De Bruijn terms.)

data BindingT sig where

Typed variables and binders

Constructors

VarT :: Typeable a => Name -> BindingT (Full a)

LamT :: Typeable a => Name -> BindingT (b :-> Full (a -> b))

Instances

NFData1 BindingT

Symbol BindingT

StringTree BindingT

Render BindingT

Equality BindingT

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

hash assigns the same hash to all variables and binders. This is a valid over-approximation that enables the following property:

alphaEq a b ==> hash a == hash b

BindingDomain BindingT

EvalEnv BindingT RunEnv

maxLamT :: Project BindingT sym => AST sym a -> Name

Get the highest name bound by the first LamT binders at every path from the root. If the term has ordered binders [1], maxLamT returns the highest name introduced in the whole term.

[1] Ordered binders means that the names of LamT nodes are decreasing along every path from the root.

lamT_template

Arguments

:: Project BindingT sym

=> (Name -> sym (Full a))

Variable symbol constructor

-> (Name -> ASTF sym b -> ASTF sym (a -> b))

Lambda constructor

-> (ASTF sym a -> ASTF sym b)

-> ASTF sym (a -> b)

Higher-order interface for variable binding

Assumptions:

• The body f does not inspect its argument.
• Applying f to a term with ordered binders results in a term with ordered binders [1].

[1] Ordered binders means that the names of LamT nodes are decreasing along every path from the root.

See "Using Circular Programs for Higher-Order Syntax" (ICFP 2013, http://www.cse.chalmers.se/~emax/documents/axelsson2013using.pdf).

lamT :: (BindingT :<: sym, Typeable a) => (ASTF sym a -> ASTF sym b) -> ASTF sym (a -> b)

Higher-order interface for variable binding

This function is lamT_template specialized to domains sym satisfying (BindingT :<: sym).

lamTyped :: (sym ~ Typed s, BindingT :<: s, Typeable a, Typeable b) => (ASTF sym a -> ASTF sym b) -> ASTF sym (a -> b)

Higher-order interface for variable binding

This function is lamT_template specialized to domains sym satisfying (sym ~ Typed s, BindingT :<: s).

class BindingDomain sym where

Domains that "might" include variables and binders

Methods

prVar :: sym sig -> Maybe Name

prLam :: sym sig -> Maybe Name

renameBind :: (Name -> Name) -> sym sig -> sym sig

Rename a variable or a lambda (no effect for other symbols)

Instances

BindingDomain sym

BindingDomain BindingT

BindingDomain Binding

BindingDomain sym => BindingDomain (Typed sym)

BindingDomain sym => BindingDomain (AST sym)

(BindingDomain sym1, BindingDomain sym2) => BindingDomain ((:+:) sym1 sym2)

BindingDomain sym => BindingDomain ((:&:) sym i)

data Let sig where

A symbol for let bindings

This symbol is just an application operator. The actual binding has to be done by a lambda that constructs the second argument.

The provided string is just a tag and has nothing to do with the name of the variable of the second argument (if that argument happens to be a lambda). However, a back end may use the tag to give a sensible name to the generated variable.

The string tag may be empty.

Constructors

Let :: String -> Let (a :-> ((a -> b) :-> Full b))

Instances

Symbol Let

StringTree Let

Render Let

Equality Let

Eval Let

EvalEnv Let env

data MONAD m sig where

Monadic constructs

See "Generic Monadic Constructs for Embedded Languages" (Persson et al., IFL 2011 http://www.cse.chalmers.se/~emax/documents/persson2011generic.pdf).

Constructors

Return :: MONAD m (a :-> Full (m a))

Bind :: MONAD m (m a :-> ((a -> m b) :-> Full (m b)))

Instances

Symbol (MONAD m)

StringTree (MONAD m)

Render (MONAD m)

Equality (MONAD m)

Monad m => Eval (MONAD m)

Monad m => EvalEnv (MONAD m) env

newtype Remon sym m a where

Reifiable monad

See "Generic Monadic Constructs for Embedded Languages" (Persson et al., IFL 2011 http://www.cse.chalmers.se/~emax/documents/persson2011generic.pdf).

It is advised to convert to/from Remon using the Syntactic instance provided in the modules Language.Syntactic.Sugar.Monad or Language.Syntactic.Sugar.MonadT.

Constructors

Remon :: (forall r. Typeable r => Cont (ASTF sym (m r)) a) -> Remon sym m a

Fields

unRemon :: forall r. Typeable r => Cont (ASTF sym (m r)) a

Instances

Monad (Remon dom m)

Functor (Remon sym m)

Applicative (Remon sym m)

type Domain (Remon sym m a) = sym

type Domain (Remon sym m a) = sym

type Internal (Remon sym m a) = m (Internal a)

type Internal (Remon sym m a) = m (Internal a)

desugarMonad :: (MONAD m :<: sym, Typeable a, Typeable m) => Remon sym m (ASTF sym a) -> ASTF sym (m a)

One-layer desugaring of monadic actions

desugarMonadTyped :: (MONAD m :<: s, sym ~ Typed s, Typeable a, Typeable m) => Remon sym m (ASTF sym a) -> ASTF sym (m a)

One-layer desugaring of monadic actions

Free and bound variables

freeVars :: BindingDomain sym => AST sym sig -> Set Name

Get the set of free variables in an expression

allVars :: BindingDomain sym => AST sym sig -> Set Name

Get the set of variables (free, bound and introduced by lambdas) in an expression

renameUnique' :: forall sym a. BindingDomain sym => [Name] -> ASTF sym a -> ASTF sym a

Rename the bound variables in a term

The free variables are left untouched. The bound variables are given unique names using as small names as possible. The first argument is a list of reserved names. Reserved names and names of free variables are not used when renaming bound variables.

renameUnique :: BindingDomain sym => ASTF sym a -> ASTF sym a

Rename the bound variables in a term

The free variables are left untouched. The bound variables are given unique names using as small names as possible. Names of free variables are not used when renaming bound variables.

Alpha-equivalence

type AlphaEnv = [(Name, Name)]

Environment used by alphaEq'

alphaEq' :: (Equality sym, BindingDomain sym) => AlphaEnv -> ASTF sym a -> ASTF sym b -> Bool

alphaEq :: (Equality sym, BindingDomain sym) => ASTF sym a -> ASTF sym b -> Bool

Alpha-equivalence

Evaluation

type family Denotation sig

Semantic function type of the given symbol signature

Instances

type Denotation (Full a) = a

type Denotation ((:->) a sig) = a -> Denotation sig

class Eval s where

Methods

evalSym :: s sig -> Denotation sig

Instances

Eval Empty

Eval Let

Eval Construct

Eval Literal

Eval BindingWS

Eval Tuple

Monad m => Eval (MONAD m)

Eval sym => Eval (ReaderSym sym)

(Eval s, Eval t) => Eval ((:+:) s t)

Eval sym => Eval ((:&:) sym info)

evalDen :: Eval s => AST s sig -> Denotation sig

Evaluation

type family DenotationM m sig

Monadic denotation; mapping from a symbol signature

a :-> b :-> Full c

to

m a -> m b -> m c

Instances

type DenotationM m (Full a) = m a

type DenotationM m ((:->) a sig) = m a -> DenotationM m sig

liftDenotationM :: forall m sig proxy1 proxy2. Monad m => SigRep sig -> proxy1 m -> proxy2 sig -> Denotation sig -> DenotationM m sig

Lift a Denotation to DenotationM

type RunEnv = [(Name, Dynamic)]

Runtime environment

class EvalEnv sym env where

Evaluation

Minimal complete definition

Nothing

Methods

compileSym :: proxy env -> sym sig -> DenotationM (Reader env) sig

Instances

EvalEnv Empty env

EvalEnv Let env

EvalEnv BindingT RunEnv

EvalEnv Construct env

EvalEnv Literal env

EvalEnv Tuple env

EvalEnv sym env => EvalEnv (Typed sym) env

Monad m => EvalEnv (MONAD m) env

(EvalEnv sym1 env, EvalEnv sym2 env) => EvalEnv ((:+:) sym1 sym2) env

EvalEnv sym env => EvalEnv ((:&:) sym info) env

compileSymDefault :: forall proxy env sym sig. Eval sym => SigRep sig -> proxy env -> sym sig -> DenotationM (Reader env) sig

Simple implementation of compileSym from a Denotation

evalOpen :: EvalEnv sym env => env -> ASTF sym a -> a

Evaluation of open terms

evalClosed :: EvalEnv sym RunEnv => ASTF sym a -> a

Evaluation of closed terms where RunEnv is used as the internal environment

(Note that there is no guarantee that the term is actually closed.)