Language.Syntactic.Functional

Basics for implementing functional EDSLs

Syntactic constructs

newtype Name

Variable name

Constructors

Name Integer

Instances

Enum Name

Defined in Language.Syntactic.Functional

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

Defined in Language.Syntactic.Functional

Methods

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

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

Integral Name

Defined in Language.Syntactic.Functional

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

Defined in Language.Syntactic.Functional

Methods

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

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

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

negate :: Name -> Name

abs :: Name -> Name

signum :: Name -> Name

fromInteger :: Integer -> Name

Ord Name

Defined in Language.Syntactic.Functional

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

Defined in Language.Syntactic.Functional

Methods

toRational :: Name -> Rational

Show Name

Defined in Language.Syntactic.Functional

Methods

showsPrec :: Int -> Name -> ShowS

show :: Name -> String

showList :: [Name] -> ShowS

NFData Name

Defined in Language.Syntactic.Functional

Methods

rnf :: Name -> ()

EvalEnv BindingT RunEnv

Defined in Language.Syntactic.Functional

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

Defined in Language.Syntactic.Functional

Methods

symSig :: Literal sig -> SigRep sig

StringTree Literal

Defined in Language.Syntactic.Functional

Methods

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

Render Literal

Defined in Language.Syntactic.Functional

Methods

renderSym :: Literal sig -> String

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

Equality Literal

Defined in Language.Syntactic.Functional

Methods

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

hash :: Literal a -> Hash

Eval Literal

Defined in Language.Syntactic.Functional

Methods

evalSym :: Literal sig -> Denotation sig

EvalEnv Literal env

Defined in Language.Syntactic.Functional

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

Defined in Language.Syntactic.Functional

Methods

symSig :: Construct sig -> SigRep sig

StringTree Construct

Defined in Language.Syntactic.Functional

Methods

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

Render Construct

Defined in Language.Syntactic.Functional

Methods

renderSym :: Construct sig -> String

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

Equality Construct

Defined in Language.Syntactic.Functional

Methods

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

hash :: Construct a -> Hash

Eval Construct

Defined in Language.Syntactic.Functional

Methods

evalSym :: Construct sig -> Denotation sig

EvalEnv Construct env

Defined in Language.Syntactic.Functional

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

Defined in Language.Syntactic.Functional

Methods

rnf1 :: Binding a -> ()

Symbol Binding

Defined in Language.Syntactic.Functional

Methods

symSig :: Binding sig -> SigRep sig

StringTree Binding

Defined in Language.Syntactic.Functional

Methods

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

Render Binding

Defined in Language.Syntactic.Functional

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

Defined in Language.Syntactic.Functional

Methods

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

hash :: Binding a -> Hash

BindingDomain Binding

Defined in Language.Syntactic.Functional

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, https://emilaxelsson.github.io/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

Defined in Language.Syntactic.Functional

Methods

rnf1 :: BindingT a -> ()

Symbol BindingT

Defined in Language.Syntactic.Functional

Methods

symSig :: BindingT sig -> SigRep sig

StringTree BindingT

Defined in Language.Syntactic.Functional

Methods

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

Render BindingT

Defined in Language.Syntactic.Functional

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

Defined in Language.Syntactic.Functional

Methods

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

hash :: BindingT a -> Hash

BindingDomain BindingT

Defined in Language.Syntactic.Functional

Methods

prVar :: BindingT sig -> Maybe Name

prLam :: BindingT sig -> Maybe Name

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

EvalEnv BindingT RunEnv

Defined in Language.Syntactic.Functional

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, https://emilaxelsson.github.io/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

Defined in Language.Syntactic.Functional

Methods

prVar :: sym sig -> Maybe Name

prLam :: sym sig -> Maybe Name

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

BindingDomain BindingT

Defined in Language.Syntactic.Functional

Methods

prVar :: BindingT sig -> Maybe Name

prLam :: BindingT sig -> Maybe Name

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

BindingDomain Binding

Defined in Language.Syntactic.Functional

Methods

prVar :: Binding sig -> Maybe Name

prLam :: Binding sig -> Maybe Name

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

BindingDomain sym => BindingDomain (Typed sym)

Defined in Language.Syntactic.Functional

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)

Defined in Language.Syntactic.Functional

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)

Defined in Language.Syntactic.Functional

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)

Defined in Language.Syntactic.Functional

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

Defined in Language.Syntactic.Functional

Methods

symSig :: Let sig -> SigRep sig

StringTree Let

Defined in Language.Syntactic.Functional

Methods

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

Render Let

Defined in Language.Syntactic.Functional

Methods

renderSym :: Let sig -> String

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

Equality Let

Defined in Language.Syntactic.Functional

Methods

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

hash :: Let a -> Hash

Eval Let

Defined in Language.Syntactic.Functional

Methods

evalSym :: Let sig -> Denotation sig

EvalEnv Let env

Defined in Language.Syntactic.Functional

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 https://emilaxelsson.github.io/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)

Defined in Language.Syntactic.Functional

Methods

symSig :: MONAD m sig -> SigRep sig

StringTree (MONAD m)

Defined in Language.Syntactic.Functional

Methods

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

Render (MONAD m)

Defined in Language.Syntactic.Functional

Methods

renderSym :: MONAD m sig -> String

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

Equality (MONAD m)

Defined in Language.Syntactic.Functional

Methods

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

hash :: MONAD m a -> Hash

Monad m => Eval (MONAD m)

Defined in Language.Syntactic.Functional

Methods

evalSym :: MONAD m sig -> Denotation sig

Monad m => EvalEnv (MONAD m) env

Defined in Language.Syntactic.Functional

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 https://emilaxelsson.github.io/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

Fields

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

Instances

Monad (Remon dom m)

Defined in Language.Syntactic.Functional

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

Functor (Remon sym m)

Defined in Language.Syntactic.Functional

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)

Defined in Language.Syntactic.Functional

Methods

pure :: a -> Remon sym m a

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

liftA2 :: (a -> b -> c) -> Remon sym m a -> Remon sym m b -> Remon sym m c

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

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

(sym ~ Typed s, Syntactic a, Domain a ~ sym, BindingT :<: s, MONAD m :<: s, Typeable m, Typeable (Internal a)) => Syntactic (Remon sym m a)

Defined in Language.Syntactic.Sugar.MonadTyped

Associated Types

type Domain (Remon sym m a) :: Type -> Type

type Internal (Remon sym m a)

Methods

desugar :: Remon sym m a -> ASTF (Domain (Remon sym m a)) (Internal (Remon sym m a))

sugar :: ASTF (Domain (Remon sym m a)) (Internal (Remon sym m a)) -> Remon sym m a

(Syntactic a, Domain a ~ sym, Binding :<: sym, MONAD m :<: sym, Typeable m, Typeable (Internal a)) => Syntactic (Remon sym m a)

Defined in Language.Syntactic.Sugar.Monad

Associated Types

type Domain (Remon sym m a) :: Type -> Type

type Internal (Remon sym m a)

Methods

desugar :: Remon sym m a -> ASTF (Domain (Remon sym m a)) (Internal (Remon sym m a))

sugar :: ASTF (Domain (Remon sym m a)) (Internal (Remon sym m a)) -> Remon sym m a

type Domain (Remon sym m a)

Defined in Language.Syntactic.Sugar.MonadTyped

type Domain (Remon sym m a) = sym

type Domain (Remon sym m a)

Defined in Language.Syntactic.Sugar.Monad

type Domain (Remon sym m a) = sym

type Internal (Remon sym m a)

Defined in Language.Syntactic.Sugar.MonadTyped

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

type Internal (Remon sym m a)

Defined in Language.Syntactic.Sugar.Monad

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)

Defined in Language.Syntactic.Functional

type Denotation (Full a) = a

type Denotation (a :-> sig)

Defined in Language.Syntactic.Functional

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

class Eval s where

Methods

evalSym :: s sig -> Denotation sig

Instances

Eval Empty

Defined in Language.Syntactic.Functional

Methods

evalSym :: Empty sig -> Denotation sig

Eval Let

Defined in Language.Syntactic.Functional

Methods

evalSym :: Let sig -> Denotation sig

Eval Construct

Defined in Language.Syntactic.Functional

Methods

evalSym :: Construct sig -> Denotation sig

Eval Literal

Defined in Language.Syntactic.Functional

Methods

evalSym :: Literal sig -> Denotation sig

Eval BindingWS

Defined in Language.Syntactic.Functional.WellScoped

Methods

evalSym :: BindingWS sig -> Denotation sig

Eval Tuple

Defined in Language.Syntactic.Functional.Tuple

Methods

evalSym :: Tuple sig -> Denotation sig

Monad m => Eval (MONAD m)

Defined in Language.Syntactic.Functional

Methods

evalSym :: MONAD m sig -> Denotation sig

Eval sym => Eval (ReaderSym sym)

Defined in Language.Syntactic.Functional.WellScoped

Methods

evalSym :: ReaderSym sym sig -> Denotation sig

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

Defined in Language.Syntactic.Functional

Methods

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

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

Defined in Language.Syntactic.Functional

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)

Defined in Language.Syntactic.Functional

type DenotationM m (Full a) = m a

type DenotationM m (a :-> sig)

Defined in Language.Syntactic.Functional

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

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

Instances

EvalEnv Empty env

Defined in Language.Syntactic.Functional

Methods

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

EvalEnv Let env

Defined in Language.Syntactic.Functional

Methods

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

EvalEnv BindingT RunEnv

Defined in Language.Syntactic.Functional

Methods

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

EvalEnv Construct env

Defined in Language.Syntactic.Functional

Methods

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

EvalEnv Literal env

Defined in Language.Syntactic.Functional

Methods

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

EvalEnv Tuple env

Defined in Language.Syntactic.Functional.Tuple

Methods

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

EvalEnv sym env => EvalEnv (Typed sym) env

Defined in Language.Syntactic.Functional

Methods

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

Monad m => EvalEnv (MONAD m) env

Defined in Language.Syntactic.Functional

Methods

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

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

Defined in Language.Syntactic.Functional

Methods

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

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

Defined in Language.Syntactic.Functional

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