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

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 :: 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 :: Binding :<: s => (ASTF s a -> ASTF s b) -> ASTF s (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 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).

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

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 :: BindingT :<: s => AST s 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 :: forall s a b. (BindingT :<: s, Typeable a) => (ASTF s a -> ASTF s b) -> ASTF s (a -> b)

Higher-order interface for typed 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).

class BindingDomain sym where

Domains that "might" include variables and binders

Methods

prVar :: sym sig -> Maybe Name

prLam :: sym sig -> Maybe Name

Instances

BindingDomain sym

BindingDomain BindingT

BindingDomain Binding

BindingDomain sym => BindingDomain (AST sym)

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

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

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 Mon using the Syntactic instance provided in the modules Data.Syntactic.Sugar.Monad or Data.Syntactic.Sugar.MonadT.

Constructors

Remon :: (forall r. (Monad m, MONAD m :<: sym) => Cont (ASTF sym (m r)) a) -> Remon sym m a

Fields

unRemon :: forall r. (Monad m, MONAD m :<: sym) => Cont (ASTF sym (m r)) a

Instances

Monad m => Monad (Remon dom m)

Functor (Remon sym m)

Applicative m => Applicative (Remon sym m)

(Syntactic a, (~) (* -> *) (Domain a) sym, (:<:) Binding sym, (:<:) (MONAD m) sym, Monad m) => Syntactic (Remon sym m a)

(Syntactic a, (~) (* -> *) (Domain a) sym, (:<:) BindingT sym, (:<:) (MONAD m) sym, Monad m, Typeable * (Internal a)) => Syntactic (Remon sym m a)

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, Monad m) => Remon sym m (ASTF sym a) -> ASTF sym (m a)

One-layer desugaring of monadic actions

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 BindingWS

Eval Construct

Eval sym => Eval (ReaderSym sym)

Monad m => Eval (MONAD m)

(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 BindingT RunEnv

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

Well-scoped terms

class Ext ext orig where

Environment extension

Methods

unext :: ext -> orig

Remove the extension of an environment

diff :: Num a => Proxy ext -> Proxy orig -> a

Return the amount by which an environment has been extended

Instances

(Ext env e, (~) * ext (a, env)) => Ext ext e

Ext env env

lookEnv :: forall env a e. Ext env (a, e) => Proxy e -> Reader env a

Lookup in an extended environment

data BindingWS sig where

Well-scoped variable binding

Well-scoped terms are introduced to be able to evaluate without type casting. The implementation is inspired by "Typing Dynamic Typing" (Baars and Swierstra, ICFP 2002, http://doi.acm.org/10.1145/581478.581494) where expressions are represented as (essentially) Reader env a after "compilation". However, a major difference is that "Typing Dynamic Typing" starts from an untyped term, and thus needs (safe) dynamic type casting during compilation. In contrast, the denotational semantics of BindingWS (the Eval instance) uses no type casting.

Constructors

VarWS :: Ext env (a, e) => Proxy e -> BindingWS (Full (Reader env a))

LamWS :: BindingWS (Reader (a, e) b :-> Full (Reader e (a -> b)))

Instances

Symbol BindingWS

Eval BindingWS

lamWS :: forall a e sym b. BindingWS :<: sym => ((forall env. Ext env (a, e) => ASTF sym (Reader env a)) -> ASTF sym (Reader (a, e) b)) -> ASTF sym (Reader e (a -> b))

Higher-order interface for well-scoped variable binding

Inspired by Conor McBride's "I am not a number, I am a classy hack" (http://mazzo.li/epilogue/index.html%3Fp=773.html).

evalOpenWS :: Eval s => env -> ASTF s (Reader env a) -> a

Evaluation of open well-scoped terms

evalClosedWS :: Eval s => ASTF s (Reader () a) -> a

Evaluation of closed well-scoped terms

type family LiftReader env sig

Mapping from a symbol signature

a :-> b :-> Full c

to

Reader env a :-> Reader env b :-> Full (Reader env c)

Instances

type LiftReader env (Full a) = Full (Reader env a)

type LiftReader env ((:->) a sig) = (:->) (Reader env a) (LiftReader env sig)

type family UnReader a

Instances

type UnReader (Reader e a) = a

type family LowerReader sig

Mapping from a symbol signature

Reader e a :-> Reader e b :-> Full (Reader e c)

to

a :-> b :-> Full c

Instances

type LowerReader (Full a) = Full (UnReader a)

type LowerReader ((:->) a sig) = (:->) (UnReader a) (LowerReader sig)

data ReaderSym sym sig where

Wrap a symbol to give it a LiftReader signature

Constructors

ReaderSym :: (Signature sig, Denotation (LiftReader env sig) ~ DenotationM (Reader env) sig, LowerReader (LiftReader env sig) ~ sig) => Proxy env -> sym sig -> ReaderSym sym (LiftReader env sig)

Instances

Eval sym => Eval (ReaderSym sym)

type WS sym env a = ASTF (BindingWS :+: ReaderSym sym) (Reader env a)

Well-scoped AST

fromWS :: WS sym env a -> ASTF (Binding :+: sym) a

Convert the representation of variables and binders from BindingWS to Binding. The latter is easier to analyze, has a Render instance, etc.

smartWS :: forall sig sig' bsym f sub sup env a. (Signature sig, Signature sig', sub :<: sup, bsym ~ (BindingWS :+: ReaderSym sup), f ~ SmartFun bsym sig', sig' ~ SmartSig f, bsym ~ SmartSym f, sig' ~ LiftReader env sig, Denotation (LiftReader env sig) ~ DenotationM (Reader env) sig, LowerReader (LiftReader env sig) ~ sig, Reader env a ~ DenResult sig') => sub sig -> f

Make a smart constructor for well-scoped terms. smartWS has any type of the form:

smartWS :: (sub :<: sup, bsym ~ (BindingWS :+: ReaderSym sup))
    => sub (a :-> b :-> ... :-> Full x)
    -> ASTF bsym (Reader env a) -> ASTF bsym (Reader env b) -> ... -> ASTF bsym (Reader env x)