\section{More On Ruler Frontend} %% Ruler formats %format derivation = "\mathsf{derivation}" %format syntax = "\mathsf{syntax}" %format keywords = "\mathsf{keywords}" %format inputs = "\mathsf{inputs}" %format outputs = "\mathsf{outputs}" %format branch = "\mathsf{branch}" %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 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}" %% Ruler functions %format emptyenv = "\emptyset" %% Haskell formats %format hlet = "\mathbf{let}" %format hin = "\mathbf{in}" %format hfix = "\mathbf{fix}" %format hif = "\mathbf{if}" %format hthen = "\mathbf{then}" %format helse = "\mathbf{else}" %format hcase = "\mathbf{hcase}" %format hof = "\mathbf{of}" %% Common symbols %format |- = "\vdash" %format ~> = "\leadsto" %format |-> = "\mapsto" %format . = "." %format === = "\rule{8em}{1px}" %% Spacing %format ^^^ = "\;" %format ^^^^^ = "\hspace{1cm}" %% Common names %format e1 %format e2 %format v1 %format v2 %format env = "\Gamma" %format ty = "\tau" \newcommand\Repmin{\scshape Repmin \normalfont} \newcommand\Interpreter{\scshape Ruler Interpreter \normalfont} \newcommand\Compiler{\scshape Ruler Compiler \normalfont} \section{Introduction} A type system specifies a {\it typing relation} that classifies which types are valid for an expression. Given a type system, it is often not immediately clear if there exists an algorithm that {\it infers} valid types given an expression, when a valid type exists. Furthermore, when multiple types are valid for an expression, it is also often not clear which of these types the inference algorithm actually infers. This tutorial introduces \Ruler, a domain-specific language for {\it executable} specifications of {\it complex} type systems, designed for the generation of both a type inferencer and documentation. The language has facilities to deal with the incremental behavior of type inference, and aspect-oriented abstraction mechanisms to cope with design complexity. Not all type systems can be easily expressed in \Ruler, but for those that are, there is an inference algorithm that infers one particular (preferably the most general) valid type of an expression. For those that cannot, in particular type systems in which the typing relation is not functional, the inferencer is sound but not complete. Given a typing relation specified with inference rules, type inference is generally the process of finding out which rules to apply (obtaining a so called derivation tree, which is a proof that the typing relation holds), and how to instantiate the object variables of these rules (thus finding the types). The \Ruler language is loosely based on these inference rules. In contrast to other approaches that employ search strategies, there are two underlying design decisions in \Ruler: \begin{itemize} \item The object variables (meta variables) of the typing relation are partitioned in inputs and outputs. The outputs are a {\it function} of the inputs. \item The structure of the derivation tree is determined only by what becomes gradually known about the object variables during inference. \end{itemize} We obtain {\it efficient} inference algorithms using these design decisions, in both time and space, comparable to hand written traversals over abstract syntax trees. However, so called declarative type systems, which are nondeterministic in the structure of the derivation tree or in the contents of the object variables, may not be expressible in \Ruler or require additional effort. \Ruler has a special facility to delay decisions about the structure of the derivation tree until more is known about some of the object variables. Many nondeterministic aspects are dealt with this way. In this tutorial, we focus on the aspect-oriented basis underlying \Ruler. The facilities for deferring decisions will be covered in a later tutorial. We gradually introduce features by means of several examples. First we give an abstract overview of \Ruler in Section~\ref{sect.tutorial.overview}, then show how to get started in Section~\ref{sect.tutorial.helloworld}. We start with a simple arithmetic evaluator in Section~\ref{sect.tutorial.arithmetic}, where we introduce the rule syntax and the use of data structures. We give inference algorithms for several type systems of increasing complexity, beginning with a monomorphic type inferencer in Section~\ref{sect.tutorial.mono}, where we see how to deal with not yet known information during inference. The classical Damas-Milner type system is taken as example in Section~\ref{sect.tutorial.milner}. There, we show how to write judgments in lambda calculus-style instead of rule-style. In Section~\ref{sect.tutorial.milneraspect} we show how to write the inferencer for Damas-Milner in an aspect-oriented fashion. Then in Section~\ref{sect.tutorial.repmin}, we deal with functions where some of the inputs depend on some of its outputs, by taking the classical \Repmin problem as example. \section{Abstract Overview} \label{sect.tutorial.overview} In this section, we position \Ruler in the field of meta-systems by giving an overview of the challenges it has been designed to deal with, and give a characterization in terms of the lambda calculus. \subsection{Challenges} We briefly touched the inference problem in the introduction. Based on experiences with the UHC compiler, we identify several practical challenges. \begin{description} \item[Experimentation.] A type system is often not just a theoretic artifact. The designer has an inference algorithm in mind and typically writes a prototype implementation for experimentation. With \Ruler, we provide a reusable inference framework for rapid prototyping of type systems. The \Interpreter offers facilities for the visualization and debugging of the constructed derivation trees, or for the inspection of a failure to construct a derivation tree. \item[Efficiency.] Type inference is a form of proof-search. The proof is the derivation tree, where each node corresponds to a rule that has been applied, and the {\it attributes} of these nodes correspond to the instantiations of the object variables of the rules. Traditional Prolog-based approaches perform a breadth-first exploration of the search space. This search is too slow for a practical setting. The evaluation model of \Ruler does not perform any search to obtain the structure of the derivation tree. The underlying assumption is that the contents of the attributes of the derivation determine the shape of the tree. In practice, many of the type systems can be easily written as a collection of syntax directed or type directed inference rules. These thus satisfy that assumption. \item[Soundness, completeness and consistency.] A language designer typically has a specification of a type system in terms of declarative type rules already. This designer wants an inference algorithm that resembles these rules. This algorithm is easier to explain, and it is easier to see that the algorithm is consistent with the rules. In fact, the soundness and completeness of the inference algorithm with respect to the type system is an important question. In \Ruler, the type system and inference algorithm are the same artifact and thus mutually consistent. Ruler programs can be pretty-printed to a textual representation as a collection of type rules, and there are language constructs to influence the visual representation. Compared to inference algorithms written in conventional (functional) programming languages for a certain type systems, have ruler programs a closer resemblance to such type systems. In fact, with a ruler program, it is straightforward to prove soundness with respect to such a type system. Completeness requires effort to show that the explicit scheduling decisions about which part of the derivation to construct in the evaluation model of \Ruler, are taken in the right order. \item[Coping with complexity.] Type systems for real-world languages comprise many features and are consequently verbose and complex, with typing relations over many object variables, and formed by a large number of inference rules. Although there are typically concise declarative rules for individual language features, this is not the case anymore when combining these features. The type rule formalism thus lacks abstraction to cope with complex rules with many object variables. Not only the type rule formalism, but also many implementation techniques suffer from the lack of abstraction. A practical type inferencer needs to be highly parametrizable, and combine information from various places in the abstract syntax tree. The propagation of information at the place it is available to the place it is needed, requires extensive book keeping. \Ruler offers two essential abstraction mechanisms. Instead of giving a single large relation between object variables, as with type rules, the relations are described in parts as separate aspects in \Ruler, and combined in a big relation automatically. Furthermore, typing relations can be higher-order, which makes them highly parametrizable. \item[Interoperability.] The type inferencer is only a single component of a compiler. There is interaction with other components, such as a code generator. The \Compiler generates attribute grammar code for those parts of the derivation tree that can be constructed in a syntax directed fashion. These attribute grammars provide an interface for integration. \end{description} \subsection{Characterization} We characterize \Ruler by looking at particular language features in relation to the lambda calculus. \begin{description} \item[Functions and function calls.] In \Ruler, there is a connection between the evaluation of functions and the construction of derivation trees. Each function call corresponds to a node in the derivation tree. Each function call during the evaluation of a function corresponds thus to a subtree. The attributes of a node in the derivation tree consist of the inputs and outputs of the function. \item[Application and beta reduction.] In functional programming, beta reduction is performed when a function has received values for all its arguments (a saturated function application). In \Ruler, beta reduction is totally separated from function applications. Ruler's equivalent of lambda abstraction takes multiple arguments and returns multiple results. There is a special operation (named |establish| later), that causes a portion of a ruler lambda (which we call {\it derivations}) to be beta-reduced (called {\it visited}). With each visit a portion of the derivation tree is produced, and each parent must be partially constructed before a child is. This separation is important. The default execution model is a depth-first construction of the derivation tree. The order of construction determines what information is inferred at which moment. This default order may not be suitable for a particular application, and by controlling the beta reduction, we can deviate from this order. \item[Guesses, unification and side effect.] In functional languages, there are concepts of bottom values and references. \Ruler has a special form of values that is a combination of the above: values that may not yet be known during inference. We call these {\it guesses}. A guess has an observable identity and an actual value. The actual value is undefined until the guess is known, and remains constant ever after. Furthermore, \Ruler has a first-order unification operator which is used to assert the equality between values and causes guesses to be defined. This is a side-effectful operation. A part of a ruler program observing an unknown guess may have observed a known guess if it was executed at a later moment during inference. Inference becomes unpredictable when this difference matters. In future versions of the ruler language, we intent to limit this side-effect. Pattern matches require the input value to be defined up to the depth of the match. A fixation procedure then forces not yet known guesses to application defined fixed constants that may be observed. \item[Statically ordered evaluation with multiple visits.] For some complicated type systems, the inputs of a typing relation may be dependent on some of the outputs. Lazy evaluation offers a nice evaluation model for these cases. There are several practical reasons against lazy evaluation, however. One may accidentally introduce a hard to find loop, or cause a condition not to be checked, because some part of the code is never used. Also, when dealing with values containing guesses, inferencers need to carry a substitution around, which forces a certain evaluation order. This is not necessarily the case for \Ruler, because the book keeping is hidden, but never the less would this book keeping be (much) more expensive due to guesses and backtracking when using lazy evaluation. Ruler therefore takes a statically ordered evaluation model. To deal with cases whith a non-cyclic dependence of an input on an output, \Ruler supports multiple visits. Beta reduction is done partially. In each visit a portion of the output is produced with a portion of the inputs. \item[Foreign functions.] Ruler has no primitive operations, nor a concept of data structures. Instead, there is an interface to call Haskell functions. These Haskell functions take care of constructing Haskell values and manipulating them. These Haskell values may contain guesses. We provide an API to incorporate them in Haskell data types and to inspect and manipulate them. Ruler programs typically perform many pattern matches, even though \Ruler has technically no concept of a pattern. Pattern matches are performed by building values with guesses in them through the Haskell functions, and performing the match with unification. Future versions of \Ruler have limited knowledge of data structures for more efficient pattern matches. Note that although ruler programs are evaluated eagerly, this is not necessarily the case for the Haskell functions. The results of these Haskell functions are reduced to weak head normal form, but the actual moment and depth of inspection of deeper parts of the values we leave unspecified. \end{description} \section{Hello World!} \label{sect.tutorial.helloworld} In this section we show the basic concepts of ruler programs: {\it derivations}, {\it statements}, and {\it expressions}. The explanation will be in terms of concepts known from functional programming and type systems. We show how to use the \Interpreter to execute such a program, and how to interpret the results. We keep the explanation to the bare essentials only, and explore different forms of statements and expressions in later sections in more detail. \subsection{Basic Concepts} \paragraph{Derivation trees.} In type systems, a derivation tree is a proof that a typing relation holds between object terms. These object terms are typically environments, objects and types. More complicated type systems have many forms of typing relations and many forms of object terms. We consider type systems specified with inference rules. The nodes of a derivation tree of such a system correspond to rules, the children of a node to judgments of such a rule. The object terms are {\it attributes} of the nodes. In \Ruler, typing relations are {\it functional}. The object terms are partitioned in parameters and results. The derivation tree in this setting is a proof that such a function was successfully applied to its inputs and produced its results. Each node corresponds to a fully saturated function call, and both the actual values of the parameters as the actual results form the attributes of the node. \paragraph{Derivations.} In functional programming, functions are represented with a lambda abstraction. Functions in \Ruler have correspondences with lambda abstractions, but are not the same. A lambda abstraction has a single input and a single output, plus an {\it algorithm} (is this case, some code corresponding to the body of the function) that may call other functions and produces the output in the end. The lambda abstraction look-a-like in \Ruler is called a {\it derivation}. A derivation has (multiple) inputs and (multiple) outputs, and many bodies called {\it branches}. Each branch defines a possible alternative for a node in the derivation tree. These branches are the \Ruler analogy to inference rules. A branch contains the algorithm (in the form of a list of statements, to be discussed later) that constructs the subderivations and produces the outputs. \begin{figure}[htb] \begin{code} derivation inputs args { ^^^ branch main: eval message "Hello World!"; } \end{code} \caption{@examples/helloworld.rul@} \label{fig.tutorial.codehelloworld} \end{figure} An example derivation is given in Figure~\ref{fig.tutorial.codehelloworld}. It defines an input |args|, no outputs, and only has a single branch called |main|. It also has a single statement, to be discussed later. Haskell functions can masquerade as derivations. |message| is an example of such an {\it external function}. We discuss external functions in Section~\ref{fig.tutorial.externals}. \paragraph{Expressions and statements.} There are two main syntactical categories in \Ruler: expressions and statements. Expressions are {\it evaluated} to values and statements are {\it executed}, producing no values but side effect. Several forms of expressions and statements are explained in this tutorial. We define their semantics in terms of their respective evaluation and execution. The derivation that we saw in Figure~\ref{fig.tutorial.codehelloworld} is an example of such an expression. We come back to its evaluation and the resulting value shortly. There is a single statement in the |main| branch. This |eval| statement takes an expression, evaluates it, and throws away the result. In this case, the expression is an application expression, applying the expression |message| (an identifier) to the expression |"Hello World"| (a string). Again, we explain these application expressions later. \paragraph{Values} In a functional language, there are two categories of values. Values in the form of constructors, and values related to lambda abstractions, namely closures or thunks, and partial applications. Ruler has the same types of values: \begin{description} \item[Haskell Values.] These are values opaque to \Ruler, such as integers, strings, lists, maps, and abstract syntax trees. These values can be passed around, but not directly manipulated. External Haskell functions manipulate these data structures. \item[Closures.] Evaluation of a derivation expression is quite straightforward. Some representation of the derivation, and bindings for the free variables, are stored in a closure-value. No further execution inside the derivation itself is performed. A closure is obtained by evaluating a derivation expression, but there is one other way to obtain a closure. One can write the lambda expression |\x -> e|, for a derivation with one input and one output, with as value for the output the result of evaluating the expression |e|. In other words, we encode conventional lambda abstraction as restricted forms of derivations. \item[Partial applications.] A closure represents an abstract derivation tree. An abstract derivation tree can be transformed into a real derivation tree in three steps. The first step is to {\it instantiate} the closure, by means of the |inst| statement: \begin{code} inst e as d; \end{code} Here |e| represents a derivation-expression (for example, the expression in Figure~\ref{fig.tutorial.codehelloworld}), and |d| is a name. As side effect is bound to |d| the partial application, obtained from evaluating |e| and instantiating the resulting closure. Secondly, values need to be passed as actual parameters of the partial application. In functional programming, a partial application keeps track of arguments until all are available to call the actual function. In \Ruler, a partial application collects bindings for inputs and outputs. Values are bound to inputs and outputs through equality statements: \begin{code} d.args == nil; \end{code} In this case, the empty list |nil| is assigned to the input |args|. The expression |d.args| is an example of a field expression, where |d| must be bound to a partial application, and |args| be an input or output of the corresponding derivation. The last step is to start the construction of the derivation tree (comparable with beta reduction). This step is implicitly taken in functional programming, but must be done explicitly in Ruler with the |establish| statement: \begin{code} establish d; \end{code} As effect, a branch is selected that matches the inputs (explained later), its statements executed, and the results unified with the outputs bound in the partial application. So, a partial application keeps track of both bindings for inputs and outputs, as well as the derivation tree constructed so far. A special form of application is the application expression in Figure~\ref{fig.tutorial.codehelloworld}. This is a short hand notation for instantiating the closure, passing the argument, and establishing the result. Indeed, conventional function application is a three step process in \Ruler. We introduce ruler syntax in the next section. This syntax provides an alternative way to specify |inst|, |establish| and equality statements. Combined with the functional syntax above, one rarily writes statements such as |inst| explicitly. \item[Guess.] Aside from the above three values, \Ruler has one extra type of values: {\it guesses}. A guess can be seen as a special form of an integer, and we constraint Haskell values such that they can contain these guesses. A guess is obtained by using the |fresh| statement: \begin{code} x fresh; \end{code} Execution of such a statement binds a fresh guess to the name |x|. We require the Haskell values to be convertible from and to guesses. A guess may become defined due to execution of equality statements: \begin{code} x == 3; \end{code} Execution produces the side effect that the fresh guess bound to x has become known as the value |3|. This effect is irreversible, except through backtracking (to be explained later). \end{description} \subsection{The \Interpreter} This tutorial is based on the use of the following tools: the \Interpreter\footnote{\url{https://svn.science.uu.nl/repos/project.ruler.systems/ruler-interpreter/}} to execute ruler programs and dot\footnote{\url{http://www.graphviz.org/}} to visualize the derivation trees. Figure~\ref{fig.tutorial.commandline} lists some useful commandline options. A ruler program is a ruler expression. The first step the ruler interpreter takes is to evaluate this expression, which results in a closure value. It then takes a second step: it takes the closure and instantiates it, obtaining a partial application. The root of the tree is required to have one input attribute called |args|. The ruler interpreter assigns the list of commandline arguments to this input attribute and runs the algorithm to produce the tree. Finally, the resulting derivation tree is pretty printed. If the execution of the algorithm fails, then a partial derivation tree is pretty printed such that the problem can be inspected. \begin{figure}[htb] \begin{description} \item[@-d@, @-d2@, @-d3@, @-d4@] The debug level, by default |0|. \item[@-Tdot@, @-Ttxt@, @-Ttex@] Specifies the output format. Text output is the default. Alternatively, a print to a @dot@ graph, or to \LaTeX can be chosen. We patched the HTML renderer of @dot@ to produce slightly better graphics. \item[@-m@] Outputs messages to @stderr@. This comes in useful when debugging a non-terminating ruler program. \item[@-DBT@, @-DTB@] Specifies the direction in which the derivation tree grows. We adhere to the convention to grow derivation trees from bottom to top, but the direction can be inverted by means of @-DTB@. \item[@-I@] Loads a list of statements in @path@ into the interpreter, and brings the bindings in scope of the main expression. The files are loaded in the order of appearance of their corresponding commandline argument. \end{description} \caption{Commandline parameters of the \Interpreter.} \label{fig.tutorial.commandline} \end{figure} We execute this ruler program discussed earlier (Figure~\ref{fig.tutorial.codehelloworld}) with the ruler interpreter, and produce a pretty print of the derivation tree by running: \begin{verbatim} ./ruler -Tdot -o./derivation.dot helloworld.rul dot -Tpdf -o derivation.pdf derivation.dot \end{verbatim} Consequently, the interpreter evaluates the expression |message "Hello World"|. As we showed above, the body of message executes with |"Hello World"| as parameter. In this case, |message| is an external function that takes the input string and records is as a note in the derivation tree. Figure~\ref{fig.tutorial.fighelloworldok} shows the resulting pretty print. \clearpage \begin{figure}[htb] \centering \includegraphics*[viewport=60 50 220 210]{aspect-rules/figures/helloworld-ok} \caption{A successful derivation of the Hello World program} \label{fig.tutorial.fighelloworldok} \end{figure} The derivation tree grows from bottom to top. Nodes in the derivation tree are represented by rectangles containing the following components: \begin{itemize} \item The name of the branch in the black box, followed by the location of the branch in the @helloworld.rul@ file, and the location in the source file of the |derivation|. External derivations (such as |message|), do not have a location, and some derivations can actually span more than a single location. \item A table with the input and output attributes of the derivation. The inputs and outputs are marked @I@ and @O@ respectively. Of each attribute the name is printed, and the actual value. \item In the blue box, the list of children, including the name (and location in the source file), and arrows pointing to the subderivations. \item A list of messages that were produced during the execution of algorithm of the node. \end{itemize} \begin{figure}[htb] \begin{code} derivation inputs args { ^^^ branch main: x fresh; eval message x; } \end{code} \caption{@examples/helloworld.rul@} \label{fig.tutorial.codehelloworld-wrong} \end{figure} Alternatively, an incorrect ruler program is given in Figure~\ref{fig.tutorial.codehelloworld-wrong}. We made two changes: the branch |main| has two statements, and the input string is replaced with a fresh guess. The execution order is determined by requiring that values need to be defined before they their use. In this case, fresh defines |x| and |message| uses |x|, so coincidentally the order in which the statements appear in the example is also the order in which they are evaluated. The mistake is to pass the fresh guess |x| to |message|, and |message| only evaluates successfully if it gets a concrete string as parameter. Consequently, executing his ruler program results in a failed derivation, as shown in Figure~\ref{fig.tutorial.codehelloworld-wrong}. The incomplete nodes are printed in red, with an error message explaining the reason why the corresponding derivation did not evaluate fully. If one node is incomplete, then by definition all its parents are incomplete too. A shorter version of the original error message is shown as message for all the nodes up to the root. \begin{figure}[htb] \centering \includegraphics*[viewport=60 50 500 260,scale=0.7]{aspect-rules/figures/helloworld-failed} \caption{A failed derivation of the Hello World program} \label{fig.tutorial.fighelloworldfailed} \end{figure} \subsection{Syntax} To conclude, Figure~\ref{fig.tutorial.syntax1} gives an overview of the expressions and statements as seen so far. We introduce more forms of expressions and statements in later sections. \begin{figure}[htb] \noindent Expressions:\\ \begin{tabular}{ll} |x| & looks up |x| in the environment \\ |f.x| & looks up attribute |x| of derivation |f| \\ |e1 e2| & applies |e1| to the result of |e2| (special case of |inst| and |establish|) \\ |derivation ...| & general abstraction: multiple inputs, multiple outputs, branches. \\ |\e1 -> e2| & lambda abstraction (special case of general abstraction) \\ \end{tabular} \\\\ \noindent Statements:\\ \begin{tabular}{ll} |eval e;| & evaluates e and throws away the result. \\ |x fresh;| & creates a fresh guess and binds it to |x|. \\ |inst e as d;| & evaluates |e| to a closure, instantiates it to a partial application, and binds to |d|.\\ |e1 == e2;| & evaluates |e1| and |e2|, and unifies the results.\\ |establish d;| & constructs an instantiated derivation.\\ \end{tabular} \caption{Syntax summary.} \label{fig.tutorial.syntax1} \end{figure} In the remainder of this tutorial, the word ``derivation'' can stand for both (sub) derivation trees in their different froms, or a |derivation| function. \section{Arithmetic Evaluator} \label{sect.tutorial.arithmetic} In the previous section we gave a simple example of a ruler expression and explained how to use the the tools involved. In the coming sections we gradually introduce more expression and statement forms, starting with rule syntax in this section. \begin{figure}[htb] \begin{mathpar} \fbox{$ \inferrule*[] {} { g : e |=>| v }$}\\ \inferrule*[right=const] {} { g : i |=>| i } \inferrule*[right=var] { (x,v) \in g } { |g : x => v| } \inferrule*[right=let] { |g : e1 => v1| \\ |x| \mapsto |v1|, |g : e2 => v2| } { |g : hlet x = e1 hin e2 => v2| } \inferrule*[right=add] { |g : e1 => v1| \\ |g : e2 => v2| } { |g : e1 + e2 => add v1 v2| } \inferrule*[right=sub] { |g : e1 => v1| \\ |g : e2 => v2| } { |g : e1 - e2 => sub v1 v2| } \inferrule*[right=mul] { |g : e1 => v1| \\ |g : e2 => v2| } { |g : e1 * e2 => mul v1 v2| } \inferrule*[right=div] { |g : e1 => v1| \\ |g : e2 => v2| } { |g : e1 * e2 => div v1 v2| } \end{mathpar} \begin{code} e ::= ^^^ i ^^^ | ^^^ x ^^^ | ^^^ let x = e1 in e2 ^^^ | ^^^ e1 + e2 ^^^ | ^^^ e1 - e2 ^^^ | ^^^ e1 * e2 ^^^ | ^^^ e1 / e2 v ::= i g ::= emptyenv ^^^ | ^^^ x |-> v, g \end{code} \caption{Arithmetic evaluation rules.} \label{fig.tutorial.evalrules} \end{figure} \subsection{Example} The running example in this section is an evaluator for the (big-step) arithmetic evaluation rules in Figure~\ref{fig.tutorial.evalrules}. These rules specify the integer value |v| of an arithmetic expression |e| in an environment |g| containing bindings of identifiers |x|. The rules are a bit underspecified in the sense that semantics for |mul|, |add|, etc. are not given, but assume these correspond to binary functions on integers. \begin{figure} \begin{code} data Arith = ArithVar Name | ArithConst PrimInt | ArithAdd Arith Arith syntax ^^^ arithAdd ^^^ { 1 + 2 }; | ArithSub Arith Arith syntax arithSub { 1 - 2 }; | ArithMul Arith Arith syntax arithMul { 1 * 2 }; | ArithDiv Arith Arith syntax arithDiv { 1 / 2 }; | ArithLet Name Arith Arith ^^^^^ ^^^^^ syntax arithLet { hlet 1 = 2 hin 3 }; | ArithInd IndInfo ^^^ (Maybe Arith) \end{code} \caption{Data type for arithmetic expressions} \label{fig.tutorial.evaldata} \end{figure} We will now give a Ruler program for the rules in Figure~\ref{fig.tutorial.evalrules}. Our first step is to define precisely the data structures involved. In Figure~\ref{fig.tutorial.evaldata}, we give a data type for arithmetic expressions. It has the usual cases for variables, integers, addition, subtraction, etc. Furthermore, we define some concrete syntax for nicer manipulation of the abstract syntax, by means of |syntax| statements. The statement |syntax arithAdd { 1 + 2 }| consists of an identifier |arithAdd| and a pattern |{ 1 + 2}|. It stands for an extension of the grammar of ruler expressions, representing the function application |arithAdd e1 e2| when recognizing an expression of the form |e1 + e2|, where |e1| and |e2| are again ruler expressions. The numbers in the pattern thus stand for indexed ruler expressions, and these expressions are passed to the function in increasing order of index. Beware of ambiguities with these syntax extensions. \begin{figure} \begin{code} syntax ^^^ { ^^^ g : e => !v ^^^ }; ^^^ let evaluate = derivation inputs g, dispatch e outputs v { branch const: ^^^ === ^^^ establish ^^^ { ^^^ g : arithConst i => i ^^^}; ^^^ branch add: ^^^^^ branch sub: ^^^ establish ^^^ { ^^^ g : e1 => v1 ^^^ }; ^^^^^ ^^^ establish ^^^ { ^^^ g : e1 => v1 ^^^ }; ^^^ establish ^^^ { ^^^ g : e2 => v2 ^^^ }; ^^^^^ ^^^ establish ^^^ { ^^^ g : e2 => v2 ^^^ }; ^^^ === ^^^^^ ^^^ === ^^^ establish ^^^ { g : e1 + e2 => add v1 v2 ^^^ }; ^^^^^ ^^^ establish ^^^ { ^^^ g : e1 - e2 => sub e1 e2 ^^^ }; ^^^ branch mul: ^^^^^ branch div: ^^^ establish ^^^ { ^^^ g : e1 => v1 ^^^ }; ^^^^^ ^^^ establish ^^^ { ^^^ g : e1 => v1 ^^^ }; ^^^ establish ^^^ { ^^^ g : e2 => v2 ^^^ }; ^^^^^ ^^^ establish ^^^ { ^^^ g : e2 => v2 ^^^ }; ^^^ === ^^^^^ ^^^ === ^^^ establish ^^^ { ^^^ g : e1 * e2 => mul v1 v2 ^^^ }; ^^^^^ ^^^ establish ^^^ { ^^^ g : e1 * e2 => div v1 v2 ^^^ }; ^^^ branch alet: ^^^ let g' = extend x v1 g ^^^^^ branch var: ^^^ establish ^^^ { ^^^ g : e1 => v1; ^^^ }; ^^^^^ ^^^ let v = lookup x g ^^^ establish ^^^ { ^^^ g' : e2 => v2; ^^^ }; ^^^^^ ^^^ === ^^^ === ^^^^^ ^^^ establish ^^^ { ^^^ g : arithVar x => v ^^^ }; ^^^ establish ^^^ { ^^^ g : hlet x = e1 in e2 => v2 ^^^ }; ^^^^^ }; ^^^ derivation inputs args outputs res { branch main: let e = parse this.args; establish evaluate ^^^ { ^^^ emptyenv : e => this.res ^^^ }; } \end{code} \caption{Ruler program for arithmetic evaluation.} \label{fig.tutorial.evalcode} \end{figure} The evaluator is given in Figure~\ref{fig.tutorial.evalcode}. It has a close resemblance to the actual evaluation rules, which may already give an intuition about the semantics of this ruler program. However, we go through it step by step. There are two important syntactical categories that are used a lot in this tutorial, and which are important to distinguish. These are ruler expressions and ruler statements. We have already seen the important forms of of expressions, namely derivations, application, variables, and strings. An expression is evaluated to a value. Such a value is either an external Haskell value, an uninstantiated derivation (closure), or an instantiated derivation (partial application). Statements, on the other hand, are executed. Most statements are judgments, asserting the equality between values, asserting (introducing) subderivations, binds names to values, and introduces fresh guesses. \subsection{Evaluation and Execution} The entire expression in the example is a {\it sequence expression}, which consists of a list of statements followed by an expression. The list of statements is is executed first, in the order of appearance, then the expression is evaluated and its result is the result of the entire expression. The order of execution differs from statements of a derivation branch, which are executed in an order based upon input and output dependencies\footnote{ The rationale is that statements of a derivation branch are typically related to different aspects. For clarity, statements of a single aspect should be close to each other, and this may conflict with an evaluation order based on source location. The statements of a sequence expression, however, are typically related to a single aspect and can therefore be executed in the order of appearance, which is generally more intuitive. }. Bindings introduced during the execution of such a statement are in scope of the later statements and the expression. Summarizing the previous section, the \Interpreter expects an expression that upon evaluation results in a closure that is instantiated with the commandline parameters as its only actual parameter. So, when the \Interpreter evaluates the expression of this example, it first executes the statements in the beginning and then starts with the main derivation. We consider the remaining parts of the example in this order. The first statement is yet another |syntax| statement, but slightly different compared to the other |syntax| statements we saw earlier. It defines custom syntax for judgments. The pattern specifies the syntax, and names of the inputs and outputs (prefixed with a |!| symbol) of the judgment. In this case, it defines the syntax of the evaluation-judgment, with |g| and |e| as inputs and |v| as output. We see later how this syntax is actually used. Such syntax declarations apply to the entire file and can only occur as a statement of a toplevel sequence expression. Aside from this |syntax| statement, there is also a |keywords| statement to define additional keywords to be used in the custom syntax. These statements are skipped during execution, i.e. have no side effect. The next statement is a |let| statement. It consists of two expressions, a {\it pattern expression} on the left side and a conventional expression on the right side. A pattern expression is a conventional expression except that during evaluation the values of the identifiers are defined instead of dereferenced. In this case, the expression on the right side is evaluated, resulting in a closure-value. This value is then bound to the name |evaluate|. This |let| is recursive, so the identifier |evaluate| is in scope of the expression on the right hand side. Now consider the main derivation expression before we go into |evaluate|. It declares on output called |res|. The inputs and outputs of a derivation can be referenced by a so called field expression. A field expression consists of two identifiers separated by a dot. The first identifier must be bound to a partial application. The second identifier must be an input or output of it. The identifier |this| points to the partial application of the currently executing derivation\footnote{Alternatively, add |innername nm| to a derivation to use |nm| where you would normally use |this|.}. The first statement of the main derivation thus applies |parse| to the input |args| of the derivation, and binds the result to |e|. Assume for now that |parse| is an external function that evaluates successfully if |args| is a singleton list containing a filename, of which the file contains an arithmetic AST. Then the output is this AST. The last statement is |establish| in rules syntax form, which is one of the corner stones of a ruler program. We see some different forms of an |establish| statements during this tutorial. We already saw the core form of |establish| in the previous section. The establish statement in rules syntax does slightly more. Informally, it creates a child derivation in a couple of steps. First it instantiates the derivation by taking the closure (in this case |evaluate|) and turning it into a partial application (instantiated derivation). Then input and outputs are supplied through the use of the syntax we defined earlier. In this case |emptyset| for the environment input |g|, the parsed arithmetic expression |e| for the expression input |e|, and the output named |v| is mapped to |this.res|. Finally, the derivation is established by choosing the appropriate branch and executing the statements of the branch. \subsection{Branch Selection} Branch selection proceeds as follows. Branches are tried in the order of appearance. If all statements execute successfully, the branch is chosen. If execution of a statement in a branch fails, the execution backtracks to the next branch. However, not in all circumstances. Backtracking is limited in Ruler, for two reasons: dealing with erroneous inputs and efficiency. A branch is fixed when going in recursion (establishing a child derivation based on the same closure as the parent derivation), or just before performing an |establish|-statement, except for |establish| statements of a sequence expression. Furthermore, when an input is prefixed with |dispatch|, backtracking is only allowed when the execution of statements referencing that input fails. These statements are also executed as early as possible. Failures in other statements lead to an immediate abort. If the patterns in the branches are not overlapping, we can actually directly try the right branch based on the actual value of the input. \subsection{Rules} So, establishing |evaluate| with an empty environment and an arithmetic expression leads to the construction of the derivation bound to |evaluate|. We see now an example with many branches, and a horizontal rule statement. A horizontal-rule statement is a statement starting with a rule, followed by a list of establish statements, which we call conclusions (may be more than one). There are some essential differences: \begin{itemize} \item A conventional establish leads to the creation of a child derivation. A conclusion refers to the establishment of the current derivation. It specifies how to pattern match on inputs of the derivation, and how to construct the outputs of the derivation. \item The identifier of an |establish| may be omitted, for which implicitly |this| is taken, which then leads to the creation of a child derivation of the same form as the parent derivation. For a conclusion, the identifier must be omitted. \item The input and output expressions of a conclusion are inverted. For example, the conclusion in branch |const| maps an output expression |g| to the input |g| of the derivation, an output expression |arithConst i| to the input |e| of the derivation, and an input expression |i| to the output |v| of the derivation. Semantically, this means that an identifier |g| is in scope of the branch, an identifier |i| by matching |arithConst i| against the input |e|, and that the output |v| of the derivation is obtained by taking the value of |i|. \end{itemize} The actual contents of the rules are not surprising. We use the syntax extensions for function applications heavily for slightly more appealing pattern matches. Furthermore, |add|, |mul|, etc. are external functions operating on integers. Finally, lookup and extend are external functions operating on environments. \subsection{Evaluation By Example} To give a summary of the evaluation model discussed so far, consider having a file with the following example expression: \begin{code} let z = 3 + 4 in 6 * z \end{code} The ruler interpreter starts evaluating the expression in Figure~\ref{fig.tutorial.evalcode}. The syntax statements are ignored. The derivation-expression is evaluated to a closure and bound to |evaluate|, followed by the evaluation of the main derivation, resulting in a closure (containing among others the binding for |evaluate|). The ruler interpreter takes this closure, binds the commandline arguments to its |args| input parameter and establishes the derivation. There is only one branch called |main| which is executed. Since |e| is an output of the parsing and an input of the evaluation, the first statement is executed first. This leads to the establishment of the external derivation |parse|, which parses the expression, and the result is bound to |e|. This value of |e| is of the form: \begin{code} ArithLet z (ArithAdd (ArithConst 3) (ArithConst 4)) (ArithMul (ArithMul 6) (ArithVar z)) \end{code} Then the |evaluate| derivation is established with an empty environment and the above value as actual parameters. Branches are tried in order of appearance. The first branch that is tried is |const|. However, this fails because |ArithConst i| (for some fresh |i|) cannot be matched against the value given above. The other alternatives are tried until we reach branch |alet|. The match on input |e| succeeds, resulting in bindings: \begin{code} x ^^^ |-> ^^^ z e1 |-> ArithAdd (ArithConst 3) (ArithConst 4) e2 |-> ArithMul (ArithMul 6) (ArithVar z) \end{code} The first statement of the branch cannot be executed yet because it depends on output |v1| of the second statement. Therefore, the second statement is executed first. This leads to the creation of a child derivation with |e1| as input |e|. The branch |add| succeeds, executing the statements and creating a couple of child derivations in similar ways as described earlier. Their results |3| and |4| are added up to |7| by means of the external function |add|, and returned as |v1| in branch |alet|. Then the first statement of |alet| (is allowed to) runs, producing the singleton environment |g'| containing the mapping of |z| to |7|. Finally, the third statement executes with this extended environment, producing in the end |42|. This result is bound in the main derivation to output |this.res|. \begin{figure}[htb] \centering \includegraphics*[width=0.8\textwidth]{aspect-rules/figures/arith} \caption{The derivation tree of |evaluate (let z = 3 + 4 in 6 * z)|.} \label{fig.tutorial.examplearithtree} \end{figure} Figure~\ref{fig.tutorial.examplearithtree} shows the derivation tree that corresponds to the description above. Some of the values corresponding to attributes in the trees are pretty printed seperately from the derivation tree to keep the printed tree smaller. \subsection{Ruler Programs as Specification} We saw how to implement rules as a ruler program. Note that the ruler program itself can be used as a description of the evaluation rules. In fact, suppose that we add the following statements: \begin{code} let lookup = external lookup inputs x, g outputs v; syntax { ^^^ (x |-> v) `elem` g ^^^ }; syntax extend { ^^^ (1 |-> 2), 3 ^^^ }; \end{code} and remove the syntactical overhead (i.e. all the |establish|) keywords, then we end up with precisely the original figure. This example also shows an alternative way of accessing external derivations using derivation syntax instead of function syntax. \section{Externals} \label{fig.tutorial.externals} We used several Haskell functions as external derivations in previous sections, such as |add| and |mul|. We also used some data types such as strings and integers. In this section we show how to write these functions and the infrastructure involved. \subsection{Data Types} \Ruler has no knowledge of the structure of data types. Yet we can manipulate data types through externals. We take strings as a running example. \begin{figure}[htb] \begin{code} data PrimString = PS String | IndPS IndInfo (Maybe PrimString) ^^^ genInfos :: [ GenInfo ] genInfos = [ GenInfo PrimString IndPS IndPS True, ... ] \end{code} \caption{Example of an external data structure in @src/Externals.hs@.} \label{fig.tutorial.codestring} \end{figure} A |PrimString|, given in Figure~\ref{fig.tutorial.codestring}, is a special kind of string that is either a concrete Haskell |String| wrapped inside a |PS| constructor, or an {\it indirection} |IndPS|. We use these indirections to model guesses. In \Ruler, values are extended with guesses, but these not part of Haskell. Therefore, a data type |T| to be used with \Ruler requires an indirection constructor taking an |IndInfo| and a |Maybe T|. A yet unknown guess for a string is represented as |IndPS i Nothing|, and a known guess for a string as |IndPS i (Just (PS ...))|, with |i| some unique opaque value identifying the guess. Indirections therefore never disappear from values. We use these indirections to track where a guess (or its concrete contents) end up, such that we retain sharing. A guess can occur in multiple values, and we do not want to duplicate the actual value to all these places. Furthermore, equality check on equal guesses is faster than comparing the actual values. In fact, some more optimizations are done, such as introducing indirections when two opaque values are equal, contraction of double indirections, and caching of the free variable information (which we use heavily to test that values are not cyclic). Although there is quite some effort done in order to get sharing, we do not go as far to guarantee maximal sharing. All administration of guesses is hidden from the application. However, to ensure safety, externals are not allowed to construct the indirections themselves, and ruler programs cannot match on these alternatives. The data types added to the |genInfos| list are accessible as external derivations in Ruler. The constructors are available as lambda functions using a lowercase letter for the first capital. Integers, booleans and strings occurring are automatically represented by a PrimInt, PrimBool, and PrimString respectively. We automatically produce the functionality required by ruler for the data types in this list, such as a pretty-print function, conversion functions for guesses, and a first-order unification function. \begin{figure} \begin{code} data List a = Nil | Cons (PolyInd a) (List a) | IndList IndInfo (Maybe (List a)) \end{code} \caption{Polymorphic data structure.} \label{fig.tutorial.polyexternal} \end{figure} Finally, in Figure~\ref{fig.tutorial.polyexternal} shows a polymorphic data type. Polymorphic data types are allowed, but the polymorphic occurrences must be wrapped in a |PolyInd| value. The following ruler function shows that sometimes a guess does not have a concrete type: \begin{code} \_ -> ( x fresh; cons x nil ) \end{code} Here, this function returns a list with a single element with a polymorphic type. In the Haskell world we require a representation of this value, and a |PolyInd| provides this. \subsection{External Functions} We use the names external functions and external derivations interchangeably, most often depending on whether we look at them from the \Ruler or Haskell perspective. External functions are plain Haskell functions that take a substitution and some parameters, and return an updated substitution, some results, and possibly a list of errors. For convenience, we hide the substitution and errors in the monad |I| (of which we omit the details). \begin{figure}[htb] \begin{code} extLength :: List a -> I (SingleRes PrimInt) extLength xs = do i <- chase xs extSingleResult (PI i) where chase l = extExpand l >>= chase' ^^^ chase' Nil = return 0 chase' (Cons _ r) = do r' <- chase r return (1+r') chase' (IndList _ (Just r)) = chase' r chase' (IndList _ Nothing) = abort "length of undefined list" ^^^ extMul :: FixedInOnly PrimInt -> FixedInOnly PrimInt -> I (SingleRes PrimInt) extMul (FixedInOnly (PI i1)) (FixedInOnly (PI i2)) = singleResult (PI (i1 * i2)) ^^^ extHead :: FixedInOnly (List (PolyArg a)) -> I (SingleRes (PolyArg a)) extHead (FixedInOnly Nil) = abort "head on an empty list" extHead (FixedInOnly (Cons a _)) = extSingleResult (indToPoly a) ^^^ externals :: Map Ident External externals = Map.fromList [ mkExt True "mul" extMul , mkExt True "length" extLength , mkExt True "head" extHead , ... ] \end{code} \caption{Example of an external derivation in @src/Externals.hs@.} \label{fig.tutorial.codemessage} \end{figure} Figure~\ref{fig.tutorial.codemessage} shows some example functions. The function |extLength|, computes the length of a list by walking over the spine of the list (with the function |chase|) and counting the number of steps. If the list happens to be a guess, then the guess is expanded with |extExpand|. Then either the guess is defined and the walk continues, or the guess is undefined and computing the length fails. The function |extMul| takes two integers and multiplies them. Here we use a parameter convention. The type |FixedInOnly| specifies that the parameter must be defined and that it also does not show up in any result or side effect of the function. Consequently, the input value is guaranteed not to have any indirections and we can directly match on the conventional constructors. Aside from |FixedInOnly|, also the individual components |Fixed| and |InOnly| are available. A function taking a potentially unknown polymorphic value can use and pass around values of the type |PolyArg a|. Indirections can be converted to values of this type. The |extHead| function is an example of this case. There is currently no mechanism to dynamically load externals into the ruler interpreter. Extra data types and external derivations should simply be added by extending the lists in @src/Externals.hs@. \section{Monomorphic Type Inference} \label{sect.tutorial.mono} \subsection{Guesses} We concerned ourselves mainly with the evaluation model in previous sections. In this section we look at another important concept: guesses. Guesses represents values that are not yet known during the inference process. Many type inferencers see type variables and guesses as the same concept. In Ruler these two are separate concepts. A type variable is a value in the domain of types corresponding to some known type-level abstraction (universally quantified, existentially quantified, or a constant). A guess stands for an arbitrary unknown type, which can turn out to be a variable, but also a more complicated structure. The running example in this section is an inferencer for the simply-typed lambda calculus. The type language actually does not even have a concept of type variables\footnote{Strictly spoken has the simply typed lambda calculus only function arrows, but we are a bit more flexible in this respect.}. This difference is important. If we pattern match on a type variable, we are guaranteed that this is some fixed variable, and if we would have performed the match later, it would still be that variable. Matching a guess, however, does not give us any information. We may see a guess now, but some time later this guess may have been substituted with more concrete type information. The fact that we perform a match means that a decision has to be made based on the structure of the value. This means that in case of a guess, we either are allowed to make a decision that holds for a value with any structure, or we have to delay the decision until more of the structure of the value is known. In fact, there are two different ways of matching in Ruler. Either a match fails when a concrete value is matched against a guess, or the guess is filled in with the concrete value. Pattern matches (input expressions), for example, fail when the pattern is more defined that the value matched upon. The equality statement, introduced later in this section, however, fills in guesses when of the two values it gets, parts are more defined in one value than in the other. \begin{figure} \begin{code} data Exp = ExpVar Name | ExpConst PrimInt keywords { ^^^ hfix ^^^ }; | ExpApp Exp ^^^ Exp ^^^^^ syntax expApp { ^^^ 1 @ 2 ^^^ }; | ExpLam Name Exp syntax expLam { ^^^ \1 . 2 ^^^ }; | ExpLet Name Exp Exp syntax expLet { ^^^ hlet 1 = 2 hin 3 ^^^ }; | ExpFix Exp syntax expFix { ^^^ hfix 1 ^^^ }; | ExpInd IndInfo ^^^ (Maybe Exp) ^^^^^ ^^^ data Ty = TyCon Name ^^^^^ let int = tyCon (ident "Int"); | TyArrow Ty ^^^ Ty ^^^^^ syntax tyArrow { ^^^ 1 -> 2 ^^^ }; | TyInd IndInfo ^^^ (Maybe Ty) \end{code} \caption{Data type for lambda calculus} \label{fig.tutorial.simplydata} \end{figure} \subsection{Example} The running example in this section is a type inferencer for the simply-typed lambda calculus (with some extensions). We start again with the data types and some extra syntax in Figure~\ref{fig.tutorial.simplydata}. There are no surprises here, except that we introduce an additional keyword |hfix|, to be used in combination with custom syntax. Also, we define a data type for types, with an indirection to represent guesses (see the previous section for more details about indirections). These indirections only show up in the external representation of values (when manipulating these values with external Haskell functions). A ruler program cannot see indirections, neither pattern match on them. A ruler program can therefore only find out that a value is still a guess\footnote{It is an ongoing goal to provide abstractions such that guesses cannot be observed at all until sufficiently is known that the guesses can be observed as fixed values. Many problems with predictably of type inference are related to observing and manipulating guesses. By making the inference process pure and limiting the manipulation to some fixed places, we hope to make type inferencer more predictable.} by first failing to match on any of the other constructors (or use the |getguess| external function). \begin{figure} { %format tyf = ty "_" f %format tya = ty "_" a %format tyr = ty "_" r %format tyx = ty "_" x \begin{code} syntax ^^^ { ^^^ env |- e : !ty ^^^ }; ^^^ let infer = derivation inputs env, dispatch e outputs ty { branch var: ^^^ establish lookup ^^^ { ^^^ (x -> ty) `elem` env ^^^ }; ^^^ === ^^^ establish ^^^ { ^^^ env |- expVar x : ty ^^^ }; ^^^ branch const: ^^^ === ^^^ establish ^^^ { ^^^ env |- expConst i : int ^^^ }; ^^^ branch app ^^^ tyr fresh; ^^^ establish infer ^^^ { ^^^ env |- f : tyf ^^^ }; ^^^ establish infer ^^^ { ^^^ env |- a : tya ^^^ }; ^^^ tyf == tya -> tyr; ^^^ === ^^^ establish ^^^ { ^^^ env |- f @ a : tyr ^^^ }; ^^^ branch lam ^^^ tyx fresh; ^^^ establish infer ^^^ { ^^^ (x -> tyx),env |- e : tyr ^^^ }; ^^^ === ^^^ establish ^^^ { ^^^ env |- \x.e : tyx -> tyr ^^^ }; ^^^ branch fix ^^^ ty fresh; ^^^ establish infer ^^^ { ^^^ env |- f : ty -> ty ^^^ }; ^^^ === ^^^ establish ^^^ { ^^^ env |- hfix f : ty ^^^ }; }; ^^^ derivation inputs args outputs ty { branch main: let e = parse this.args; establish infer ^^^ { ^^^ emptyenv |- e : this.ty ^^^ }; } \end{code} } \caption{Ruler program for monomorphic type inference.} \label{fig.tutorial.monocode} \end{figure} The inferencer is given in Figure~\ref{fig.tutorial.monocode}. Like in the previous section, we start with an empty environment and a parsed expression. The idea is that we know the environment and the expression, but try to find a type for the expression. Let us go through some noteworthy points of these rules. \begin{itemize} \item For the |app| branch, we infer the types of the two subexpressions. The equality statement (|==|) accomplishes that the type of the actual parameter |a| ends up to be equal to the type of the formal parameter of |f|. Upon successful execution of the equality statement, the two values are equal and stay equal until the end of the derivation. There is a variation on the equality statement called |:=|, which has the extra requirement that the value on the right must be more defined than the value on the left. Either way, such matching fails if it causes the result to be cyclic (the so called occur check)\footnote{We plan to make cycles in guesses optional and part of the indirection structure. Some operations may work regardless of certain cycles such that checking for them is not important, while cycles are strictly forbidden for other operations.}. The computation order is as usual based on input and output dependencies, such that first $\tau_r$ is introduced. Then both a derivation for |f| and a derivation for |a| can be constructed. Both are applicable at this point, and the order of execution is in this case that the statement that appears earlier in the source code executes first. These individual types are then matched against each other in the appropriate way. This form of inference corresponds to a bottom-up approach. Alternatively, we can make a top-down approach by making the type an input instead of an output, and passing guesses for each type input that we do not know beforehand. \item For the |lam| branch, we also introduce a guess. The define before use order requires us to define $\tau_x$ before we can put it in the environment. A fresh guess satisfies this requirement. \item In the |fix| branch, a guess occurs at an output of a child derivation. The expression is thus an input for this derivation. This result is required to match |ty -> ty|. A guess can only be filled once. If a guess is matched against a concrete type, then from then on the guess points to this concrete type. Matching a guess against a guess makes the guesses equal. The interpreter keeps track of indirections in the internal representation. Matching an indirection against the same indirection succeeds directly without examining the type structure further. In the match against |ty -> ty|, the first occurrence of |ty| will cause the guess to be filled in, and that the second match is either an expensive structural equality match or a fast match if the second turns out to be the same indirection. \end{itemize} \subsection{Ruler as Type System} We conclude this section by considering \Ruler as type rule specification. The two new statements, |fresh| and |==|, can be seen as two conventional relations from a specification perspective: \begin{itemize} \item |fresh| is a one-place relation for all points in the domain. \item |==| represents structural equality. \end{itemize} Furthermore, \Ruler specifies that least restraining structural result is inferred, given the order in which the equality statements were performed. Also note that \Ruler only provides an equivalence operation for obtaining structural equivalence between values. More advanced forms of (in)equalities should be encoded differently, for example by means of subtype relations\footnote{We are considering to offer forms of equality modulo normalization.}. \section{Damas-Milner} \label{sect.tutorial.milner} In this section we give the classical Damas-Milner inference algorithm in \Ruler. In previous sections, the example algorithms essentially perform a bit of pattern matching, passing values straight to subderivations and to external derivations. However, as earlier sections showed, lambda abstraction and application are available in \Ruler, and in fact many more constructs known from functional programming, such that we can actually do most of the programming in \Ruler itself. \begin{figure}[htb] { %format tyb = "\tau_b" \begin{code} data Ty = ... | TyVar Name | TyForall (List Name) Ty ^^^ derivation ... { ... branch var: let ty = instantiate (lookup x env); === establish { env |- expVar x : ty }; branch elet: establish { env |- e : tyx }; establish { (extend x (generalize env tyx) env) |- b : tyb }; === establish { env |- hlet x = e in b : tyb }; } \end{code} } \caption{Changes with respect to monomorphic type inference.} \label{fig.tutorial.dmchanges} \end{figure} The transgression from the monomorphic type inferencer to Damas-Milner is only a small step. Figure~\ref{fig.tutorial.dmchanges} shows the changes. We add type variables to types, and a universal quantifier that binds a list of these variables. We represent the variables by a plain identifier. The |var| and |elet| case are changed, such that we |instantiate| the variables quantified over in types taken from the environment, and |generalize| over the free variables at let bindings. \subsection{Visibility annotations} Before we discuss the above functions further, we first consider the relation between such functions and derivations trees. Consider the statement: \begin{code} let v = (\x -> x) 3; \end{code} Execution of this statement leads to binding |x| to value |3|. However, since we associate each function call with a node in the derivation tree, this leads in this case to the creation of a unnamed subtree in the derivation tree, with input |3| and output |3|. Even more subtrees are created when currying is involved: \begin{code} let v = (\x y -> x) 1 2 \end{code} This leads to the creation of two subtrees. First a subtree with input |1| and as output some closure |\y -> x| with |x| bound to |1|. Then a second subtree with input |2| and output |2|. This clutters the derivation tree. Therefore, we hide subtrees resulting from lambdas by default, and provide two expressions special expression forms to fine tune this behavior: { %format nm1 = nm "_1" %format nmn = nm "_n" \begin{code} abstract nm inputs nm1,...,nmn ^^^ e hide e \end{code} } The result of evaluating the |abstract| expression is the same as evaluating |e|. The difference is that aside from evaluation of |e|, also a leaf is added to the derivation tree, named |nm|, with the inputs as attributes. The inputs must be in scope of the abstract expression. A similar story applies to hide, except that none of the subtrees that may result from the evaluation of |e| are retained. Furthermore, the more general |derivation|s, and even an |establish|, can be annotated with a similar, optional, visibility annotation for even more fine grained control: \begin{code} derivation ... visibility { ... } establish nm visibility ; visibility ::= hide -- hide this node and all its children | skip -- hide this node, but show the children | abstract nm -- represent this node with the given |nm|, hide children \end{code} We make extensive use of these visibility annotations to keep derivation trees understandable, especially when using higher-order functions. \subsection{Functional programming} In \Ruler, there are generally speaking two ways to define a typing relation. Either using type rule syntax, or by using conventional functional programming. The latter is often convenient to represent small data transformations. For example, the |instantiate| and |generalize| functions. Figure~\ref{fig.tutorial.dmgeninst} shows their definitions. \begin{figure}[htb] \begin{code} let replace = \nm rep ty -> case ty of { tyVar x -> if equal nm x then rep else ty; tyArrow f a -> tyArrow (replace nm rep f) (replace nm rep a); tyForall x t -> if equal nm x then t else tyForall x (replace nm rep t); _ -> ty; }; let instantiate = \ty -> abstract instantiate inputs ty case ty of { tyForall nms t -> let { next = \nm tr -> ( t' fresh; replace nm t' tr ); } in foldr next (instantiate t) nms _ -> ty; }; let generalize = \env ty -> let { vars = abstract nonoverlap inputs ty, env ^^^ (difference (fgv ty) (fgv env)); nms = map (\g -> ident (show g)) vars; assocs = zip vars nms; tyFull = tyForall nms ty; } in ( eval sequence (\(tuple g nm) -> exec { g == tyVar nm; }) assocs; abstract generalize inputs ty, env ^^^ tyFull ); \end{code} \caption{Generalization and instantiation} \label{fig.tutorial.dmgeninst} \end{figure} \paragraph{Generalization.} We first compute the list |vars| of undefined guesses that occur in the type but not in the environment. The |fgv| external provides the list of undefined guesses. The function |difference| we show later, but its name already suggests its behavior. We then construct a list |nms|, which contains a textual representation of each of the guesses. Finally, we substitute each of these guesses with their |tyVar| representation. A new expression is the |exec| expression, which executes a sequence of statements (in order of appearance) and throws away the result. \paragraph{Instantiation.} Instantiation removes all |tyForall| constructors, and replaces the occurrences of the variables with fresh types. The |replace| function performs case distinction on the input type |ty|, and replaces recursively. This case distinction requires some explanation, since \Ruler does not have any knowledge of data types, and thus has no knowledge about patterns. The left hand side of each case alternative is a special form of an expression, consisting only of variables and applications. First the scrutiny is evaluated, and then each alternative is tried in order of appearance. Of such an alternative, the left-hand side expression is evaluated with fresh guesses for the variables occurring at argument positions. The result is then match against the value of the scrutiny, and the branch is selected if that succeeds. Pattern matching in \Ruler thus corresponds to evaluation with guesses, followed by unification. \begin{figure}[htb] \begin{code} let foldr = \f ini xs -> case xs of { @nil -> ini; cons z zs -> f z (foldr f ini zs); }; let elem = \x ys -> foldr (\y r -> if equal x y then true else r ) false ys; let difference = \xs ys -> foldr (\x r -> if elem x ys then r else cons x r ) nil xs; let map = \f xs -> case xs of { @nil -> xs; cons x ys -> cons (f x) (map f ys); }; let zip = \xs ys -> case xs of { @nil -> xs; cons x xs' -> case ys of { @nil -> ys; cons y ys' -> cons (tuple x y) (zip xs' ys'); }; }; let null = \xs -> equal (length xs) 0; \end{code} \caption{Utility functions in \Ruler.} \label{fig.tutorial.util} \end{figure} \paragraph{Utility functions} We make heavy use of some common utility functions. They are listed in Figure~\ref{fig.tutorial.util}. One particular detail is occurrence of |@nil| in the left hand side of a case alternative. Without the |@|, this would result in the value of the scrutiny bound to nil. This is not the behavior we want. We want to match the scrutiny against the value of |nil| bound in the global environment. The |@| makes sure that we reference |nil| instead of define it. An escape to arbitrary expressions is possible by using |@{ e }|. \begin{figure} \begin{code} let equal == \a b -> abstract equal inputs a, b ( inst (derivation outputs res { branch equal: a == b; this.res == true; branch unequal: this.res == false; }) as test; establish test; test.res ); \end{code} \caption{Equality-test function.} \label{fig.tutorial.equalitycode} \end{figure} The diversity of syntaxes can be mixed. Rule syntax at places where statements are expected, and functional syntax at places where expressions are expected. For example, Figure~\ref{fig.tutorial.equalitycode} shows the |equal| function, which tests of the two inputs can be made the same. If possible, it does so and returns |true|, if not, it returns |false|. \section{Damas-Milner aspect-wise} \label{sect.tutorial.milneraspect} The type system formalism does not offer sufficient abstraction when dealing with big type systems. This lack of abstraction shows up as soon as judgments have more than a handful of inputs and outputs, and when the abstract syntax becomes more complicated. For type systems published in research papers this is typically not a big problem, because such type systems deal with a single aspect in isolation, reducing the amount of book keeping that is required, and allowing the abstract syntax to be tailored to that specific situation. This luxury, however, we do not have when constructing type systems and type inference algorithms for a practical setting, where features are not isolated but crosscut and interact. To deal with such a situation, we provide mechanisms for aspect-oriented programming, such that we can describe particular aspects of the type inference algorithm in (relative!) isolation. To show this, we take example of the previous section and structure it in three separate aspects. The first aspect concerns the construction of the shape of the derivation tree, the second aspect deals with the distribution of the environment over the tree, finally the third aspect computes the type of each expression. Some of these aspects cross-cut. The environment is needed to lookup the type of an identifier, and the type of a binding is needed in order to generalize it and put it in the environment of the body of a |hlet|. We also describe this interaction between aspects. \subsection{Derivation merging} We split the |infer| derivation of the previous section into three pieces as follows: \begin{code} let infer = merge { inferBase, inferEnv, inferTy }; \end{code} The effect is that the three closures are merged, sharing the input and output attributes. The closures retain their own local scope. Sharing of local bindings must be done explicitly. \begin{figure}[htb] \begin{code} syntax { |- e }; ^^^ let inferBase = derivation inputs e { branch var exposes nm: === establish { |- expVar nm }; ^^^ branch app exposes fd, ad: establish { |- f } as fd; establish { |- a } as ad; === establish { |- f a }; ^^^ branch lam exposes x, bd: establish { |- b } as bd; === establish { |- \x.b }; ^^^ branch elet exposes x, xd, bd: establish { |- e } as xd; establish { |- b } as bd; === establish { |- hlet x = e hin b }; }; \end{code} \caption{The AST aspect.} \label{fig.tutorial.dmaspectast} \end{figure} \begin{figure}[htb] { %format tyg = ty "_g" \begin{code} syntax { env |- }; ^^^ let inferEnv = derivation inputs env { branch var exposes env: === establish { env |- }; ^^^ branch app requires fd, ad: augment fd { env |- }; augment ad { env |- }; === establish { env |- }; ^^^ branch lam requires x, bd exposes tyx: tyx fresh; augment bd { extend x tyx env |- }; === establish { env |- }; ^^^ branch elet requires x, tyg, xd, bd exposes env: augment xd { env |- }; augment bd { extend x tyg env |- }; === establish { env |- }; }; \end{code} } \caption{The environment aspect.} \label{fig.tutorial.dmaspectenv} \end{figure} \begin{figure}[htb] \begin{code} syntax { : !ty }; ^^^ let inferTy = derivation outputs ty { branch var requires nm, env: === establish { : instantiate (lookup nm env) }; ^^^ branch app requires fd, ad: augment ad { : tya }; augment fd { : tya -> tyr }; === establish { : tyr }; ^^^ branch lam requires tyx, bd: augment bd { : tyb }; === establish { : tyx -> tyb }; ^^^ branch elet requires xd, bd, env exposes tyg: augment xd { : tyx }; let tyg = generalize env tyx; augment bd { : tyb }; === establish { : tyb }; }; \end{code} \caption{The type aspect.} \label{fig.tutorial.dmaspectty} \end{figure} Figures~\ref{fig.tutorial.dmaspectast}\ref{fig.tutorial.dmaspectenv}\ref{fig.tutorial.dmaspectty} show the three individual derivations. It is still possible to use rule syntax even when the derivations are split up. We demonstrate this extensively. The derivation in Figure~\ref{fig.tutorial.dmaspectast} is intended to construct the base structure of the derivation tree. It recursively dispatches on |e|. We |expose| those locals that we want to share with others, and |require| locals that we need others to share. In Figure~\ref{fig.tutorial.dmaspectenv} we add the |env| attribute. We distribute it accordingly, passing it to the two child derivations in the |app| branch. In the |lam| branch, we add a binding for |x|, which may be looked up in subderivations. In the |elam| branch, we require a type |tyg| to be defined, which we use as the type for |x| in the body of the let. Then finally we add the |ty| attribute, as shown in Figure~\ref{fig.tutorial.dmaspectty}. We lookup the type and instantiate it for the |var| branch, we extract the result-part in the |app| branch, build the arrow-type in the |lam| branch, and define the type |tyg| in the |elet| branch to be shared with the |elet| branch of |inferEnv|. Writing these aspects separately, allows us to focus on the bare essentials. This becomes especially important when the number of inputs and outputs grow. \subsection{Inheritance} An alternative way to merge derivations is through inheritance. An |inherit| expression is of the form: { %format en = e "_" n \begin{code} inherit e { e1, ..., en } \end{code} } Here |e, e1, ..., en| all evaluate to closures. Then |e| incorporates the statements in |e1, ..., en| in the order of appearance. Statements subsumed by statements in |e| are not incorporated. The inheriting expression |e| has access to the full scope of |e1, ..., en| and can |requires| any definition in |e1,..,en|. \begin{figure}[htb] \begin{code} let dm = derivation { branch var requires x, env: this.ty == instantiate (lookup x env); branch elet requires env, tyx, bd: bd.env == extend x (generalize env tyx) env; }; ^^^ let inferDM = inherit dm { infer }; \end{code} \caption{Damas-Milner from monomorphic with inheritance.} \label{fig.tutorial.inheritdm} \end{figure} Figure~\ref{fig.tutorial.inheritdm} shows how to obtain a type inferencer for Damas-Milner by inheriting from the type inferencer of the simply-typed lambda calculus. The equalities on |this.ty| and |bd.env| in the original definition of |infer| are overriden by these in |dm|. %if False \begin{figure}[htb] \begin{code} let testlist = cons 1 (cons 2 (cons 3 nil)); ^^^ let elemsIdDeriv = derivation inputs x outputs y { branch main: this.y == this.x; }; ^^^ let sum = derivation outputs y { branch cons requires hd, tl: this.y == add hd.y tl.y; branch nil: this.y == 0; }; ^^^ let walkList = \d -> ( let ds = derivation inputs xs { branch cons: cons !x !xs := this.xs; inst d as hd; hd.x == x; establish hd; inst this as tl; tl.xs == xs; establish tl; branch nil: nil := this.xs; }; ds ); ^^^ derivation inputs args outputs y { branch main: let e = inherit (walkList elemsIdDeriv) { sum }; inst e as d; d.xs == testlist; establish d; this.y == d.y; } \end{code} \caption{Inheritance example} \label{fig.tutorial.inherit} \end{figure} %endif \subsection{Abstract Statements} The previous sections showed how to import, share and override statements. In this section, we present a mechanism to specify default behavior using abstract statements. An Abstract statement is a template that can be instantiated automatically to many concrete statements. It is prefixed with the keyword |abstract| to mark the difference. Abstract statements may contain abstract field expressions: \begin{code} first.x -- matches the first child with attribute |x|, or |this.x| otherwise. last.x -- matches the last child with attribute |x|, or |this.x| otherwise. all.x -- matches all children with attribute x, returning a list. any.x -- matches any child with attribute |x| pred.x -- only in combination with |any|, matches the first predecessor with |x|. succ.x -- only in combination with |any|, matches the first successor with |x|. \end{code} For example, when we inherit the following derivation: \begin{code} derivation inputs env { branch var, app, lam, elet: abstract any.env == this.env; } \end{code} we get as default behavior that the environment is passed down to all the children. When there are multiple occurrences of |any| in such an abstract statement, then they all point to the same concrete child for a single instantiation of this abstract statement. \subsection{More!} We intent to have more mature variants of the aspect-oriented programming concepts in future versions of \Ruler. More fine grained control over what is exported and imported, and the possibility to merge and inherit with renaming. \section{Repmin} \label{sect.tutorial.repmin} The evaluation model of Ruler is eager. This is a problem when an input depends on an output. A typical example is the @repmin@ problem. In @repmin@, a function must transform a tree, replacing all leafs with the minimal value in the tree. This cannot be done with a single function in a strict language. Problems similar to the repmin problem arise often in type inferencing. The typical case is than some information from deeper inside the abstract syntax tree is needed. For example, to type a group of mutual recursive definitions, one may first want to obtain a list of possible type signatures defined on the definitions before proceeding with type inference. The conventional solution is to write separate helper functions, with the downsides that subresults are not shared (with consequences for efficiency and also aspect-oriented programming), and that we do not want to split up a typing relation, because the derivation trees are then totally different. \Ruler's solution is to allow visiting a partial application multiple times, using the inputs and intermediate results from visits up to the current, and producing the outputs of the current visit. \begin{figure}[htb] %{ %format :-: = "\leftrightarrowtriangle" \begin{code} syntax ^^^ { finMin |- t : !gathMin ~> !t' }; syntax node ^^^ { 1 :-: 2 }; syntax leaf ^^^ { <1> }; ^^^ let testtree = (<8> :-: <5>) :-: (<3> :-: <9>); ^^^ let repmin = derivation inputs t inputs finMin visit disperse outputs gathMin outputs t' visit disperse { ^^^ branch node: establish repmin ^^^ ^^^ m ^^^ |- ^^^ l ^^^ : ^^^ lm ^^^ ~> ^^^ l'; establish repmin ^^^ ^^^ m ^^^ |- ^^^ r ^^^ : ^^^ rm ^^^ ~> ^^^ r'; === establish m ^^^ ^^^ |- ^^^ l :-: r ^^^ : ^^^ min lm rm ^^^ ~> ^^^ l' :-: r'; branch leaf: === establish ^^^ ^^^ min ^^^ |- ^^^ ^^^ : ^^^ i ^^^ ~> ; }; ^^^ derivation inputs args outputs t { ^^^ branch main: establish repmin ^^^ ^^^ m ^^^ |- ^^^ testtree ^^^ : ^^^ m ^^^ ~> ^^^ this.t; } \end{code} %} \caption{Repmin in \Ruler.} \label{fig.tutorial.repmincode} \end{figure} Figure~\ref{fig.tutorial.repmincode} shows the repmin example in \Ruler. Inputs and outputs are marked with visit names. Those inputs and outputs of the first visit are not marked. The order of the visits can be explicitly given, but is in this case inferred automatically. In the first visit, |repmin| takes a tree |t| as input, and produces an output |gathMin|, the minimum of the subtree. Then in the second visit, named |disperse|, the minimum of the entire tree (bound to |m| in the main derivation) is passed back as the input |finMin|. The result tree consists of leaves with this |finMin| as value. \section{Conclusion} This tutorial showed the basis underlying the \Ruler language. We made a connection between derivation trees, functional programs, and type rules. In \Ruler, both type rules as well as functional programs are expressed as a single aspect-oriented programming language. Not covered in this tutorial are special annotations in relation to guesses. Dealing with the gradual availability of the contents of guesses is the core business of a type inferencer. Futhermore, we did not discuss the type system of ruler, and neither why this is necessairy for efficient compilation to attribute grammars.