\documentclass{entcs}
\usepackage{entcsmacro}

%include lhs2TeX.fmt
%include polycode.fmt

\usepackage{float}
\usepackage{graphicx}
\usepackage{pgf}
\usepackage{tikz}
\usetikzlibrary{arrows,positioning}
\floatstyle{boxed}
\restylefloat{figure}

\def\lastname{Middelkoop and Dijkstra and Swierstra}

%format ^^^^ = "\hspace{1em}"
%format ^^^ = "\;"
%format sig = "\mathbf{sig}"
%format inh = "\mathbf{inh}"
%format syn = "\mathbf{syn}"
%format sem = "\mathbf{sem}"
%format tail = "\mathbf{tail}"
%format clause = "\mathbf{clause}"
%format match  = "\mathbf{match}"
%format child  = "\mathbf{child}"
%format forall (xs) (q) = "\mathbf{forall}\;" xs ".\;" q
%format (overline (x)) = "\overline{" x "}"
%format partial = "\mathbf{partial}"
%% %format lhs = "\mathbf{lhs}"
%% %format loc = "\mathbf{loc}"
%format alt = "\mathbf{alt}"
%format none = "\mathbf{none}"
%format strict = "\mathbf{strict}"

%format alpha = "\alpha"
%format beta = "\beta"

%format (attr f a) = f "." a
%format (lhsattr a) = lhs "." a
%format (locattr a) = loc "." a
%format (sub (k) (x)) = "{" k "}_{" x "}"
%format (tau (x)) = "\tau_{" x "}"
%format (In (k) (x))  = k "I" x
%format (Out (k) (x)) = k "O" x
%format (InLhs (x))  = "lhsI" x
%format (OutLhs (x)) = "lhsO" x

%format a1
%format a2
%format k1
%format k2
%format S1
%format S2
%format S3
%format S4
%format s1
%format s2
%format b1
%format t1
%format t2
%format t3
%format t4
%format x1
%format x2
%format i1
%format i2
%format tauS' = "\tau_{" S' "}"


\begin{document}

\begin{frontmatter}
  \title{Visit Functions for the Semantics of Programming Languages}
  \author{Arie Middelkoop\thanksref{email}}
  \address{Universiteit Utrecht, The Netherlands}
  \author{Atze Dijkstra\thanksref{email}}
  \address{Universiteit Utrecht, The Netherlands}
  \author{S. Doaitse Swierstra\thanksref{email}}
  \address{Universiteit Utrecht, The Netherlands}
  \thanks[email]{Email:
    \href{mailto:ariem@@cs.uu.nl} {\texttt{\normalshape
        \{ariem,atze,doaitse\}@@cs.uu.nl}}}
\begin{abstract}
  Attribute grammars (AGs) were conceived to concisely define the semantics of
  programming languages.
  Unfortunately, when such a semantics requires
  case distinction on more than a
  single abstract syntax tree, or requires global reasoning
  about the order of data flow, these semantics cannot be expressed with AGs.
  We present a conservative extension of AGs, based on visit
  functions, that deals with the aforementioned problems.
\end{abstract}
\begin{keyword}
  attribute grammar, visit function, functional programming
\end{keyword}
\end{frontmatter}

\section{Introduction}
\label{sect.visit.intro}

  Attribute grammars concisely describe the semantics of programming
  languages~\cite{DBLP:journals/mst/Knuth68}. In this paper, we consider
  algorithmic variations on attribute grammars, which express these
  semantics in an executable way. For example, the language Haskell
  has an intricate type system, and we implemented a type inferencer
  concisely with AGs~\cite{1596650}.
  The programmer writes computations between attributes on the
  abstract syntax tree, and does not need to write code related
  to moving around values across the AST.
  Combined with copy rules~\cite{10.1109/SCAM.2007.13,DBLP:conf/icfp/VieraSS09},
  the programmer is saved from tedious boilerplate code.
  Furthermore, AGs offer an
  aspect-wise programming model~\cite{DBLP:conf/icfp/VieraSS09}.
  Because of the restrictions imposed by the formalism, AGs can be analyzed and compiled to
  efficient code~\cite{DBLP:conf/popl/KennedyW76,DBLP:journals/acta/Kastens80}.

  Often, some relations in a language's semantics use case distinction
  on multiple ASTs, which cannot be expressed by AGs.
  Clauses of a type equivalence relations in type systems, for example,
  take the ASTs of both respective arguments of the relation into consideration
  (Section~\ref{sect.visit.example}).

  In an AG, the order in which the values for attributes are evaluated
  is left implicit. Sometimes, however, we want to explicitly express
  parts of this order. For example, to exploit the knowledge that specific
  values for an attribute have been observed in a conditional computation,
  or to decorate the tree with different sets of attributes depending on the
  context (Section~\ref{sect.visit.contexts}).
  Furthermore, several whole program analyses become superfluous, or 
  are equivalent to local analyses with lower complexity bounds~\cite{512989}.

  Our contribution is a programming model based
  on visit functions~\cite{Saraiva99}. Visit functions were
  originally introduced as a technique to implement AGs efficiently
  in purely functional programming languages; in this paper, we recast
  them as a solution to the above challenges.
  The resulting programming model is more
  flexible than the one offered by attribute grammars, while
  still allowing convenient reasoning in terms of trees
  decorated with attributes.

  We implemented a preprocessor for this programming model in
  Haskell\footnote{@http://people.cs.uu.nl/ariem/visits-ag.tar.gz@}.
  The ideas presented in this paper are applicable to any language in
  which closures can be modeled easily.
  %% This holds for most modern languages available today.
  We rely on lazy evaluation to keep the explanation in this paper simple, but this is 
  not a strict requirement.
  For the technical parts of this paper, we assume that the reader is familiar with
  functional programming, and Haskell in particular.
  Consider Hudak, et al.~\cite{Hudak99agentle}, for a gentle introduction to Haskell.

  Section~\ref{sect.visit.inituition} explains the programming model and
  its semantics. Section~\ref{sect.visit.example} shows an example where
  this programming model is useful. Section~\ref{sect.visit.translation}
  describes how to translate the visit functions to Haskell. Finally,
  Section~\ref{sect.visit.motivation} shows the expressiveness of the
  formalism.


\section{Idea}
\label{sect.visit.inituition}

  We present visit functions as a domain specific language for Haskell.
  The visit functions themselves are encoded as Haskell functions, and we
  provide special syntax to write these functions in terms of attributed trees.

  A \emph{visit function} is a (partial) function that takes several inputs (\emph{inherited attributes}), delivers several outputs (\emph{synthesized attributes}),
  and (optionally) delegates some of its work to one special output called the \emph{tail}.
  This tail is again a visit function.
  The shape of such a function (i.e., the names and
  types of inputs and outputs) is specified with a \emph{type signature}. An example of such a specification
  is:
  \begin{code}
  sig S1                  -- a (possibly parametrized) type |S1| for visit functions
  inh S1  ^^^^ x :: Int   -- declare an input |x| for |S1| (of type |Int|)
  syn S1  ^^^^ y :: Char  -- declare an output |y| for |S1| (of type |Char|)
  tail S1 :: S2           -- the type of the visit function of the continuation
  \end{code}
  A visit function of the type |S1| thus takes an |Int| named |x|, computes a character |y|,
  and computes a visit function with the type |S2| that performs the remainder of the work
  (up to the imagination of the reader; see Section~\ref{sect.visit.example} for a real example).

  Each signature can be mappend to a Haskell type:
  \begin{code}
  newtype S1 = S1 (Int -> Maybe (S2, Char))
  instance Monoid S1 where mappend = ...  ^^^^ mempty = ...
  \end{code}
  %% wrap_S1 :: S1 -> Inh_S1 -> Maybe Syn_S1
  %% unwrap_S1 :: (Inh_S1 -> Maybe Syn_S1) -> S1
  %% data Inh_S1 = Inh_S1 { x_Inh_S1:: Int }
  %% data Syn_S1 = Syn_S1 { y_Inh_S1 :: Char, tl_Inh_S1 :: S2 }
  %% Remove the wrappers from the explanation? They don't really add a thing?
  The functions are partial; when no case applies, the result is a |Nothing| value, otherwise
  a |Just| with a tuple of the synthesized values.
  %% this can actually be generalized in a nice way, but doesn't fit in this paper :(
  %% Through the wrapper functions, a visit function its inputs and outputs can be addressed by
  %% name, independent of the actual argument order.
  The |Monoid| operation |mappend| glues two partial visit functions together, which results
  in a visit function that handles the union of the cases handled by the
  visit functions individually; |mempty| represents the undefined case.

  \begin{figure}[htb]
  \centering
  \begin{tikzpicture}[>=stealth']
  \node (lhs) [draw,circle] {|lhs|};
  \node (k1) [below left=4cm of lhs, draw, circle] {|k1|}
    edge[<-] (lhs.south);
  \node (k2) [below right=4cm of lhs, draw, circle] {|k2|}
    edge[<-] (lhs.south);
  \node (lhsx)  [draw,rectangle, left=0.2cm of lhs] {|x|};
  \node (lhsy)  [draw,rectangle, right=0.2cm of lhs] {|y|};
  \node (lhstl) [draw,rectangle, dotted, right=0.3cm of lhsy] {tail syn}
    edge[->, dashed, bend left=45] (lhsx.south);
  \node (lhstl1) [draw,rectangle, dotted, left=0.3cm of lhsx] {tail inh};
  \node (k1x)  [draw,rectangle, left=0.2cm of k1] {|x|}
    edge[->, dashed] (lhsx.south);
  \node (k1y)  [draw,rectangle, right=0.2cm of k1] {|y|}
    edge[<-, dashed] (lhsy.south);
  \node (k1tl) [draw,rectangle, dotted, right=0.3cm of k1y] {tail syn};
  \node (k1tl1) [draw,rectangle, dotted, left=0.3cm of k1x] {tail inh};
  \node (k2x)  [draw,rectangle, left=0.2cm of k2] {|x|}
    edge[->, bend left=45, dashed] (lhsx.south)
    edge[->, bend left=45, dashed] (k1y.south);
  \node (k2y)  [draw,rectangle, right=0.2cm of k2] {|y|}
    edge[<-, dashed] (lhsy.south);
  \node (k2tl) [draw,rectangle, dotted, right=0.3cm of k2y] {tail syn}
    edge[<-, dashed] (lhstl.south);
  \node (k2tl1) [draw,rectangle, dotted, left=0.3cm of k2x] {tail inh};
  \end{tikzpicture}
  \caption{An example of an attributed call tree with pending visits.}
  \label{fig.example.calltree}
  \end{figure}
  
  The body of a visit function is defined in terms of a one-level {\it attributed}
  static call graph with the visit function as root. Figure~\ref{fig.example.calltree} shows an
  example of such a graph (actually, a tree).
  Each round node in this graph corresponds to a \emph{function call}. An arrow from
  |f| to |g| means that |g| is called in the body of |f| (we call |g| a child of |f|).
  Each node is labelled with a name, in order to refer to attributes later. The root node corresponds to the currently executing function,
  and has the reserved name |lhs|.
  The inputs for each function call are called the
  \emph{inherited attributes} of the node in the call graph (squares to the left), and the outputs the
  \emph{synthesized attributes} (squares to the right). Attributes defined in later visits are not visible
  yet, and are indicated by the dotted boxes. Dashed arrows from an attribute |b| to
  attributes $|a|_1, \ldots, |a|_n$ denote a Haskell expression that produces a value for |b| given
  the values of $|a|_1, \ldots, |a|_n$. The visit functions are generated from this model.
  Below, we demonstrate how to denote visit functions in terms of these trees, and their semantics.

  %% %% Not important enough to include in this paper:
  %% The example in the figure does not show the full generality of visit functions.
  %% The semantics of a node can be specified by attributes, hence there can
  %% be dashed lines from a node to an attribute. Also, the visits to the
  %% the children can deviate from that of the parent.

  To illustrate, suppose that |f| is a visit function of the type |S1| which performs
  a recursive call |k1|, also calls |k1|'s continuation (of type |S2|), and defines values for some
  of the attributes:
  \begin{code}
  let f =  sem :: S1
             (attr lhs y)  = if lhsattr x > 10 then (attr k1 y) else 'z'
             attr k1 x     = 3   -- define value for inherited attribute |x| of |k1|
             child k1 :: S1 = f  -- |k1| is a recursive call
             child k1 : S2       -- call to continuation visit of |k1| (with type |S2|)
             tail sem :: S2 ...  -- definition of function for the next visit
  \end{code}
  The |sem| keyword introduces a visit function of type |S1|, followed by several \emph{statements} that
  define its contents.
  In patterns and expressions,
  attributes are referenced with the notation |attr k a| (child named |k|, its attribute |a|).
  The first statement defines the attribute |y| of |lhs| in terms
  of the synthesized attribute |y| of child |k1|, and the inherited attribute |x| of
  |lhs|.
  To prevent mixing up the inputs and outputs of functions, to the left of the
  |=|, only inherited attributes of the children and synthesized attributes of |lhs| may
  occur, and to the right only synthesized attributes of the children and inherited attributes of |lhs|.
  Inherited and synthesized attributes may use the same name, but still refer to different attributes.
  With the above rule it is always clear which of the attributes is intended.

  Ignoring several details for now, the encoding for |f| in Haskell is:
  %format htail = "tail"
  \begin{code}
  let f = \lhs_x ->  let  Just (k1_tail_S2, k1_y)  = f k1_x          -- recursive call
                          Just (k1_tail_S3, ...)   = k1_tail_S2 ...  -- second visit
                          lhs_y   = if lhs_x > 10 then k1_y else 'z'
                          k1_x    = ...        -- etc.
                          htail   = ... \ ...  -- construction of tail visit
                     in Just (htail, lhs_y)
  \end{code}

\section{Example}
\label{sect.visit.example}

  Consider a type equivalence relation used in the type system of some language
  specification. In this section, we define an inference algorithm for this
  relation with visit
  functions (i.e., executable semantics).
  The example algorithm consists of two visits, in which the second
  visit makes use of the result of a global computation based on the results of
  the first visit. Reasoning about visits is important in this case.
  Furthermore, this example requires
  case distinction on two ASTs.

  The algorithm we define as the two-visit Haskell function |unify| with the type |Unify|.
  The first visit gets two types |t1| and |t2| as input,
  and returns a substitution |sinit|, such that |sinit(t1) == sinit(t2)|,
  %% up to the depth of deviating type constructors in |t1| and |t2|. 
  unless the two types cannot be unified.
  For the
  latter cases, we return a list of error messages, but do so in the second
  visit. We want the error messages in terms of the resulting
  substitution of the first visit, to incorporate type information found in, for example,
  an entire binding group worth of inferencing. Therefore, the second visit
  takes as input the final substitution |sfinal|, and constructs then the list
  of error messages. Hence, the signatures read:
  \begin{code}
  sig Unify                                 ^^^^ ^^^^   sig Report
  inh Unify  ^^^^ t1 :: Type  t2 :: Type    ^^^^ ^^^^   inh Report  ^^^^ sfinal :: Subst
  syn Unify  ^^^^ sinit :: Subst            ^^^^ ^^^^   syn Report  ^^^^ errs :: [String]
  tail Unify :: Report                                  -- |Report| has no tail
  \end{code}
  The syntax of types plays an important role. We choose a simple
  representation in the form of variables and arrows, resembling the Haskell data type declarations:
  \begin{code}
  data Ty ^^^^ | TVar ident :: Int  ^^^^  | TArr arg :: Ty ^^^ ^^^ res :: Ty
  \end{code}
  The fields of the
  constructors must be named. We offer a special pattern match
  |k@TArr|, which introduces a virtual child |k| with the fields of |TArr| as
  attributes (i.e., |attr k arg| and |attr k res|) upon a successful match.
  %% Introducing local attributes here is perhaps not a good idea
  A special virtual child is |loc| which stores \emph{local attributes} (not visible to the outside).

  We define the actual cases of the visit function separately and combine these
  later as function |unify|. Case |unifyVar|
  applies when |t1| is a variable, and binds |t2| to that variable, resulting in a
  substitution:
  \begin{code}
  unifyVar =  sem :: Unify
                match a@TVar                     = lhsattr t1  -- tests if |lhsattr t1| is a |TVar|
                (lhsattr sinit, locattr failed)  = bind (attr a ident) (lhsattr t2)
                tail  sem :: Report  -- construct the semantics of the tail
                        locattr msg   =  "bind:"   ++ show ((lhsattr t1) `updBy` (lhsattr sfinal))
                                         ++ "to:"  ++ show ((lhsattr t2) `updBy` (lhsattr sfinal))
                        lhsattr errs  =  if locattr failed then [locattr msg] else []
  \end{code}
  Here |bind| is a conventional Haskell function that returns a tuple.
  If the pattern of a |match| statement does not apply, this particular case does not apply and the
  result is an observable |Nothing| value and can be handled. Without the |match| keyword, we call
  it an {\it eval statement}, and it is up to the programmer to guarantee that the match always succeeds.
  Note that an embedded |sem| has access to all attributes defined in its outer |sem|, such
  as the types |t1| and |t2|, as well as the local attributes |failed| and |msg|.

  When both types are or the arrow type, the semantics is simple: pairwise recursive in the subcomponents of the types, aggregating the results:
  \begin{code}
  unifyArr =  sem :: Unify
                match a@TArr  = lhsattr t1  -- if both types are arrows, intros:
                match b@TArr  = lhsattr t2  -- |attr a arg|, |attr a res|, |attr b arg|, |attr b res| 
                ^^^
                child k1 :: Unify = unify   -- recursive calls to the pairwise
                child k2 :: Unify = unify   -- subcomponents of |t1| and |t2|
                attr k1 t1     = attr a arg  ^^^^  attr k1 t2     = attr b arg   -- parametrizing the
                attr k2 t1     = attr a res  ^^^^  attr k2 t2     = attr b res   -- recursive calls
                ^^^
                lhsattr sinit  =  (attr k1 sinit) `mappend` (attr k2 sinit)
                tail  sem :: Report
                        child k1 : Report  -- calls to the second visit of the
                        child k2 : Report  -- recursive call
                        attr k1 sfinal  = lhsattr sfinal  ^^^^  attr k2 sfinal  = lhsattr sfinal
                        lhsattr errs    = attr k1 errs ++ attr k2 errs
  \end{code}
  In practice (Section~\ref{sect.visit.practice}), most of the above statements are implied by the
  structure of the |TArr| constructor and copy rules, and can be omitted, saving a lot of trivial
  code. 
  %% Most of the contents can be produced by copy rules.
  %% Note that by putting the code in this form, most of this code can actually be generated from the
  %% definition of the data type together with copy rules.

  Finally, we provide a sentinel case to be used when no other cases apply:
  \begin{code}
  unifyFail =  sem :: Unify  ^^^^  lhsattr sinit  = mempty
                                   tail  sem :: Report  ^^^^  lhsattr errs = [...]
  \end{code}

  In the end, we combine the individual cases, and invoke them from Haskell:
  \begin{code}
  unify =  unifyVar `mappend` flip unifyVar  -- symmetric cases
             `mappend` unifyArr `mappend` unifyFail
  ...  let  Just (report, sfinal)  = unify someType someOtherType
            Just errs              = report sfinal  -- feed back subst
  \end{code}


%if False
\section{Example}
\label{sect.visit.example}

  In this section, we give the semantics of an inferencer for a lambda calculus with a mutually
  recursive |let| with multiple declarations in terms of visit sequences in Haskell.

  \subsection{Data types}
  
  We introduce a number of data types that represent the AST of the example language:
  \begin{code}
  data Expr   | EVar    x  :: Name
              | EApp    f  :: Expr  a  :: Expr
              | ELam    x  :: Name  b  :: Expr
              | ELet    d  :: Decls
  type Decls  = [Decl]
  data Decl   | Decl  x :: Name  e :: Expr
  data Type   | TVar  i :: Int
              | TArr  a :: Type  r :: Type
  \end{code}
  Such a |data| declaration introduces a type (i.e., |Expr|), and a number of constructors
  for this type (i.e., |EVar| and |TArr|), including names and types of the fields of these
  constructors.
  
  These data declarations are similar to data type declarations with records in Haskell.
  For data types specified in the above way, we provide a special pattern match notation,
  e.g. |k@ELam|, for Haskell pattern expressions, which upon a successful match, binds the
  fields of the constructor to equally named attributes of the virtual child |k|. These
  attributes and children we explain later.

  \subsection{Signatures}
  
  We define types we use for the semantic functions below. These types specify the inputs and
  outputs (and their respective types) of one visit to the semantic function, and the type of
  remainder of the visits.
  
  \begin{code}
  sig Infer
  syn Infer  tp :: Type  subst :: Subst  errs :: Errs
  sig Propagate
  syn Propagate  subst :: Subst  errs :: Errs
  \end{code}
  
  \begin{code}
  forall beta (sig Validate)
  inh Validate  env     :: Lookup
  inh Validate  subst   :: Subst
  tail Validate :: beta
  \end{code}
  
  \begin{code}
  sig Single
  inh Single  ast :: Expr
  tail Single :: Validate Infer
  \end{code}

  \begin{code}
  forall (alpha beta) (sig Gather)
  inh Gather  ast :: alpha
  syn Gather  env :: Lookup
  tail Gather :: beta
  \end{code}

  \begin{code}
  sig Unify
  inh Unify  a :: Type  b :: Type
  tail Unify :: Validate Propagate
  \end{code}
  
  \begin{code}
  sig Lookup
  inh Lookup  x :: Name
  syn Lookup  tp :: Type  errs :: Errs
  \end{code}
  
  \begin{code}
  sig Fresh
  inh Fresh  subst :: Subst
  syn Fresh  subst :: Subst  tp :: Type
  sig Bind
  inh Bind  i :: Int  tp :: Type  subst :: Subst
  syn Bind  subst :: Subst
  \end{code}

  \subsection{Semantics}
  
  \begin{code}
  inferExpr :: Single Expr
  inferExpr = foldr mappend mempty [inferVar,inferLam,inferApp,inferLet]
  
  inferDecls :: Gather Decls (Validate Propagate)
  inferDecls = inferCons `mappend` inferNil
  \end{code}
  
  \begin{code}
  inferVar =  sem :: Single Expr
                match (loc@EVar) = lhsattr ast
                tail  sem :: Validate Infer
                        tail  sem :: Infer
                                child l :: Lookup = lhsattr env
                                attr l x       = locattr x
                                lhsattr tp     = attr l tp
                                lhsattr subst  = lhsattr subst
                                lhsattr errs   = attr l errs
  \end{code}
  
  \begin{code}
  inferLam =  sem :: Single Expr
                match (loc@ELam) = lhsattr ast
                child k1 :: Single Expr = inferExpr
                attr k1 ast = locattr b
                tail  sem :: Validate Infer
                        child fr :: Fresh = fresh
                        child k1 : Validate Infer
                        attr k1 env  =  sem :: Lookup
                                          guard lhsattr x == locattr x
                                          lhsattr tp = attr fr tp
                                     `mappend` (lhsattr env)
                        tail  sem :: Infer
                                child k1 : Infer
                                attr fr subst  = lhsattr subst
                                attr k1 subst  = attr fr subst
                                lhsattr subst  = attr k1 subst
                                lhsattr errs   = attr k1 errs
                                lhsattr ty     = TArr (attr fr ty) (attr k1 ty)
  \end{code}
  
  \begin{code}
  inferApp =  sem :: Single Expr
                match (loc@EApp) = lhsattr ast
                child k1 :: Single Expr = inferExpr
                child k2 :: Single Expr = inferExpr
                tail  sem :: Validate Infer
                        child fr :: Fresh = fresh
                        child k1 : Validate Infer
                        child k2 : Validate Infer
                        attr k1 env  = lhsattr env
                        attr k2 env  = lhsattr env
                        tail  sem :: Infer
                                child u :: Unify = unify
                                child u : Validate Propagate
                                child k1 : Infer
                                child k2 : Infer
                                attr fr subst  = lhsattr subst
                                attr k1 subst  = attr fr subst
                                attr k2 subst  = attr k1 subst
                                attr u subst   = attr k2 subst
                                lhsattr subst  = attr u subst
                                attr u a       = attr k1 ty
                                attr u b       = TArr (attr k2 ty) (attr fr ty)
                                lhsattr tp     = attr fr tp
                                lhsattr errs   = (attr k1 errs) ++ (attr k2 errs) ++ (attr u errs)
  \end{code}
  
  \begin{code}
  inferLet =  sem :: Single Expr
                match (loc@ELet) = lhsattr ast
                child k1 :: Group = inferDecls
                child k2 :: Expr  = inferExpr
                tail  sem :: Validate Infer
                        child k1 : Validate Propagate
                        child k2 : Validate Infer
                        attr k1 env  = attr k1 env
                        attr k2 env  = (attr k1 env) `union` (lhsattr env)
                        ...
  \end{code}
  
  \begin{code}
  inferDecl =  sem :: Gather Decl Single
                 (loc@Decl)   =  lhsattr ast
                 child fr :: Fresh = fresh
                 lhsattr env  =  sem :: Lookup
                                   guard (lhsattr x) == locattr x
                                   lhsattr tp = attr fr tp
                 ...
                   child k1 :: Single Expr
                   attr k1 ast = attr loc e
                   ...
                   child u :: Unify
                   attr u a = attr k1 tp
                   attr u b = attr fr tp
  \end{code}
  
  \begin{code}
  unify =  unifyVar `mappend` unifyArr `mappend` failUnify
  failUnify = ...
  \end{code}
  
  \begin{code}
  unifyVar =  sem :: Unify
                match (a@TVar) = lhsattr a
                match (b@TVar) = lhsattr b
                tail  sem :: Validate Propagate
                        tail  sem :: Propagate
                                lhsattr subst = lhsattr subst
                                lhsattr errs  = []
  \end{code}
  
  \begin{code}
  unifyApp =  sem :: Unify
                match (a@TArr) = lhsattr a
                match (b@TArr) = lhsattr b
                child k1 :: Unify
                attr k1 a = attr a a
                attr k1 b = attr a r
                ...
  \end{code}
%endif


\section{Translation}
\label{sect.visit.translation}

  In this section, we formally define the visit function language by means of a mapping to
  Haskell. Data type declarations and signatures can occur at places where toplevel declarations
  are allowed. The semantic blocks can occur at any place where a Haskell expression is
  expected. We describe the individual translations below.

  \subsection{Patterns}
  Attributes are translated to
  Haskell variable names. An attribute occurrence
  |attr k x| in a pattern is translated to |kOx| (with |O| meaning "out", and |k| and |x| metavariables),
  and in an expression to:
  |kIx| (with |I| meaning "in"). Local attributes in both cases are translated to |locLx|.
%%  The inverse of this scheme we use in the translation of the other constructs.
  A pattern |k@C| for some constructor |C| with fields named |x1, ..., (sub x n)|
  is translated to |C (In k x1) .. (In k (sub x n))|.

  \subsection{Type Signatures}
  A signature |forall (overline alpha) S| with inherited attributes
  |i1 :: (tau i1), ..., (sub i n) :: (tau (sub i n))|,
  synthesized attributes |s1 :: (tau s1), ..., (sub s m) :: (tau (sub s m))|, and tail with type
  |S' (overline (tauS'))|, is translated to:
  \begin{code}
  newtype S (overline alpha) = S (S_imp (overline alpha))
  type S_imp (overline alpha) = (tau i1) -> ... -> (tau (sub i n)) -> Maybe (S' (overline tauS'), (tau s1), ..., (tau (sub s m)))
  instance Monoid (S (overline alpha)) where
    mempty = S (\lhs_i1 ... lhs_(sub i n) -> Nothing)
    mappend (S s1) (S s2) = S ( \lhs_i1 ...  lhs_(sub i n) -> 
      maybe (s2 (InLhs i1) ... (InLhs (sub i n))) Just (s1 (InLhs i1) ... (InLhs (sub i n))) )
  \end{code}
  %% Drop the wrapper stuff?? Saves at least some space.
  %% data Inh_S (overline alpha) = Inh_S { i1_Inh_S :: (tau i1), ..., (sub i n)_Inh_S :: (tau (sub i n)) }
  %% data Syn_S (overline alpha) = Syn_S { tl_Syn_S :: S' (overline tauS'), s1_Syn_S :: (tau s1), ..., (sub s m)_Inh_S :: (tau (sub s m)) }
  %% wrap_S f (Inh_S i1 ... (sub i n)) =  case (f i ... lhs_(sub i n)) of
  %%                                               Just (tl, s1, (sub s m))  -> Just (Syn_S tl s1 ... (sub s m))
  %%                                               Nothing                   -> Nothing
  
  \subsection{Visit Functions}
  A semantic block |sem :: S ...| is translated to the following expression:
  \begin{code}
  S  (\  (InLhs (sub i 1)) ... (InLhs (sub i n)) ->
         let  ...          -- translation for statements
              htail = ...  -- translation for tail code
         in  if and [b1,...,(sub b r)]
             then Just (htail, OutLhs (sub s 1), ..., OutLhs (sub s m))
             else Nothing )
  \end{code}
  When |S| does not have a tail, the |htail| part is not generated.
  The booleans |sub b i| are defined by the translation of match statements,
  and indicate whether the matches succeeded.
  Because of Haskell's lazy evaluation,
  the order of the |sub b i|'s in the list determines the order in which the matches are
  performed. Here we take the order of appearance: in Section~\ref{sect.visit.aggressiveoptimization}
  we describe how to determine the least influential order, as
  addressed by Boyland~\cite{DBLP:journals/toplas/Boyland96} for attribute grammars.

  Each match statement is numbered by its order of appearance. The \emph{match statement} |match p = e| numbered |i|, with a pattern |p| and an expression |e|
  is translated to:
  \begin{code}
  ((sub b i), a1, ..., (sub a n)) =  case e' of
                                       p'  -> (True, a1, ..., (sub a n))
                                       _   -> (False, undefined, ..., undefined)
  \end{code}
  where |p'| is the Haskell pattern with attribute occurrences substituted to Haskell names |a1, ..., (sub a n)| and
  |e'| is the Haskell expression with the occurrences substituted.
  An \emph{eval statement} of the form |p = e| is translated directly to |p' = e'|.

  For the translation of statements, we have a number of choices.
  Here we assume that visits to children always succeed. With slightly different translation strategies, we
  can allow failing children to fail the parent observably, thus allowing more extensive forms of backtracking.
  A \emph{child statement} |child k :: S = f| is translated to:
  \begin{code}
  Just (k_tail_S', In k (sub s 1), ..., In k (sub s m)) = f (Out k (sub i 1)) ... (Out k (sub i n))
  \end{code}
  Similarly, a \emph{child visit statement} |child k : S = f| (|f| is by default |id|) is translated to:
  \begin{code}
  Just (k_tail_S', In k (sub s 1), ..., In k (sub s m)) = f k_tail_S (Out k (sub i 1)) ... (Out k (sub i n))
  \end{code}
  The function |f| has the option to transform the semantics of the child visit, based on context of the
  parent.


\section{Discussion}
\label{sect.visit.motivation}

  In this section, we further motivate our choice for visit functions.
    
  \subsection{Contexts}
  \label{sect.visit.contexts}
    Bidirectional type rules are hard to model with attribute grammars, because the attribution of the tree
    depends on a context expected by the parent. With visit functions, we tackle this problem by
    introducing an additional visit with an input identifying the context requested by the caller:
    \begin{code}
    forall beta (sig Validate)                                           -- |beta| the type of the tail
    inh Validate ^^^^ h :: Handle beta  ^^^^ ^^^^ tail Validate :: beta  -- type of |h| determines |beta|
    ^^^^
    sig Check  ^^^^  ^^^^  inh Check  ^^^^  tp :: Type          -- possibilities for |beta|  
    sig Infer  ^^^^  ^^^^  syn Infer  ^^^^  tp :: Type          -- note the inh/syn difference
    \end{code}
    The handle is expressed by a GADT:  %%% common knowledge not worth a citation  ~\cite{jones06}:
    \begin{code}
    data Handle a :: * -> * ^^^^ where  ^^^^  HandleInfer :: Handle Infer
                                              HandleCheck :: Handle Check
    \end{code}
    The context-dependent tail visit function can now be written as:
    \begin{code}
    sem :: forall beta (Validate beta)
      tail  ^^^^  case lhsattr h of
                    HandleInfer  -> sem :: Infer  ^^^^ lhsattr tp = ...
                    HandleCheck  -> sem :: Check  ^^^^ ... = lhsattr tp
    \end{code}
    The GADT matches on the |Handle beta| constructors is a proof that the type |beta| is actually
    of the type |Infer|, respectively |Check|, and thus we are allowed to write a |sem|-block
    with a more specific type in the context where this match is performed.
    %% %% Not needed for this example anymore, but in general nice to have:
    %% To facilitate this, the translation given in the previous section becomes slightly more complicated
    %% as the matches with booleans have to become nested case statements to convince the Haskell type checker.

    As another example, Appel~\cite{DBLP:books/cu/Appel1998} introduces expression kinds for
    code generation of boolean expressions in different contexts.
%%    As another example, Appel~\cite{DBLP:books/cu/Appel1998} introduces expression kinds in Chapter 7.2 to
%%    depending on the context, generate code for MiniJava based on the use in a statement, expression or relation %%context. In the latter case, two extra inherited attributes are used to carry labels.

  
  \subsection{Sharing, Memoization, and Bounded Static Variation}
    When the values for the inherited attributes are taken from a finite domain, we can play the bounded static variation trick~\cite{153676}.
    All possible results can be lazily
    precomputed by changing the translation of a semantics block to:
    \begin{code}
    let  imp  = ...  -- conventional sem-translation
         arr  = array [ (toIndex key, imp (sub v 1) ... (sub v k)) | key@((sub v 1),...,(sub v n)) <- enumValues ]
    in S (\ (sub i 1) ... (sub i n) -> arr ! toIndex ((sub i 1),...,(sub i n)))
    \end{code}
    This particular scheme ensures that sharing is retained when invoking this visit function
    several times with exactly the same inputs. This is beneficial when the computation of synthesized
    attributes is expensive in time or space.
  
    \subsection{Aggressive Optimization}
    \label{sect.visit.aggressiveoptimization}
      We define |strict sem :: ...| as a semantics block with a different evaluation model.
      We demand that values for the inherited and synthesized attributes
      of that visit are not allowed to be |undefined|. This is a stronger demand than requiring the visit
      to be strict in all its inherited attributes.

      Then, following Kastens~\cite{DBLP:journals/acta/Kastens80}, 
      if in this case the graph of static attributed call graph is non-cyclic in the attributes, the
      dependency relation between attributes defines a partial order on the attribute computations. We obtain
      a total order by giving precedence to the attribute that occurs earlier
      in the source code. We can then compute the attributes strictly in the resulting order,
      resulting in the construction of fewer closures and more control over memory retainment,
      as deferred computations keep otherwise unused memory alive.
      %% The ideas in this paper can thus be integrated in languages without lazy evaluation.
      %% Measurements with the editor Proxima
      %% no space for citation ~\cite{Schrage04proxima}
      %% showed drastic performance improvements.


%%    \subsection{Clauses}
%%    When different cases have a common tail, we can factor out the common functionality:
%%    \begin{code}
%%    sem :: S  ...  ^^^^ -- statements for all clauses
%%              clause  ... ^^^^ -- statements
%%              clause  ... ^^^^ -- statements
%%              tail ...
%%    \end{code}
%%
%%    When we mark the signature as |total|, we get rid of the Maybe data type.

%%  \subsection{Other Result Types}
%%
%%  We now return a Maybe-tuple as result type, where nothing encodes failure and
%%  just the values we compute in the non-failure case. We can also see this differently:
%%  the callee makes a decision: in the failure case it decides to return a value without
%%  any results, and in the other case it returns a value with many results.
%%  The caller must handle these cases.
%%  We can generalize this by letting the callee choosing a data type and data constructor
%%  to be used as return value and requiring the caller to deal with all these cases.
%%  In case of an error, for example, the callee could return more information than just
%%  a plain "Nothing" value.

  \subsection{Practice}
  \label{sect.visit.practice}
%% Experience with UHC and the need of aspect-oriented programming and copy rules.
%%
%% Doaitse:
%% je zou nog kunnen zeggen dat deze hele exercitie gebaseerd is op de ervaring bij het gebruik van AG's in de UHC, en dat dit eenstap voorwaarts is die een patroon afdekt dat veel voorkomt en tot dusvvere nog niet lekker met AG's liep. merk ook op dat een en ander een conservatieve uitbreiding van AG's is, en dat we hhet bestaande AG formalisme hie rin in kunnen bedden.
  We use attribute grammars extensively in the Haskell compiler UHC~\cite{1596650}.
  We rely heavily on the separation of concerns offered by attributes, in combination with
  copy rules to keep the implementation of this large compiler feasible.
  The work presented in this paper is a conservative extension of AGs; hence, we made a step
  forward to abstract from often occurring patterns that we could not express easily with AGs before.


\section{Related Work}
\label{sect.visit.relatedwork}

  Attribute grammars were invented by
  Knuth~\cite{DBLP:journals/mst/Knuth68}
  to define the semantics of context-free languages.
  AG evaluators recently regained popularity in Java~\cite{DBLP:journals/entcs/WykBGK08,DBLP:conf/oopsla/EkmanH07},
%% some of them
%%  recent~\cite{DBLP:journals/entcs/WykBGK08,DBLP:conf/oopsla/EkmanH07}\cite{uuagc}.

  Several attribute grammar techniques are important to our work.
  Kastens~\cite{DBLP:journals/acta/Kastens80} introduced ordered attribute
  grammars. In OAGs, the evaluation order of attribute
  computations as well as attribute lifetime can be determined statically,
  making severe optimizations possible (Section~\ref{sect.visit.aggressiveoptimization}).
  Related are Kennedy et al.~\cite{DBLP:conf/popl/KennedyW76} and
  Kuiper et al.~\cite{Kuiper87usingattribute}.

  Vogt et al.~\cite{DBLP:conf/pldi/VogtSK89} introduced higher-order
  attribute grammars. Computed attributes in such AGs can be made part
  of the tree and decorated with attributes themselves. 
  Our approach supports these higher-order attributes naturally, and even treat
  the semantic functions themselves first class.

  Saraiva et al.~\cite{Saraiva99} described in Chapter 3 multiple traversal functions as a technique
  to implement attribute grammars with a purely functional programming
  language. The visit function model proposed in this paper is directly
  based on this technique, as well as the concepts of
  generic attribute grammars in Chapter 5.
  Novel in our work is the use of contexts (Section~\ref{sect.visit.contexts}),
  and the embedding of visit functions inside visit functions.

  Boyland~\cite{DBLP:journals/toplas/Boyland96} treated the problem that choosing
  a wrong pattern match order may result in cyclic computations. He defined
  conditional attribute grammars, and showed a similar approach as
  Kastens~\cite{DBLP:journals/acta/Kastens80} on how to order the pattern matches.
  Finding orders are NP-hard problems or worse. Fortunately, in our case,
  the programmer defines the global order, which simplifies the analyses.
  In fact, for visit functions, the order-analyses have a polynomial complexity bound.

\section{Conclusion}
\label{sect.visit.conclusion}

  We introduced a programming model for visit functions, intended to write
  executable versions of many forms of semantics of programming languages,
  e.g. type inferencers, evaluators and code generators.
  This programming model is essentially a higher-order attribute grammar
  on the static one-level call tree of the visit functions.
  This model allows us to express case distinction on multiple abstract
  syntax trees, and express the order of non-local data flow.

  We intend to apply these visit functions to several problems.
  In the field of type systems, we represent executable versions of
  relations as visit functions. Cases for these functions can be added
  during execution, locally defined in the scope of some other visit function.
  For example, we represent environments \emph{intentionally} in
  terms of a lookup visit function (or even different operations using
  the contexts of Section~\ref{sect.visit.contexts}).
  Due to the ease of adding extra attributes to such a function,
  we establish data exchange between use and call site, which is normally
  difficult because these sites can be far away in the AST.

  Furthermore, we intend to model the semantics of context reduction,
  which is used to resolve overloading in Haskell's type system, 
  with visit functions in the presence of several type class extensions,
  such as overlapped instances. Earlier we had to resort to external
  constraint solvers because attribute grammars are not expressive
  enough.
  
  Also, we intend to model the semantics of parser combinators~\cite{DBLP:conf/lernet/Swierstra08}
  in terms of visit functions. Currently, writing
  certain analysis on the internal representation is hard due to the
  amount of boilerplate code that has to be written. We expect to
  generate most of this boilerplate code by using visit functions.
  For this particular problem, the sharing optimization and contexts
  are a requirement.

  %% Finally, due to the aggressive optimizations applicable to visit
  %% functions, a direction of future work is to perform a flow analysis
  %% on (possibly cyclic) Haskell functions to detect if these can be
  %% written as visit functions.

  \bibliographystyle{entcs}
  \bibliography{references}

\end{document}