Safe Haskell	None

Data.Syntactic.Functional

Contents

Syntactic constructs
Alpha-equivalence
Evaluation
Well-scoped terms

Description

Basics for implementing functional EDSLs

Synopsis

Syntactic constructs

newtype Name Source

Variable name

Constructors

Name Integer

Instances

Enum Name
Eq Name
Integral Name
Num Name
Ord Name
Real Name
Show Name
EvalEnv BindingT RunEnv

data Construct a whereSource

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

StringTree Construct
Render Construct
Equality Construct
Eval Construct
EvalEnv Construct env

data Binding a whereSource

Variables and binders

Constructors

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

Instances

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 Source

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

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 aSource

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 a whereSource

Typed variables and binders

Constructors

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

Instances

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 Source

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

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 whereSource

Domains that "might" include variables and binders

Methods

prVar :: sym sig -> Maybe Name Source

prLam :: sym sig -> Maybe Name Source

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 whereSource

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

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 whereSource

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)

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

One-layer desugaring of monadic actions

Alpha-equivalence

type AlphaEnv = [(Name, Name)]Source

Environment used by alphaEq'

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

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

Alpha-equivalence

Evaluation

type family Denotation sig Source

Semantic function type of the given symbol signature

class Eval s whereSource

Methods

evalSym :: s sig -> Denotation sigSource

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 sigSource

Evaluation

type family DenotationM m sig Source

Monadic denotation; mapping from a symbol signature

 a :-> b :-> Full c

to

 m a -> m b -> m c

liftDenotationM :: forall m sig proxy1 proxy2. (Monad m, Signature sig) => proxy1 m -> proxy2 sig -> Denotation sig -> DenotationM m sigSource

Lift a Denotation to DenotationM

type RunEnv = [(Name, Dynamic)]Source

Runtime environment

class EvalEnv sym env whereSource

Evaluation

Methods

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

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, Signature sig) => proxy env -> sym sig -> DenotationM (Reader env) sigSource

Simple implementation of compileSym from a Denotation

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

Evaluation of open terms

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

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 whereSource

Environment extension

Methods

unext :: ext -> origSource

Remove the extension of an environment

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

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 aSource

Lookup in an extended environment

data BindingWS a whereSource

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

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

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

Evaluation of open well-scoped terms

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

Evaluation of closed well-scoped terms

type family LiftReader env sig Source

Mapping from a symbol signature

 a :-> b :-> Full c

to

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

type family UnReader a Source

type family LowerReader sig Source

Mapping from a symbol signature

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

to

 a :-> b :-> Full c

data ReaderSym sym a whereSource

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

Well-scoped AST

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

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 -> fSource

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)