Language.Syntactic.Functional

Basics for implementing functional EDSLs

Syntactic constructs

newtype Name

Variable name

Constructors

Name Integer

Instances

Enum Name

Methods

succ :: Name -> Name

pred :: Name -> Name

toEnum :: Int -> Name

fromEnum :: Name -> Int

enumFrom :: Name -> [Name]

enumFromThen :: Name -> Name -> [Name]

enumFromTo :: Name -> Name -> [Name]

enumFromThenTo :: Name -> Name -> Name -> [Name]

Eq Name

Methods

(==) :: Name -> Name -> Bool

(/=) :: Name -> Name -> Bool

Integral Name

Methods

quot :: Name -> Name -> Name

rem :: Name -> Name -> Name

div :: Name -> Name -> Name

mod :: Name -> Name -> Name

quotRem :: Name -> Name -> (Name, Name)

divMod :: Name -> Name -> (Name, Name)

toInteger :: Name -> Integer

Num Name

Methods

(+) :: Name -> Name -> Name

(-) :: Name -> Name -> Name

(*) :: Name -> Name -> Name

negate :: Name -> Name

abs :: Name -> Name

signum :: Name -> Name

fromInteger :: Integer -> Name

Ord Name

Methods

compare :: Name -> Name -> Ordering

(<) :: Name -> Name -> Bool

(<=) :: Name -> Name -> Bool

(>) :: Name -> Name -> Bool

(>=) :: Name -> Name -> Bool

max :: Name -> Name -> Name

min :: Name -> Name -> Name

Real Name

Methods

toRational :: Name -> Rational

Show Name

Methods

showsPrec :: Int -> Name -> ShowS

show :: Name -> String

showList :: [Name] -> ShowS

NFData Name

Methods

rnf :: Name -> ()

EvalEnv BindingT RunEnv

Methods

compileSym :: proxy RunEnv -> BindingT sig -> DenotationM (Reader RunEnv) sig

data Literal sig where

Literal

Constructors

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

Instances

Symbol Literal

Methods

symSig :: Literal sig -> SigRep sig

StringTree Literal

Methods

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

Render Literal

Methods

renderSym :: Literal sig -> String

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

Equality Literal

Methods

equal :: Literal a -> Literal b -> Bool

hash :: Literal a -> Hash

Eval Literal

Methods

evalSym :: Literal sig -> Denotation sig

EvalEnv Literal env

Methods

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

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

Methods

symSig :: Construct sig -> SigRep sig

StringTree Construct

Methods

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

Render Construct

Methods

renderSym :: Construct sig -> String

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

Equality Construct

Methods

equal :: Construct a -> Construct b -> Bool

hash :: Construct a -> Hash

Eval Construct

Methods

evalSym :: Construct sig -> Denotation sig

EvalEnv Construct env

Methods

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

data Binding sig where

Variables and binders

Constructors

Var :: Name -> Binding (Full a)

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

Instances

NFData1 Binding

Methods

liftRnf :: (a -> ()) -> Binding a -> ()

Symbol Binding

Methods

symSig :: Binding sig -> SigRep sig

StringTree Binding

Methods

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

Render Binding

Methods

renderSym :: Binding sig -> String

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

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

Methods

equal :: Binding a -> Binding b -> Bool

hash :: Binding a -> Hash

BindingDomain Binding

Methods

prVar :: Binding sig -> Maybe Name

prLam :: Binding sig -> Maybe Name

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

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

Methods

liftRnf :: (a -> ()) -> BindingT a -> ()

Symbol BindingT

Methods

symSig :: BindingT sig -> SigRep sig

StringTree BindingT

Methods

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

Render BindingT

Methods

renderSym :: BindingT sig -> String

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

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

Methods

equal :: BindingT a -> BindingT b -> Bool

hash :: BindingT a -> Hash

BindingDomain BindingT

Methods

prVar :: BindingT sig -> Maybe Name

prLam :: BindingT sig -> Maybe Name

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

EvalEnv BindingT RunEnv

Methods

compileSym :: proxy RunEnv -> BindingT sig -> DenotationM (Reader RunEnv) sig

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

Minimal complete definition

prVar, prLam, renameBind

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

Methods

prVar :: sym sig -> Maybe Name

prLam :: sym sig -> Maybe Name

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

BindingDomain BindingT

Methods

prVar :: BindingT sig -> Maybe Name

prLam :: BindingT sig -> Maybe Name

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

BindingDomain Binding

Methods

prVar :: Binding sig -> Maybe Name

prLam :: Binding sig -> Maybe Name

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

BindingDomain sym => BindingDomain (Typed sym)

Methods

prVar :: Typed sym sig -> Maybe Name

prLam :: Typed sym sig -> Maybe Name

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

BindingDomain sym => BindingDomain (AST sym)

Methods

prVar :: AST sym sig -> Maybe Name

prLam :: AST sym sig -> Maybe Name

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

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

Methods

prVar :: (sym1 :+: sym2) sig -> Maybe Name

prLam :: (sym1 :+: sym2) sig -> Maybe Name

renameBind :: (Name -> Name) -> (sym1 :+: sym2) sig -> (sym1 :+: sym2) sig

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

Methods

prVar :: (sym :&: i) sig -> Maybe Name

prLam :: (sym :&: i) sig -> Maybe Name

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

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

Methods

symSig :: Let sig -> SigRep sig

StringTree Let

Methods

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

Render Let

Methods

renderSym :: Let sig -> String

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

Equality Let

Methods

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

hash :: Let a -> Hash

Eval Let

Methods

evalSym :: Let sig -> Denotation sig

EvalEnv Let env

Methods

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

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)

Methods

symSig :: MONAD m sig -> SigRep sig

StringTree (MONAD m)

Methods

stringTreeSym :: [Tree String] -> MONAD m a -> Tree String

Render (MONAD m)

Methods

renderSym :: MONAD m sig -> String

renderArgs :: [String] -> MONAD m sig -> String

Equality (MONAD m)

Methods

equal :: MONAD m a -> MONAD m b -> Bool

hash :: MONAD m a -> Hash

Monad m => Eval (MONAD m)

Methods

evalSym :: MONAD m sig -> Denotation sig

Monad m => EvalEnv (MONAD m) env

Methods

compileSym :: proxy env -> MONAD m sig -> DenotationM (Reader env) sig

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 :: {..} -> Remon sym m a

Fields

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

Instances

Monad (Remon dom m)

Methods

(>>=) :: Remon dom m a -> (a -> Remon dom m b) -> Remon dom m b

(>>) :: Remon dom m a -> Remon dom m b -> Remon dom m b

return :: a -> Remon dom m a

fail :: String -> Remon dom m a

Functor (Remon sym m)

Methods

fmap :: (a -> b) -> Remon sym m a -> Remon sym m b

(<$) :: a -> Remon sym m b -> Remon sym m a

Applicative (Remon sym m)

Methods

pure :: a -> Remon sym m a

(<*>) :: Remon sym m (a -> b) -> Remon sym m a -> Remon sym m b

(*>) :: Remon sym m a -> Remon sym m b -> Remon sym m b

(<*) :: Remon sym m a -> Remon sym m b -> Remon sym m a

type Domain (Remon sym m a)

type Domain (Remon sym m a) = sym

type Domain (Remon sym m a)

type Domain (Remon sym m a) = sym

type Internal (Remon sym m a)

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

type Internal (Remon sym m 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)

type Denotation (Full a) = a

type Denotation ((:->) a sig)

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

class Eval s where

Minimal complete definition

evalSym

Methods

evalSym :: s sig -> Denotation sig

Instances

Eval Empty

Methods

evalSym :: Empty sig -> Denotation sig

Eval Let

Methods

evalSym :: Let sig -> Denotation sig

Eval Construct

Methods

evalSym :: Construct sig -> Denotation sig

Eval Literal

Methods

evalSym :: Literal sig -> Denotation sig

Eval BindingWS

Methods

evalSym :: BindingWS sig -> Denotation sig

Eval Tuple

Methods

evalSym :: Tuple sig -> Denotation sig

Monad m => Eval (MONAD m)

Methods

evalSym :: MONAD m sig -> Denotation sig

Eval sym => Eval (ReaderSym sym)

Methods

evalSym :: ReaderSym sym sig -> Denotation sig

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

Methods

evalSym :: (s :+: t) sig -> Denotation sig

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

Methods

evalSym :: (sym :&: info) sig -> Denotation sig

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)

type DenotationM m (Full a) = m a

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

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

Methods

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

compileSym :: (Symbol sym, Eval sym) => proxy env -> sym sig -> DenotationM (Reader env) sig

Instances

EvalEnv Empty env

Methods

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

EvalEnv Let env

Methods

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

EvalEnv BindingT RunEnv

Methods

compileSym :: proxy RunEnv -> BindingT sig -> DenotationM (Reader RunEnv) sig

EvalEnv Construct env

Methods

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

EvalEnv Literal env

Methods

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

EvalEnv Tuple env

Methods

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

EvalEnv sym env => EvalEnv (Typed sym) env

Methods

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

Monad m => EvalEnv (MONAD m) env

Methods

compileSym :: proxy env -> MONAD m sig -> DenotationM (Reader env) sig

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

Methods

compileSym :: proxy env -> (sym1 :+: sym2) sig -> DenotationM (Reader env) sig

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

Methods

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

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.)