\documentclass[preprint,natbib]{sigplanconf}

%include lhs2TeX.fmt
%include polycode.fmt

\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{amsthm}
\usepackage{stmaryrd}
\usepackage{txfonts}
\usepackage{float}
\usepackage{mathpartir}
\usepackage{xcolor}
\usepackage{natbib}
\usepackage[pdftex]{graphicx}

\floatstyle{boxed}
\restylefloat{figure}


%format ^^^^ = "\hspace{1em}"
%format ^^^ = "\;"
%format . = "."
%format mid = "\mid"
%format dot = "\;.\;"
%format comp = "\circ"
%format :- = "\vdash"
%format ~> = "\leadsto"
%format vdashe = :- "_" e
%format vdashp = :- "_" p
%format vdashphat = :- "_{\hat{p}}"
%format p0
%format p1
%format p2
%format e0
%format e1
%format e2
%format f1
%format fi = f "_" i
%format fn = f "_" n
%format ty = "\tau"
%format x0
%format x1
%format x2
%format xn = x "_" n
%format ty0
%format ty1
%format ty2
%format ty3
%format env = "\Gamma"
%format env0
%format env1
%format env2
%format envl = env "_" l
%format envg = env "_" g
%format ctx  = "\delta"
%format ctxallow = "+"
%format ctxdisallow = "\times"
%format pat = "p"
%format phat = "\hat{p}"
%format phat0
%format phat1
%format phat2
%format inferPhat = infer "\hat{P}"
%format === = "\hrulefill"
%format fbox (a)   = "\fbox{\ensuremath{" a "}} \hspace{1em}"
%format overlinea = "\overline{" a "}"
%format overlinec = "\overline{" c "}"
%format overlinep = "\overline{" p "}"
%format overlines = "\overline{" s "}"
%format boxx      = "\fbox{\ensuremath{" x "}} "

%% Ruler formats
%format relation   = "\mathsf{relation}"
%format derivation = "\mathsf{derivation}"
%format syntax     = "\mathsf{syntax}"
%format keywords   = "\mathsf{keywords}"
%format input      = "\mathsf{input}"
%format output     = "\mathsf{output}"
%format inputs     = "\mathsf{inputs}"
%format outputs    = "\mathsf{outputs}"
%format branch     = "\mathsf{branch}"
%format def        = "\mathsf{def}"
%format exec       = "\mathsf{exec}"
%format eval       = "\mathsf{eval}"
%format fresh      = "\mathsf{fresh}"
%format visit      = "\mathsf{visit}"
%format let        = "\mathsf{let}"
%format inst       = "\mathsf{inst}"
%format as         = "\mathsf{as}"
%format establish  = "\mathsf{establish}"
%format innername  = "\mathsf{innername}"
%format dispatch   = "\mathsf{dispatch}"
%format external   = "\mathsf{external}"
%format merge      = "\mathsf{merge}"
%format inherit    = "\mathsf{inherit}"
%format seal       = "\mathsf{seal}"
%format abstract   = "\mathsf{abstract}"
%format hide       = "\mathsf{hide}"
%format skip       = "\mathsf{skip}"
%format case       = "\mathsf{case}"
%format of         = "\mathsf{of}"
%format in         = "\mathsf{in}"
%format if         = "\mathsf{if}"
%format then       = "\mathsf{then}"
%format else       = "\mathsf{else}"
%format requires   = "\mathsf{requires}"
%format exposes    = "\mathsf{exposes}"
%format augment    = "\mathsf{augment}"
%format first      = "\mathsf{first}"
%format last       = "\mathsf{last}"
%format all        = "\mathsf{all}"
%format any        = "\mathsf{any}"
%format succ       = "\mathsf{succ}"
%format pred       = "\mathsf{pred}"
%%% %format this       = "\mathsf{this}"
%format none       = "\mathsf{none}"

%% Haskell formats
%format hlet   = "\mathbf{let}"
%format hin    = "\mathbf{in}"
%format hif    = "\mathbf{if}"
%format hthen  = "\mathbf{then}"
%format helse  = "\mathbf{else}"
%format hfresh = "fresh"
%format hcase  = "\mathbf{case}"
%format hdo    = "\mathbf{do}"
%format unknown(i) = ? "_" i


\newcommand\LamPat{\scshape LamPat\normalfont}
\newcommand\Ruler{\scshape Ruler\normalfont}

\newcommand\url[1]{\tt{#1}}

\begin{document}

\conferenceinfo{TLDI '10}{January 23, 2010, Madrid.}
\copyrightyear{2010}
\copyrightdata{[to be supplied]}

% \titlebanner{banner above paper title}        % These are ignored unless
\preprintfooter{Aspect-Oriented Programming with Type Rules}   % 'preprint' option specified.

\title{Factoring Type Rules Into Aspects}

\authorinfo{Arie Middelkoop\and Atze Dijkstra\and S. Doaitse Swierstra}
           {Universiteit Utrecht}
           {\{ariem,atze,doaitse\}@@cs.uu.nl}

\maketitle


\begin{abstract}
Type systems are typically specified with type rules (suitable for formal
analysis and explanation), but sometimes also directly as an executable
Haskell program. Most properties (especially declarative) are more
concisely expressed with type rules. Some recurring specification patterns,
however, are more easily expressed in Haskell.

We present \Ruler, a language for expressing aspect-oriented type rules,
a best-of-both-worlds combination of both type rules and abstractions offered
by Haskell.
\end{abstract}

\category{F.3.1}{Logics and Meanings of Programs}{Specifying and Verifying and Reasoning about Programs}
\terms{Algorithms, Languages}
\keywords{Type system, type rules, inference algorithm, aspect-oriented programming}

\section{Introduction}
\label{sect.aspect.introduction}

  Type systems specify which terms in a programming language are valid by
  relating types to them.
  In our experience with the Haskell compiler UHC, a wide gap exists between
  the type system (used for formal reasoning and explanation) and its
  associated inference algorithms (written in Haskell). This gap is undesirable,
  as it makes consistency between specification and implementation hard to
  enforce.
  
  There are several proposals (Section~\ref{sect.aspect.relatedwork}) for closing this gap (including
  our previous work on Ruler~\cite{DBLP:conf/flops/DijkstraS06}) by increasing the expressiveness
  of programming languages, such that the algorithms resemble the rules more.
  
  In this paper, however, we approach the problem from the other direction:
  we propose an aspect-oriented formulation of type rules, such that the rules
  better resemble the algorithms.
  
  \paragraph{Motivation.}
  A type system can be fully specified by type rules, but those rules are
  at most a partial specification of an inference algorithm. An inference algorithm
  itself could have been a specification for type rules, but is generally too
  precise (and thus too verbose) as such. Hence, specifications and implementations
  are typically written in different formalisms, leaving the question open whether
  the inference algorithm does what the type system describes.
  
  More precisely, the inference
  algorithm must be {\it sound} with respect to the type system (i.e.
  never infer a ``wrong'' type), is preferably {\it complete} (i.e. infers a
  type when there is one), and infers {\it principal types} (i.e. if there are
  multiple types possible, it finds the most general one).
  
  Proving these properties can be done for small type systems that are dealing
  with one particular language feature, but is infeasible for complex
  type systems in which many language features interact, such as the Haskell
  type system~\cite{DBLP:journals/jfp/Faxen02}.
  
  In such a practical setting, the best we can hope for is too share
  as much as possible between the type system and inference algorithm. Those
  corresponding parts cannot be different, thus providing a weaker form of
  consistency, more based on sound engineering.
  
  Our goal is to write the inference algorithm as type rules extended with
  a minimal amount of additional code~\cite{DBLP:conf/flops/DijkstraS06}.
  Many proposals are made to increase
  expressiveness of programming languages, such that less additional code is
  needed. However, there are some abstractions in the implementation language
  that clash with the type rule formalism, because these abstractions cannot be
  expressed there. In particular, with Haskell's reader and writer monads, generic
  parameter passing behavior can be concisely expressed, and certain monadic
  combinators allow interaction between parameters to be expressed in isolation.
  
  In this paper, we see typing relations as the composition of partially
  specified relations, each dealing with a particular combination of the
  parameters of the type rules in isolation. With abstract judgments and
  abstract terms, we specify generic equational behavior between the
  term variables of the rules.
  
  \paragraph{Contributions.}
  More precisely, our contributions are:
  
  \begin{itemize}
  \item We first provide evidence to our claim that type rules lack
        expressiveness. In Section~\ref{sect.aspect.example} we give
        a type system which we will use to illustrate our point, and in 
        Section~\ref{sect.aspect.haskell} we give two different inferencers
        for the type system. The first inferencer
        is derived directly from the type rules, and the second one is crafted
        by hand. This second inferencer is more concise, and we point out what
        is missing in the type rules that causes this difference.
        
        For example, the following snippets from Section~\ref{sect.aspect.haskell1} and
        Section~\ref{sect.aspect.haskell2} show that the |envg| environment is
        explicitly passed in the first inferencer, whereas its description is
        separated into a monad the second inferencer. We further explain this in
        Section~\ref{sect.aspect.haskell}.
        
        \begin{code}
        infer :: .. Env -> IO Ty      ^^^^   infer :: .. ReaderT Env IO Ty
        infer (App f a) envg          ^^^^   infer (App f a)
          = do  .. <- infer f envg    ^^^^     = do  .. <- infer f
                .. <- infer a envg    ^^^^           .. <- infer a
        \end{code}
        
  \item We present an aspect-oriented and executable formulation of our example in
        Section~\ref{sect.aspect.rulerexample}. We split the typing relation in
        smaller relations that we call {\it aspect relations}. These aspect
        relations have partial partial rules. A weaving mechanism combines the
        rules back into a full typing relation. The rules may have abstract
        judgments and terms, which are instantiated during the weaving process
        to concrete judgments and terms.

        For example, the first of the following partial rules mentions the term variable
        |envg|. The first judgment is an abstract judgments that is applicable
        to any judgment of the given form, that is, can be specialized to any
        judgment having a global environment parameter |envg|.
        The second rule shows the abstract
        term |all.envl|. This abstract term is specialized with a list of
        the terms of all judgments with a local environment parameter |envl|. 

        \begin{mathpar}
        \inferrule
          { |any: envg :- | }
          { |envg :- | }
        
        \inferrule
          { \\ }
          { | unions all.envl :- | }
        \end{mathpar}
        
        Partial rules can be grouped to form aspect relations and
        be combined by weaving, which must be defined explictly with several
        built-in weaving functions.
        For example, we construct a full typing relation by merging individual
        aspect relations, and sealing the result to resolve dependencies between
        the individual parts and eliminate the abstract judgments and terms, in
        a particular order based on inheritance. Overlapping judgments of the
        inheriting relation overrule those of the inherited relation.

        \begin{code}
        let  tpRelation   =  seal (  merge  exprAspect envAspect
                                            typeAspect )
             envAspect    =  inherit envExplicit envImplicit
             envExplicit  =  relation envg :: Env
                               .. -- rules and abstract judgments
        \end{code}

  \item We formalized the above ideas and present \Ruler{} in
        Section~\ref{sect.aspect.ruler}, a language for aspect-oriented
        and executable type rules. A tutorial~\cite{arie09} and an
        interpreter~\cite{arie092} for the language are available on the web.
  \end{itemize}

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

  Given a type system, two typical questions are raised, namely whether the
  type system satisfies some correctness properties, and whether a sound and
  complete inference algorithm exists.
  We partition the related work based on what question it aims to answer.
  
  \subsection{Formal Analysis}
  
  Much research is carried out to improve formal analysis of type rules.
  Given a language, type system, and operational semantics, properties such
  as type safety and principal types are obvious question to pose and try to
  answer. Many case studies are
  carried out to prove properties of type systems in various theorem provers,
  such as Coq~\cite{DBLP:journals/corr/abs-cs-0603118},
  Twelf~\cite{DBLP:conf/tphol/Schurmann09},
  and Isabelle~\cite{DBLP:conf/tphol/WenzelPN08}.

  Many of the proofs for properties of type systems require induction and case
  distinction based on the structure of the rules, expressions and types.
  A type system can be described in Ott~\cite{DBLP:conf/icfp/SewellNOPRSS07},
  which then generates the formalization for such theorem provers, and some
  inductive helper functions. SASyLF~\cite{1411266} is a similar proof
  assistant tailored for type systems, intended for education.
  
  Some theorem provers (Twelf and Isabelle for example) can generate an
  inference algorithm for (executable) specifications. However, as we put forward
  in this paper, these type system specifications lack abstraction, and
  due to the verbosity of the formalism soon become very large and difficult to
  keep an overview of. Also, efficiency and interoperability is typically a
  problem with the generated algorithms (backtracking search), limiting its
  practical use to experimentation.

  Many properties such as contracts~\cite{DBLP:conf/popl/XuJC09}) and
  their proofs are relatively local. The aspect-oriented type rule formalism
  we present in this paper, may therefore be beneficial in such problem domains.
  For properties that span the entire type system
  (i.e. global invariants), the conventional proof tactics of proof
  assistants (like Coq) may need to have some notion of the individual aspects
  of the type system specification, because for big systems the term in the
  underlying theory quickly grows too large to manipulate.

  
  \subsection{Inference Algorithms}
  
  For some type systems, no sound and complete inference algorithm
  exists~\cite{859871}. For others clean and concise algorithm exists, such as
  the Hindley-Damas-Milner system and the algorithm of Milner~\cite{Milner78atheory}, which forms the
  basis of inference algorithms for Haskell and ML. In other cases, the
  inference algorithm is a hybrid approach between type checking and type
  inference, either by having an incomplete inference algorithm, or by
  enforcing and exploiting the presence of type annotations in the language at
  hand~\cite{DBLP:conf/icfp/VytiniotisWJ08}\cite{DBLP:conf/popl/Leijen09}.
  
  Concise inference algorithms can be written using techniques from Prolog, or
  more recently, Functional Logic Programming~\cite{DBLP:journals/jlp/Hanus94}.
  Constraint Handling Rules~\cite{DBLP:conf/iclp/Schrijvers08} is a popular
  implementation technique for search algorithms. This is particularly
  useful for non-deterministic parts of the type system.
  However, for those parts that are deterministic, conventional tree traversals
  are preferable because of efficiency and better integration with all the
  other aspects a compiler has to deal with.
  
  Sulzmann~\cite{Sulzmann00ageneral} presents HM(X)~\cite{DBLP:journals/jfp/SulzmannS08},
  a general framework for Hindley-Milner style type systems.
  It is based on a fixed set of type rules parameterized over some relation |X|,
  for which an inference algorithm needs to be given to obtain an inferencer for
  the full language.
  
  These above approaches are at least as verbose as type rules.
  Recurring patterns in type rules are thus also recurring patterns in
  the inference algorithms. HM(X) deals with some recurring patterns limited to
  Hindley-Milner, but does not provide a general mechanism.

  Closer to the extensions that we propose is TinkerType~\cite{DBLP:journals/jfp/LevinP03}.
  TinkerType is a framework for the
  compact and modular descriptions of type systems (and other deductive systems).
  In TinkerType, rules are given independently, and associated with each rule is
  a concrete piece of inference code for this rule and a list with the names
  of language features for which this rule is applicable.
  An assembler glues the individual
  pieces of code together based on the features the language designer is
  interested in, using a fixed weaving algorithm.
  An essential difference between our work and theirs is that we provide a finer
  level of granularity, namely combinations of individual parameters of a relation,
  potentially spanning multiple rules. Also, we provide abstract judgments and
  terms, allowing generic behavior to be defined over arbitrary rule structures.
  Finally, we require an explicit definition of how the aspects are woven
  together, with a couple of built-in relations. TinkerType's implicit weaving
  algorithm based on features is an orthogonal idea, that could be build on
  top of our weaving mechanism.
  
  The work we present here is an extension of previous work done on \Ruler{}
  by \citet{DBLP:conf/flops/DijkstraS06}. In this previous work, typing
  relations are defined in incremental steps in a hierarchy. For example,
  the first typing relation is a syntax-directed version of a declarative
  type system. Then, with each increment, extra parameters can be added
  to the typing relations, extra judgments to the rules, and extra terms to
  the judgments. Two additional mechanisms make the specification executable:
  adding direction to the parameters (making
  them inputs or outputs) turns the relations into functions, and secondly,
  a mechanism for external relations in Haskell makes the specification executable.
  In this way part of the type system of a full Haskell compiler has been described in
  a compositional and incremental way~\cite{DBLP:conf/afp/DijkstraS04}\cite{atze:phd}.
  This paper presents an extension of this approach by including
  abstract judgments and abstract terms for generic behavior over the structure
  of rules (eliminating the need for writing many trivial terms), and
  full-aspect oriented modularity, instead of stacking increments.
  
  Our idea of abstract judgments and abstract terms arose from type inferencer
  specifications with attribute grammars~\cite{DBLP:conf/afp/DijkstraS04}.
  Attribute grammars associate with each node in the abstract syntax tree a
  number of input and output attributes, and defines relations between these
  attributes, usually in the form of functions. 
  The UUAGC system\footnote{\url{http://www.cs.uu.nl/wiki/HUT/AttributeGrammarSystem}}
  allows these
  functions to be written as a collection of separate fragments, which are
  collected by the system, analysed together, and out of its composition a
  tree-walk evaluation is constructed. Most of the trivial functions can be
  omitted, and are filled in by so called copy-rules. Our abstract judgments and
  terms play a similar role in the type rule specifications.
  
  \citet{meijerjeuring95} did show the connection between
  monads and attribute grammars. Recently, \citet{1596586} showed
  how to encode attribute grammars directly in Haskell, and express |Reader|,
  |Writer| and |State|-like programming patterns. Thus, it is not surprising
  that there is a strong connection between aspect-oriented type rules,
  attribute grammars and monadic abstraction.
  
  \begin{figure}[htp]
  \begin{code}
        -- expressions
  e     =    i          -- integer
        mid  x          -- variable    
        mid  C          -- constructor
        mid  \pat . e   -- lambda with pattern
        mid  e1 e2      -- application
  ^^^
        -- patterns
  pat   =    x            -- simple pattern binding
        mid  <phat>       -- complex pattern
  phat  =    phat pat     -- pattern application
        mid  C            -- constructor
  ^^^
        -- types
  ty    =    T            -- first order type constructor
        mid  ty1 -> ty2   -- function type constructor
  ^^^
        -- 
  \end{code}
  With lower case identifiers |x|, integers |i|,
  constructors |C `elem` {S, P}|, and type constructors
  |T `elem` {Int, Single, Pair}|.
  \caption{\LamPat, a lambda calculus with lambda patterns.}
  \label{aspect.example.lambda}
  \end{figure}

\section{Running Example}
\label{sect.aspect.example}

% Reasons for using the running example
%   * conceptually simple type system
%   * complex type system due to abstract syntax, parameters

  In this section, we introduce the language \LamPat: the simply-typed
  lambda calculus, extended with lambda patterns and data constructors.
  We use \LamPat{} as a running example throughout this paper to demonstrate the specification of its semantics by means of Ruler.
  The bindings introduced by lambdas in this language
  use a pattern expression instead of a formal parameter.
  The type system we
  define for \LamPat{} looks simple at first sight, but is actually quite complex due to extra
  abstract syntax and typing relations with more parameters in \LamPat. A typical functional
  language has many of such extensions on the lambda calculus; after
  this example, it is not hard to imagine that type systems for mainstream
  functional languages are even more complex.
  
  First we give a couple of examples, then give the syntax of the language,
  and finally a static semantics. We omit a discussion of the operational
  semantics, and neither concern ourselves with proving progress and
  preservation properties, as these are outside the scope of this paper.
  
  \subsection{Examples}
  \label{sect.aspect.language.example}

% Example expressions
  Consider the following data type declarations:
  \begin{code}
  data Single  where  S ::         Int  -> Single
  data Pair    where  P :: Int ->  Int  -> Pair
  \end{code}
  We wrote these data type declarations in GADT-style. We assume these and only
  these data types to be available in the \LamPat{} language. 
  
  The following \LamPat{} expressions demonstrate what is and what is not a valid
  \LamPat{} expression. Consider them in the context in which the above data types
  are defined.
  \begin{code}
  \(S x) dot x            -- Ex1: OK
  \(x y) dot x            -- Ex2: disallow pattern functions
  \(P x x) dot x          -- Ex3: duplicate occurrence of |x|
  \S dot 3                -- Ex4: under-saturated pattern
  \(S x y) dot x          -- Ex5: over-saturated pattern
  (\(S x) dot x) (P 3 3)  -- Ex6: type error 
  \end{code}
  The first expressions corresponds to a function that takes one parameter,
  pattern matches on the |S| constructor to access the value and binds it to |x|, and
  returns this value. The remaining expressions have invalid patterns for various reasons. The
  last three examples contain type errors. In example four, the pattern containing
  S is not fully saturated, since the type of the pattern should be |Single|,
  but it is |Int -> Single|. In example five, |S| appears to be a
  constructor with type |Int -> ... -> Single|, but its signature specifies
  otherwise. In example six, we apply a function that expects a |Single| to a
  |Pair|.
  
  \subsection{Static Behavior}
  
  We define a grammar and type system to enforce the following static behavior:
  \begin{itemize}
  \item All variables that occur in an expression are bound in a pattern in an
        encapsulating lambda. Free variables are disallowed, with the exception
        of those introduced by the global environment. 
  \item All patterns should start with a constructor introduced by a data-type
        declaration. We disallow pattern functions.
  \item No duplicate occurrences of variables in a pattern (third example).
  \item Pattern expressions must be fully saturated (fourth example), by
        allowing an outermost arrow type constructor only for patterns that are
        single variables.
  \item The type of the pattern and variables must match their use (last two
        examples).
  \end{itemize}
  The second item is enforced by the grammar, the other items by the type
  system.

  \subsection{\LamPat{} Syntax}

  Figure~\ref{aspect.example.lambda} lists the grammar of expressions,
  pattern expressions and types. The grammar is largely based on the simply
  typed lambda calculus, except that lambda expressions contains a pattern |p|
  instead of just an identifier |x|. Furthermore, we allow a couple of
  zero-order type constructors (|Int|, |Single| and |Pair|).
  
  Patterns mimic the syntax of expressions. Similarly to a function call, we
  encode the match on a constructor with a number of pattern applications, which
  are left associative.
  There are two nonterminals for patterns, |pat| and |phat| respectively. Since
  a |phat| cannot be a single variable, we enforce that a series of pattern applications
  start with a constructor. Furthermore, the switch from |pat| to
  |phat| is explicit in the abstract syntax, which occurs always above a
  series of pattern applications. This property we exploit in the type rules to
  enforce saturated constructor matches.
  For example, the pattern |P (S x) (P y z)| is encoded as
  %format <  =  "<\!\!"
  %format >  =  "\!\!>"
  %format >> =  ">>"
  |<(P <S x>) <(P y) z>>|, where we made the switch from |pat| to |phat|
  explicit with brackets.

  \subsection{Static Semantics}
  \label{sect.aspect.example.rules}

  \begin{figure}[htb]
  \begin{mathpar}
  \fbox{\ensuremath{|envg vdashe e : ty|}}\\
  
  \inferrule*[right=e.int]
    { }
    { |envg vdashe i : Int| }

  \inferrule*[right=e.var]
    { |(x :: ty) `elem` envg| }
    { |envg vdashe x : ty| }
 
  \inferrule*[right=e.con]
    { |(C :: ty) `elem` envg| }
    { |envg vdashe C : ty| }

  \inferrule*[right=e.app]
    { |envg vdashe f : ty1 -> ty2| \\
      |envg vdashe a : ty1|
    }
    { |envg vdashe f a : ty2| }

  \inferrule*[right=e.lam]
    { |envg ; envl vdashp p : ty1| \\
      |envl envg vdashe e : ty2|
    }
    { |envg vdashe \p . e : ty1 -> ty2| }
  
  \end{mathpar}
  
  \begin{mathpar}
  \fbox{\ensuremath{|envg ; envl vdashp p : ty|}}\\
  
  \inferrule*[right=p.var]
    { |(x :: ty) `elem` envl| }
    { |envg ; envl :- x : ty| }
  
  \inferrule*[right=p.top]
    { |envg ; envl vdashphat phat : T| }
    { |envg ; envl vdashp phat : T| }
  
  \end{mathpar}
  
  \begin{mathpar}
  \fbox{\ensuremath{|envg ; envl vdashphat phat : ty|}}\\
  
  \inferrule*[right=p.con]
    { |(C :: ty) `elem` envg| }
    { |envg ; envl vdashphat C : ty| }
  
  \inferrule*[right=p.app]
    { |envg ; env1 vdashphat phat1 : ty1 -> ty2| \\
      |envg ; env2 vdashp p2 : ty1| \\
      |env1 # env2|
    }
    { |envg ; env1 env2 vdashphat phat1 p2 : ty2| }
  \end{mathpar}
  \caption{Pattern and expression rules.}
  \label{fig.aspect.example.rules}
  \end{figure}
  
  Figure~\ref{fig.aspect.example.rules} lists the type rules for \LamPat.
  There are two essential differences with respect to the type rules of the
  simply typed lambda calculus~\cite{509043}.
  In rule \TirName{e.lam}, instead of extending
  the environment with some fresh type for the identifier of the lambda, we
  extend the environment with potentially many bindings, one for each
  variable occurring in the pattern. Furthermore, there is a judgment for
  typing patterns and defining the bindings for variables in these patterns.

  We consider the rules for patterns in more detail.
  The judgment of the form |envg ; envl :- p : ty| expresses that in
  global environment |envg|, the pattern |p| has type |ty|, with bindings of
  the variables of the pattern in the local environment |envl|.

  The rules mention two environments, each used differently:
  a global environment |envg| and a local environment |envl|. The global
  environment starts out with the type signatures for the data
  constructors |S| and |P|. The new bindings brought into scope by a pattern
  in the lambda extend the environment for the expression inside the lambda.
  These new bindings we represent with a local environment |envl|.
  The juxtaposition of |envg| and |envl| in rule \TirName{e.lam} represents the
  union of the two environments.

  Rule \TirName{p.var} states that the local environment has a binding for
  |x|, whereas rule \TirName{p.con} states the the global environment must have
  one for the data constructor. Hence, the local environment contains the types
  for variables occurring in the patterns, and the global environment types for
  variables in scope and for data constructors.
  
  Rule \TirName{p.top} requires pattern applications to be fully saturated.
  The type of the non-variable pattern must be a nullary type constructor |T|.
  In \LamPat, these are all types except for those with an outermost arrow.
  For example, the pattern consisting of a single |S| has type |Int -> Single|, which is not allowed.
  On the other hand, the pattern |P x y| has type |Pair| and falls in the
  syntactic category of types |T|.
  
  Rule \TirName{p.app} prevents duplicate occurrences of variables in a pattern
  by requiring that its two local environments (|env1| and |env2|, respectively)
  have disjoined domains (|env1 # env2|). For example, in pattern
  |P x x|, \TirName{p.app} on |P x| and |x| cannot be applied: the
  local environments for these two subparts have |x| in common. Furthermore,
  like the conventional \TirName{e.app} rule, the rule requires the argument
  type of the ``function part'' of the application to match the type of the
  argument part. In pattern |S x|, for example, the type for |S| is |Int -> Single|.
  Hence the type associated with |x| must be |Int|, and the type for the pattern as a whole
  is |Single|.


\section{Inference Algorithms for \LamPat in Haskell}
\label{sect.aspect.haskell}

  Similar to Jones~\cite{Jones99typinghaskell}, we give two inference algorithms
  for \LamPat{} in Haskell. The first algorithm we obtain by straightforwardly
  transforming the type rules (Section~\ref{sect.aspect.haskell1}). The
  second algorithm (Section~\ref{sect.aspect.haskell2}) is hand crafted, using
  reader and writer monads to abstract from trivial parameter and result
  passing. We discuss (Section~\ref{sect.aspect.haskell.discuss}) that the
  difference between the two algorithms corresponds to similar trivial
  relations between terms in type rules.

  % what types are we interested in?
  %  * most general type
  %  * smallest environment
  %  * placeholder types

  Type rules are at most a partial specification of an inference algorithm.
  In addition to the type rules, we specify that the inferencer gets the
  expression and initial environment as a given, and either infers the smallest
  environments and most general types that fit the type rules, or if there are
  no such environments or types, reports a type error.
  In case there are two or more unequal types for an expression, we assume that
  the smallest in terms of visual appearance is chosen.


\subsection{Structure-reserving Translation}
\label{sect.aspect.haskell1}

  \begin{figure}[htp]
  \begin{code}
  data Expr   =  EVar String | EInt Int | ECon String
              |  EApp Expr Expr | ELam Pat Expr
  data Pat    =  PVar String | PTop Pat
              |  PCon String | PApp Pat Pat
  data Ty     =  Int | Single | Pair | Ty -> Ty | unknown(i)
  \end{code}

  \begin{code}
  inferE :: Expr -> Env -> IO Ty
  inferE (EInt _) envg
    = return Int
  inferE (EVar x) envg
    = lookup x envg
  inferE (ECon c) envg
    = lookup c envg
  inferE (EApp f a) envg
    = do  ty1 <- inferE f envg
          ty2 <- inferE a envg
          ty3 <- hfresh
          unify ty1 (ty2 -> ty3)
          return ty3
  inferE (ELam p e) envg
    = do  (ty1, envl) <- inferP p envg
          ty2 <- inferE e (envl `union` envg)
          return (ty1 -> ty2)
  \end{code}

  \begin{code}
  inferP :: Pat -> Env -> IO (Ty, Env)
  inferP (PVar x) envg
    = do  ty <- fresh
          return (ty, singleton x ty)
  inferP (PTop phat) envg
    = do  (ty, envl) <- inferPhat phat envg
          checkT ty
          return (ty, envl)
  \end{code}

  \begin{code}
  inferPhat :: Pat -> Env -> IO (Ty, Env)
  inferPhat (PCon c) envg
    = do  ty <- lookup c envg
          return (ty, empty)
  inferPhat (PApp f a)
    = do  (ty1, env1) <- inferPhat f envg
          (ty2, env2) <- inferP a envg
          disjoined env1 env2
          ty3 <- fresh
          unify ty1 (ty2 -> ty3)
          return ty3
  \end{code}

  \begin{code}
  disjoined :: MonadError IOError m => Env -> Env -> m ()
  disjoined e1 e2
    =  hif null ( (keySet e1) `intersection` (keySet e2) )
       hthen return ()
       helse throwError $ userError "duplicate var"
  ^^^^
  checkT :: (MonadError IOError m, MonadIO m) => Ty -> m ()
  checkT ty
    = do  ty1 <- deref ty
          case ty1 of
            _ -> _   ^^^ -> throwError $ userError "not a T"
            _        ^^^ -> return ()
  \end{code}

  \caption{Main inferencer code.}
  \label{fig.aspect.example.code1}
  \end{figure}
  
  
  For a concrete implementation, we require extra information in addition to the
  type rules and what terms we are interested in, namely a definition of the
  data types, and code for relations not expressed with rules (i.e. lookup
  in the environment). We give the algorithm in Figure~\ref{fig.aspect.example.code1}
  and discuss below the above mentioned pieces of information in the figure.

% data types
%   * single AST for patterns
%   * The PTop constructor
%   * representing both environments with Env String Ty
%   * environment operations (lookup, union, empty and insert)

  \paragraph{Data types.}
  The data types correspond directly to the grammar we gave in the previous
  section, except that we collapsed patterns |pat| and |phat|. Therefore, where
  in the grammar there is a switch from |pat| to |phat| (that we indicated with
  brackets in some pattern examples in the previous section), there is
  an occurrence of |PTop| in the AST.
  
  The data type for types contains one extra alternative, a placeholder
  |unknown(i)|. These placeholders represent types that are not yet known during
  inference. The inference algorithm does not use them directly, but these are
  used internally by the operations |unify| and |hfresh| we explain
  later.

  We represent environments |Env| with a |Map String Ty|, and can use the
  conventional operations |lookup|, |union|, |empty| and |insert| to
  manipulate these environments.
  
% monadic inference
%   * 1 pass traversal
%   * inference monad (unification, fresh variables, throwing of errors)

  \paragraph{Monadic inference} Type inference is a stateful computation. Initially types are unknown
  (represented by place holders), and are gradually defined when matched against
  concrete terms. As is typical for these so-called syntax directed and
  deterministic type rules~\cite{509043}, the inference algorithm is essentially
  a one-pass traversal over the expression and patterns (the abstract syntax
  tree). For the \LamPat's simple type language, first-order unification suffices to
  infer types. However, the order of computation is important. Certain checks
  cannot be done too early, otherwise the required type information may not be
  available yet.
  
  Following Jones~\cite{Jones99typinghaskell} and many others that wrote
  type inferencers in Haskell, we write the inferencers in monadic style, using
  the following monadic operations:
  \begin{code}
  hfresh  :: MonadIO m => m Ty
  unify   :: MonadIO m => Ty -> Ty -> m ()
  deref   :: MonadIO m => Ty -> m Ty
  \end{code}
  |hfresh| introduces a fresh type in the form of a place holder. |unify|
  matches two types, potentially filling in place holders. If the two types
  cannot be unified, inference fails with an error. Finally, |deref| is the
  identity function, except that if a place holder is passed, it returns
  the contents of the place holder. We omit the implementation details of these
  monadic operations.
  
% the functions
%   * signature, inputs and outputs
%   * each rule a function alternative
%   * input terms, output terms, and fresh
%   * pattern matches and unify & judgements and relations

  \paragraph{Inference functions.}
  
  We translate each typing relation into a (monadic) function. Information that
  we may assume as given is input to such functions, and inferred information
  is an output. Hence, |inferE| gets an expression and global environment,
  and returns a type, while |inferP| in addition returns a local environment.
  
  Each type of judgment corresponds to a function, and each rule for a judgment
  typeto an alternative for this function. Each judgment corresponds to a
  function call. The results are produced in a monad supporting |MonadError|
  and |MonadIO| operations. In this example, we take the |IO| monad.
  The terms in the conclusion in the rule we translate to
  pattern matches on the inputs of the function, and to expressions for the
  output. Similarly, inputs of the judgments we translate to expressions, and
  outputs to pattern matches. However, for a pattern match we have two options:
  either we perform a Haskell pattern match, or use unification. With a Haskell
  pattern match, we check if a value has a certain structure and take action
  accordingly. With unification, we enforce such a structure.

  The order in which we translate judgments is important. In the
  |EApp| case, |ty1| and |ty2| must be defined before their use in the
  call to unify. Furthermore, when a type cannot be introduced before its
  use, we use |hfresh| to introduce it, as is the case with |ty3|.
  
  Following the requirement of obtaining a minimal local environment, we
  produce the smallest local environment that each rule permits. In rule
  \TirName{p.var}, the binding |x :: ty| must be in the local environment, hence
  we produce the singleton environment with this binding. Rule \TirName{p.top}
  demands that the environment is passed on unchanged. Rule \TirName{p.con}
  places no demands, hence we take the empty environment. Finally,
  \TirName{p.app} demands that we take the union of the two local environments.

% some relations not described by rules
%   * disjoined
%   * syntactical class and checkT

  Finally, there are some relations not described by rules, and we give an
  algorithm for those: |disjoined| returns an error if there is an overlap between the respective domains
  of the two environments, and |checkT| makes
  sure that its input is not an arrow-type. Since types can contain place
  holders, we have to use |deref| before the case analysis. However,
  we also need to ensure that this place holder is filled in before we
  dereference it. This is fortunately the case, because the type inferred for
  a |phat| is ultimately part of the signature for a constructor, which is
  always fully defined.

\subsection{Hand-crafted Translation}
\label{sect.aspect.haskell2}

  \begin{figure}[htp]
  \begin{code}
  type InferE a = ReaderT Env IO a
  type InferP a = ReaderT Env (WriterT Env IO) a
  \end{code}
  
  \begin{code}
  inferE :: Expr -> InferE Ty
  inferE (EInt _)
    = return Int
  inferE (EVar x)
    = lookup x
  inferE (ECon c)
    = lookup c
  inferE (EApp f a)
    = do  ty1 <- inferE f
          ty2 <- inferE a
          ty3 <- hfresh
          unify ty1 (ty2 -> ty3)
          return ty3
  inferE (ELam p e)
    = do  (ty1, envl) <- mapReaderT runWriterT (inferP p)
          ty2 <- local (envl `union`) (inferE e)
          return (ty1 -> ty2)
  \end{code}
  
  \begin{code}
  inferP :: Pat -> InferP Ty
  inferP (PVar x)
    = do  ty <- fresh
          tell (singleton x ty)
          return ty
  inferP (PCon c)
    = lookup c
  inferP (PTop p)
    = do  ty <- inferP p
          checkT ty
          return ty
  inferP (PApp f a)
    = do  (ty1, env1) <- listen (inferP f)
          (ty2, env2) <- listen (inferP a)
          disjoined env1 env2
          ty3 <- hfresh
          unify ty1 (ty2 -> ty3)
          return ty3
  \end{code}
  
  \begin{code}
    lookup :: (MonadError IOError m, MonadReader Env m) =>
                 String -> m Ty
    lookup x = do env <- ask
                  hcase lookup x env hof
                    Nothing -> throwError $ userError "undefined var"
                    Just ty -> return ty
  \end{code}
  
  \caption{Main inferencer code.}
  \label{fig.aspect.example.code2}
  \end{figure}
  
  We now turn to the hand crafted inferencer in Figure~\ref{fig.aspect.example.code2}.
  The traversal itself remains the same, but the code itself has become
  more concise.
  
  \paragraph{Reader Monad.}
        Parameters that are not essential to distinguish which function alternative
        to take are hidden in the |Reader| monad. In case of our example, this is
        the global environment. Hence, the parameter disappeared from the
        function definition and also does not have to be given with each
        call to |inferE| and |inferP|, and the call to |lookup|.
        
        The default behavior is locally overridden at those places where the default
        behavior is not suitable. For example, in the case for |ELam|,
        the global environment is extended with the inferred local
        environment, using the |Reader|-monad operation |local|\footnote{\url{http://www.haskell.org/all\_about\_monads/html/readermonad.html}}.
  
  \paragraph{Writer Monad.}
        Some results that are in the class |Monoid| (having a zero and a sum)
        can be hidden in the |Writer| monad. For these results, the default
        behavior is to take the sum of the values coming out of recursive calls,
        and use |zero| when there are none. This behavior can be overriden with
        Writer-monad operations\footnote{\url{http://www.haskell.org/all\_about\_monads/html/writermonad.html}}: |tell| to append a value, |listen| to
        access the hidden result, and |censor| to modify such a result.

        The monoid-instance for an environment computes the smallest
        environment that includes all the entries provided with |tell|.
        With |listen| and |censor| the hidden local environment can be
        accessed and manipulated in a relatively isolated way. We therefore
        hide the local environment, and |inferP| does not explicitly return this
        value anymore.

        The case for |PApp| uses |listen| to access the two local
        environments for the |disjoined| check.
  
  \paragraph{Aspect Orientation.}
    Monadic operations such as |local f (infer ..)|, allow overruling behavior
    to be specified in a relatively isolated way, by taking |f| as the
    composition of separate aspect-wise functions |f1 comp ... comp fn|, where each
    |fi| takes a record of the inputs and produces a potentially updated record.
    In our example, there is only one input |envg|, and |f| consists only of a
    single function that extends its actual parameter |envg| with the local environment.
  
  \paragraph{Complexity.}
  % discuss how this saved code
  % add a case for parentheses
  % discuss the many attributes of UHC
  The default behavior offered by the reader and writer monads are appropriate
  for many of the expression cases. Trivial propagation of inputs and outputs
  is factored out of the code. In fact, consider adding a case for parentheses
  to the grammar and a rule to type system which does not change the semantics.
  This rule is very verbose, since for every parameter of the typing relation,
  all terms in the conclusion of the rule are equated to their corresponding
  term of its single judgment. These are all trivial, hence can all be omitted
  in the reader-writer monad implementation.
  
  Our experiences with the Utrecht Haskell Compiler shows~\cite{1596650} that such
  abstractions pay off when dealing with more complex
  abstract syntax trees and with typing relations with more parameters.
  Inference functions in UHC have over twenty
  parameters, propagating environments for types and kinds, data structure
  information, constraints, and context information. In most cases, there is
  only an interest in a strict subset of all these parameters. Abstraction
  mechanisms, with similar functionality as the reader and writer monads shown
  in this section, take care of the rest. Indeed, at those places where the
  implementation is concise, the corresponding type rules are verbose.


\subsection{Discussion}
\label{sect.aspect.haskell.discuss}

% Monads are too implementation-specific for use in a specification
%   + switching from one reader type to another is annoying to write and
%     is not aspect-wise
% Which types to put in the monad and which as inputs and outputs?
%   not all types can be put in the writer monad (only monoids)
% design patterns

  The reader and writer monads are a useful abstraction mechanism when writing
  type inference algorithms. We would like to have this abstraction mechanism
  as well for type rules.
  
  We observe that the abstractions offered by the reader and writer monads
  correspond to {\it design patterns}. Typically, information is distributed
  from the top of the AST to the bottom, only modified along this process at
  a few places. Similarly, information is gathered from the bottom of the
  AST back to the top, and combined at each node in a universal way.
  
  Concrete reader and writer monads, however, are too algorithmic for use in a
  declarative specification as their fixes the traversal of the AST~\cite{meijerjeuring95}. 
  Also, with
  monads, parameters are treated differently when hidden in a monad or kept
  explicit as parameter of the relation. In general, it is easier to use an
  explicit parameter, and easier to pass around a hidden one. Hence, we want
  a mechanism that combines these two different conventions.
  Furthermore, we want to write the overruling code truly separately. The
  mechanism offered by |local| is too ``local''.

  Therefore, we take another approach than concrete reader and writer monads.
  We keep all parameters of the typing relation explicit, but split up a call to
  this relation (i.e. a judgment) in smaller pieces and use a weaving mechanism
  to compose them back into a single judgment. Each judgment-part refers
  to a subset of the parameters involved. Terms for parameters may be omitted.
  The weaving mechanism invents a fresh term for these parameters, and
  instantiates {\it generic judgments} to define them. For example, the
  environment-term of judgments is equated to the environment-term of the
  conclusion if it is missing (reader monad behavior), and the local-environment
  term of the conclusion is equated to some combination of the local-environment
  terms of the judgments if it is missing (writer monad behavior).
  We present this approach in the next section.


\section{\Ruler}
\label{sect.aspect.ruler}

  \begin{figure}[htb]
  \begin{code}
     -- expressions
  e  =    x                                 -- variable lookup
     mid  def x                             -- variable declaration
     mid  a.x                               -- field lookup
     mid  derivation overlinep overlinec    -- derivation declaration
     mid  external x overlinep              -- external derivation
     mid  (overlines; e)                    -- sequence
     mid  seal e                            -- finalize derivation
     mid  merge e1 e2                       -- merge two derivations
     mid  inherit e1 e2                     -- inherit from derivation
  ^^^
     -- statements
  s  =    x fresh                           -- introduce fresh term
     mid  e1 == e2                          -- unify two terms
     mid  establish e as f                  -- establish a subderivation
  ^^^
     -- parameter declaration
  p  =    input   x  :: ty                  -- input parameter
     mid  output  x  :: ty                  -- output parameter
  ^^^
  c  =    boxx overlines                    -- a rule
     mid  s                                 -- rule independent statement
  ^^^
     -- child identifiers
  a  =    f                                 -- concrete child name
     |    all | any | pred | succ           -- abstract child identifier
  \end{code}
  With identifiers |x| and  |f|.
  
  \caption{\Ruler{} core calculus.}
  \label{fig.aspect.ruler.core}
  \end{figure}
  
  We give a quick introduction to \Ruler, a language for aspect-oriented and
  executable type rules. For a more thorough explanation, see the ruler
  tutorial~\cite{arie09} and implementation~\cite{arie092}). We split the
  explanation in two parts. In this section we briefly discuss how to encode the
  type rules in the ruler core language by example, and show the aspect-oriented
  mechanisms in the next section. Many details of this core language are hidden
  behind syntactic sugar for type rules and lambda calculus, which we use in the
  next section.
  
  \paragraph{Syntax.}
  We give a small aspect-oriented core language for type rules in
  Figure~\ref{fig.aspect.ruler.core}. We used overbar notation to represent a
  vector.
  % AM: a vector of what? non-terminals? grammar-items? :P
  We first explain some of the syntactic
  constructs, and then given a example of a type rule in this language.
  Aside from type rules, also the lambda calculus can be embedded
  (which is also often used to specify small relations in type rules), but we
  omit these details.

  \paragraph{Derivation.}
  A |derivation| introduces an anonymous functional relation with zero or
  more input and output parameters. This relation is a conventional lambda if
  it has exactly one output.
  
  A derivation consists of one or more rules, each with a name and one or more
  judgments. The order of appearance of judgments does not matter.
  In contrast to type rules, there are only a limited number of
  fixed judgment forms (called statements), but with these statements,
  arbitrary judgments can be encoded.
  The statement |x fresh| introduces a fresh term. Given some relation |r| with
  parameters |x1,...,xn| specified by |e|, the statement |establish e as f|
  represents the type rule judgment |r(f.x1,...,f.xn)| with fresh terms
  |f.x1,...,f.xn|. Finally, the statement |e1 == e2| declares its two terms to
  be equal.
  
  %format fxfieldlookup =  "f.\:x"

  Expressions |e| specify terms. Both |x| and |def x| represent terms with the
  given name. The difference is that |x| requires the term to be defined, while
  |def x| specifies that the term is defined. The expression |fxfieldlookup| represents
  the term named |x| of established subexpression |f|.
  The sequence expression |(overlines; e)| represents
  a term specified by |e| and statements |overlines|.
  With |external|, any Haskell value (including functions and data constructors)
  can be represented as a relation. Relations are first class, in fact, the
  term language consist only of (possibly external) relations.
  Furthermore, all expressions have a type, and relations can be higher order,
  but we omit these details.
  
  %format marker1 = "\makebox[1em][l]{\color{darkgray}{$" envg vdashe \p . b : ty1 -> ty2 "$}}"
  %format marker2 = "\makebox[1em][l]{\color{darkgray}{$" envg ; envl vdashp p : ty1 "$}}"
  %format marker3 = "\makebox[1em][l]{\color{darkgray}{$" envl envg vdashe b : ty2  "$}}"
  
  \begin{figure}[htb]
  \begin{code}
  inferE  ==      derivation  input  envg :: Env, e :: Expr  output ty :: Ty
                     fbox (e.lam)  (elam (def p) (def b)) == this.e
  marker1                          this.ty  ==  P.ty -> E.ty
                                   ^^^
                                   establish inferP as P
  marker2                          P.envg  ==  this.envg
                                   P.p     ==  p
                                   ^^^
                                   establish this as E
  marker3                          E.envg  ==  (union ^^^ P.envl ^^^ this.envg)
                                   E.e     ==  b
  \end{code}
  \caption{Example translation to the core calculus.}
  \label{fig.aspect.ruler.core.example}
  \end{figure}
  
  \paragraph{Example.}
  Figure~\ref{fig.aspect.ruler.core.example} shows an encoding of the
  \TirName{e.lam} rule. This encoding consists of three parts, corresponding
  to the three judgments of the \TirName{e.lam} type rule. We printed the
  judgments of the \TirName{e.lam} rule in the same picture, for ease of
  comparison.
  
  We introduce a |derivation|, which declares the parameters of judgments of
  this type and lists the rules. The typing
  judgments of this form take a global environment |envg| and an expression |e|
  as input, and have a type |ty| as output.
  
  Then we give the rules for proving
  such a typing judgment, in this case only \TirName{e.lam}. The first two
  statements correspond to the conclusion judgment of \TirName{e.lam}. For the
  |e.lam| rule to be applicable, the expression (which we refer to with |this.e|)
  must be of the form |elam p b| (where |elam| is a \Ruler{} equivalent of
  |ELam|). If this match succeeds, this actually defines term variables |p| and
  |b|, hence we write |def p| and |def b|. Furthermore, the conclusion judgment
  specifies that the result type |this.ty| must be the arrow of the type of the
  pattern (|P.ty| in this example) and the body of the lambda (|B.ty| in this
  example).
  
  The next three statements encode the judgment for the pattern. We call this
  judgment P with the |establish| statement, and give bindings for its inputs.
  In this case, the term variable |p| is not defined by the pattern judgment,
  thus we omit |def|. Because we distinuish definition sites from use sites,
  we are able to check that all used term variables are defined.
  
  The final three statements correspond to the judgment for the body. The
  judgment states that it takes the union of the local and global environment
  as its global environment.
  
  \paragraph{More detailed semantics.}
  The expression |this.e| refers to the term of parameter |e| corresponding to
  the conclusion of the rule. Similarly |P.ty| refers to the term of parameter
  |ty| of judgment |P|.
  
  Judgments in type rules are thus translated to an |establish|, followed by a
  several equations corresponding to the terms in the type rules.
  
  The external |elam| represents a relation with inputs |arg1| and |arg2|, and an
  output |res|, such that |res| is equal to the Haskell value |ELam arg1 arg2|.
  For convenience, we use syntactic sugar for function applications.
  The expression |elam p b| is translated to the sequence expression
  (|overlines|; e), with |establish elam as D|, |D.arg1 == p|, and
  |D.arg2 == b D.res| for |overlines| and |D.res| for |e|.
  
  Finally, we use custom syntax for judgments, which we translate accordingly:
  \begin{code}
  syntax envg ; envl |- e : ty                                   establish inferP as P
  establish                                                      P.envg  == env1
    inferP env1 ; env2 |- b : ty1   ^^^^  ~>  ^^^^               P.envl  == env2  
     as P                                                        P.e     == b
                                                                 P.ty    == def ty1
  \end{code}

  The remaining syntactical cases are covered in the next section.
  
  \paragraph{Precise semantics.}
  We gave an intuition for a denotational semantics of \Ruler{} in terms of
  type rules. In Section~\ref{sect.aspect.haskell1} we gave an intuition for
  a denotational semantics of type rules to Haskell. In this paper, we make a
  case for aspect-oriented type rules, and omit a formal semantics for \Ruler.

\section{Executable Type System in \Ruler}
\label{sect.aspect.rulerexample}

  To demonstrate the aspect-oriented type rules, we reformulate the type rules of
  Section~\ref{sect.aspect.example.rules} in \Ruler. In previous work,
  \citet{DBLP:conf/flops/DijkstraS06} show how to
  stack an executable type system on top of a declarative type system. Here,
  we directly give an executable version of the type system.

\subsection{Outline}

  We split the specification in several parts, which we cover individually in
  following sections:
  
  \begin{description}
  \item[Inference tree.]
    Aspects |baseE| and |baseP| specify the structure of the inference tree.
  \item[Global environment.]
    Aspects |globalE| and |globalP| specify how the global environment is
    distributed over the inference tree.
  \item[Local environment.]
    Aspect |localP| specifies how to obtain a local environment from a
    pattern.
  \item[Type.]
    Finally, aspects |typeE| and |typeP| specify the type of a pattern and
    the type of an expression.
  \end{description}
  
  We write partial relations for these aspects, and combine them as follows:

  \begin{code}
  let  inferE = seal (merge baseE globalE typeE)
       inferP = seal (merge baseP globalP localP typeP)
  \end{code}
  
  The |merge| expression specifies a term that is the combination of the partial
  relations it is parametrized with. The free variables of a partial relation,
  i.e. those not in scope of the relation, are shared in a merged relation.
  The |seal| expression requires the relation specified by its parameter
  expression to be complete. All variables must be defined and all abstract
  statements must be instantiated to concrete statements. An |establish| may
  only be parametrized with a closed relation.

  \begin{figure}[htb]
  \begin{code}
  syntax ^^^^  :- e                     -- type an expression |e|
  syntax       :- p                     -- type a pattern p
  syntax ^^^^  envg :-                  -- ... in environment |envg|
  syntax       envl :-                  -- ... in environment |envl|
  syntax       : ty                     -- ... with type |ty|
  syntax       (nm :: ty) `elem` env    -- |nm| has type |ty| in environment |env|
  syntax       l # r                    -- |l| and |r| are disjoined
  ^^^
  syntax       eapp  ^^^^  1 @ 2        -- application pattern
  syntax       elam  ^^^^  \1 . 2       -- lambda pattern
  \end{code}
  \caption{Custom syntax for judgments and terms.}
  \label{fig.aspect.ruler.example.judgmentsyntax}
  \end{figure}

  Since, we split the typing relations in smaller relations, we also split up
  the special syntax for its judgments
  (Figure~\ref{fig.aspect.ruler.example.judgmentsyntax}).

\subsection{Structure Aspect}

  \begin{figure}[htb]
  \begin{code}
    let baseE = derivation input e :: Expr
      fbox (e.int)  === 
                    establish ^^^^  :- eint i
      ^^^^
      fbox (e.var)  ===
                    establish       :- evar nm  ^^^^  ^^^
      ^^^^
      fbox (e.con)  ===
                    establish       :- econ nm
      ^^^^
      fbox (e.app)  establish       :- f              as F
                    establish       :- a              as A
                    ===
                    establish       :- f @ a
      ^^^^
      fbox (e.lam)  establish       :- p              as P
                    establish       :- e              as E
                    ===
                    establish       :- \p.e
  \end{code}
  
  \begin{code}
    let baseP = derivation input p :: Pat
      fbox (p.var)   ===
                     establish ^^^^  :- pvar nm  ^^^^  ^^^
      ^^^^
      fbox (p.con)   ===
                     establish       :- pcon nm
      ^^^^
      fbox (p.top)   establish       :- p              as P
                     ===
                     establish       :- ptop p
      ^^^^
      fbox (p.app)   establish       :- p1             as P1
                     establish       :- p2             as P2
                     ===
                     establish       :- p1 @ p2
  \end{code}
  \caption{The structure aspect.}
  \label{fig.aspect.ruler.example.structureaspect}
  \end{figure}
  
  Figure~\ref{fig.aspect.ruler.example.structureaspect} shows aspects |baseE|
  and |baseP|. These aspects define the shape of the derivation tree (a proof
  for a judgment), by pattern matching on the expression.
  
  For example, rule |e.app| partially specifies how to prove a typing judgment
  |inferE| if its |e|-term is an application |f @ a|. It defines a judgment
  named |F|, and a judgment named |A|, whose |e| parameters are mapped to
  |f| and |a| respectively.
  
  The horizontal line is syntactic sugar. The establish statement below it
  does not define a judgment, but refers to the judgment for which the
  rule defines the proof.


\subsection{Global Environment Aspect}

  \begin{figure}[htb]
  \begin{code}
  let  globalE  = inherit globalExplE globalImpl
       globalP  = globalImpl
  \end{code}
  
  \begin{code}
  let globalImpl = derivation input envg :: Env
    abstract any.envg  ==  this.envg
  \end{code}

  \begin{code}
  let globalExmplE = derivation
    fbox (e.lam)  establish B  ^^^^ (union P.envl this.envg) :-
  \end{code}
  
  \begin{code}
  let  union   = external union   input   l     :: Env
                                  input   r     :: Env
                                  output  u     :: Env
       unions  = external unions  input   envs  :: [Env]
                                  output  u     :: Env
  \end{code}
  \caption{The global environment aspect.}
  \label{fig.aspect.ruler.example.environaspect}
  \end{figure}
  
  For the global environment aspect (Figure~\ref{fig.aspect.ruler.example.environaspect}),
  we define a parameter |envg| and its rules. We split the relation |globalE| in two
  relations. An implicit part defining a generic rule for |envg|, and an explicit part that
  specifies how to deal with |envg| for the |e.lam| case. The |inherit| expression
  merges |globalExplE| and |globalImpl| by only taking those statements from |globalImpl|
  that are not overruled by |globalExplE|.
  
  Relation |globalImpl| defines generic behavior. For each judgment |F|
  that does not have an equation for |F.envg|, the abstract statement gives an
  equation by instantiation of the abstract identifier |any| to |F|. In this case,
  the term |this.envg| is taken, thus corresponding to the reader monad behavior.
  For clarity, we prefix an abstract statement with the keyword |abstract|.
  Also, the abstract statement is not given in the context of a rule, hence it
  applies to all rules in the sealed relation.
  
  The abstract statement can also be written using syntactic sugar for an
  {\it abstract judgment}:
  \begin{code}
    establish any ^^^^ envg :-
    ===
    establish ^^^^  envg :-
  \end{code}
  This syntactic sugar has the advantage that the visual representation
  better resembles the original type rule language.

\subsection{Local Environment Aspect}

  \begin{figure}[htb]
  \begin{code}
  let localP = inherit localExplP localImpl
  \end{code}
  
  \begin{code}
  let localImpl = derivation output envl :: Env
    abstract this.envl  ==  unions all.envl
  \end{code}

  \begin{code}
  let localExplP = derivation
      fbox (p.app)   establish disjoined   ^^^^  P1.envl # P2.envl
  \end{code}
  
  % relations as lambdas too

  \begin{code}
  let  disjoined     = \l r ->  assert (null (intersection l r))
       assert        = external  input   b     :: Bool
       null          = external  input   env   :: Env
                                 output  b     :: Bool
       intersection  = external  input   l     :: Env
                                 input   r     :: Env
                                 output  i     :: Env
  \end{code}
  \caption{The local environment aspect.}
  \label{fig.aspect.ruler.example.environaspectlocal}
  \end{figure}
  
  For the local environment aspect (Figure~\ref{fig.aspect.ruler.example.environaspectlocal}), we split again in an explicit and implicit
  relation. The explicit relation takes care of the disjoinedness check in rule
  |p.app|. For all other cases, the implicit behavior is taken.
  
  The implicit behavior defines |this.envl| as |unions| over the list of the
  |envl| terms of all judgments that have this term. If there are none with
  such an |envl| term, this list is empty. This behavior thus mimics the
  writer monad. We only have to define |this.envl| at places where we want to
  ensure that something is added to the environment. The generic behavior takes
  care of the rest.

  In the last two sections, we covered the abstract identifiers |any| and |all|.
  Furthermore, we provide |first| and |last|, which reference the first and the
  last judgment (having a certain parameter), respectively. Within an abstract
  statement, multiple occurrences of |any| for the same parameter, reference the
  same judgment. Furthermore, in an abstract statement containing |any|, |pred|
  and |succ| refer respectively to the closest judgment having a certain
  parameter before and after the judgment identified by |any|.

  For example, we capture the behavior of the |State| monad as follows:
  \begin{code}
    relation  input   sIn   :: Int
              output  sOut  :: Int
      first.sIn  == this.sIn
      any.sIn    == prev.sOut
      this.sOut  == last.sOut
  \end{code}
  We thus use |this.sIn| for the first judgment. For each subsequent judgment,
  the |sOut| of the previous is taken, and in the end the |sOut| of the
  last judgment is used as |sOut|. 
  

\subsection{Type Aspect}

  \begin{figure}[htb]
  \begin{code}
  let Int = TyCon "Int"
      ^^^^
      typeE = derivation output ty :: Ty
      fbox (e.int)  ===
                    establish ^^^^  : Int
      ^^^^
      fbox (e.var)  establish lookup  ^^^^  (nm :: ty) `elem` this.envg
                    ===
                    establish       : ty
      ^^^^
      fbox (e.con)  establish lookup  ^^^^  (nm :: ty) `elem` this.envg
                    ===
                    establish       : ty
      ^^^^
      fbox (e.app)  ty2 fresh
                    F.ty == A.ty -> ty2
                    ===
                    establish       : ty2
      ^^^^
      fbox (e.lam)  ===
                    establish       : P.ty -> E.ty
  \end{code}

  \begin{code}
  let typeP = derivation output ty :: Ty
      fbox (p.var)   ty fresh
                     establish ^^^^  : ty
      ^^^^
      fbox (p.con)   establish lookup  ^^^^  (nm :: this.ty) `elem` this.envg 
      ^^^^
      fbox (p.top)   assert (isTyCon P.ty)
                     ===
                     establish       : P.ty
      ^^^^
      fbox (p.app)   ty2 fresh
                     P1.ty == P2.ty -> ty2
                     ===
                     establish       : ty2
  ^^^^
  let isTyCon = \ty ->  case ty of
                          tycon _  -> true
                          _        -> false
  \end{code}
  \caption{The type aspect.}
  \label{fig.aspect.ruler.example.typeaspect}
  \end{figure}
  
  Figure~\ref{fig.aspect.ruler.example.typeaspect} contains the type aspect.
  The rules mention many term variables referring to terms provided by the other
  partial relations.
  
  Writing the rules in an aspect-oriented fashion has some notational overhead.
  On the other hand, we can now explain each aspect separately, and
  in isolation (up to the shared term variables). It is also relatively easy
  to add new aspects.
  Furthermore, the abstract terms capture generic behavior, and also allows us
  to give a generic explanation.

%if False
\section{Discussion}

  % what to do with non-determinism in rules?
  % what if checks are done too early?
  
  % multiple traversals
  
  % explain the grand-design of ruler.
%endif

\section{Conclusion}

  We conclude, based on our case study in Section~\ref{sect.aspect.haskell},
  that type rule formalism lacks abstraction. We identified several recurring patterns
  in type rules, and presented aspect-oriented type rules to abstract over
  these patterns. A type system written in an aspect-oriented fashion, has
  several advantages because parts can be described and explained in an
  isolated fashion. Also, common behavior can be factored out, and specialized
  at various other places.
  On the other hand, this also introduces indirection and slight
  notational overhead. However, this pays off for the complex type systems we
  are interested in.
  
  We made these ideas concrete in the form of \Ruler, including
  a tutorial~\cite{arie09} and an implementation~\cite{arie092} in the form of
  an interpreter.
  
  We are currently working on a compiler for \Ruler{} by combining previous work
  on Ruler~\cite{DBLP:conf/flops/DijkstraS06} with the results presented in this
  paper. This compiler turns type rules into attribute grammar code, which in
  turn is suitable for integration in the Haskell compiler UHC.
  Furthermore, since we have mappings from type rules and lambda calculus to
  \Ruler{}, we intend to use \Ruler{} as the formal basis for several
  type rule extensions, dealing with declarative type systems.

\acks

  This work was supported by Microsoft Research through its European PhD
  Scholarship Programme, and the LerNet Alpha-project, which made it possible
  to carry out the initial research for this paper at the Universidade Federal
  de Minas Gerais in Brazil.
  
  The first author wants to thank the Universit\:{a}t Freiburg for
  providing a friendly and hospitable environment in which a portion of the
  work on the \Ruler{} interpreter was done.

%% \bibliographystyle{abbrvnat}
\bibliographystyle{plainnat}
\bibliography{ruler-aspect}

\end{document}