Santiago M.
Pericas-Geertsen
Boston University
Download and unpack the zip file dl.zip. The downloadable package includes the script dl than can be used to run the interpreter. The interpreter can be started with type checking turned off (useful for prototyping) by typing dl --untyped. Files can be loaded into the interpreter's environment using <dl:load> (cf. Section 12.10).
As a "proof of concept" we have implemented an interpreter for a language based on the \delta\lambda-Calculus. We refer to this language as DL. This chapter describes the syntax of DL as well as the semantics of a few constructs that are not present in the basic calculus.
Following a current trend (in languages such as XSLT, XML Schemas, etc.), we have opted for an XML-based syntax for the language DL. Thus, every DL expression is a legal XML document. The advantages of this approach are the following:
Expressions (programs) can be embedded as part of XML documents. For example, an XML document can carry an "embedded stylesheet", which is a piece of DL code that translates the contents of the document to a displayable format such as HTML.
Off-the-shelf tools, such as validating parsers, can be used to implement compilers/interpreters for DL.
Programmable text editors (e.g., Emacs or XEmacs) can be easily extended to aid programmers write syntactically correct code.
Based on our experience, the only disadvantage of using an XML-based syntax is the fact that programs tend to be long due to the verbosity of the constructs. However, to a certain extent, this problem is offset by the use of an extension to our editor of choice to help in the creation/edition of DL programs.
As in other languages whose syntax is XML-based, we employ XML namespaces to distinguish active vs. passive data. More specifically, every expression <<expr>> presented to our interpreter is evaluated in the following context:
<?xml version="1.0"?>
<dl:top-level xmlns:dl="http://types.bu.edu/xml/dlcalculus"
xmlns:ty="http://types.bu.edu/xml/dlcalculus/types">
<<expr>>
</dl:top-level>which adds the XML header <?xml version="1.0"?>, so that a standard XML parser recognizes the document as parsable, and also defines the namespaces dl and ty. Therefore, every subexpression in <<expr>> of the form <dl:...> or <ty:...> will be recognized as a construct in DL as opposed to passive data (as suggested by their names, the prefix dl is reserved for terms and the prefix ty is reserved for types).
The following meta-variables are used throughout this chapter for the presentation of the syntax:
s, s1, . . . range over an infinite set of strings;
l, l1, . . . range over an infinite set of labels;
x, y, z, f, g, t, t1, . . . range over an infinite set of variable names;
n, m range over the set of natural numbers.
The set of strings, labels and variable names coincide with the set of text nodes, element names and attribute values, respectively, as defined in the W3C Recommendation for XML.
Strings in the DL language define the contents of a document. Thus, everything that is not markup is a string or, using XML terminology, a text node. Although not necessary in general, it is also possible to define a string using the construct <dl:string>. For example, the following two expressions are identical:
This is an e-mail message.
<dl:string>This is an e-mail message.</dl:string>
The expression <dl:string> is often needed for readability --specially when the string spans multiple lines-- and to define the empty string as <dl:string/>.
Labeled expressions in the \delta\lambda-Calculus are written as l< D > for some expression D and label l. In the DL language, we use the more standard (and more verbose!) syntax where D is delimited by <l> and </l>. To exemplify, the e-mail message from Example 6.2 is written as:
<email> <sender>santiago@cs.bu.edu</sender> <receiver>all@cs.bu.edu</receiver> <subject>An e-mail message as an XML document</subject> <message>This is an e-mail message.</message> </email>
Strings and labeled expressions are evaluated in accordance to the operational semantics defined in Section 7.1 for the \delta\lambda-Calculus. That is, a string evaluates to itself and a labeled expression evaluates to a labeled expression (of the same label) where its sub-expression is fully evaluated.
Tuples in the \delta\lambda-Calculus are written as D1, . . . , Dn; thus each component of a tuple is separated by a ",". In DL, following standard XML syntax, tuples can be implicit. That is, tuples can be defined simply by writing a sequence of expressions one after the other with no delimiters or separators. For example, the expression
<sender>santiago@cs.bu.edu</sender> <receiver>all@cs.bu.edu</receiver> This is an e-mail message.
is a tuple of length 3 where the first two components are labeled expressions and the last component is a string. The BNF syntax for tuples of expressions (a similar rule is used for tuple of types) is defined by the following production:
<<dl-tuple>> ::= <<dl-expr>> | <<dl-expr>> <<dl-tuple>>
It is also possible (and often necessary) to define a tuple explicitly. The expression <dl:tuple> can be used for that purpose. For example, the explicit tuple that corresponds to the implicit tuple shown above is
<dl:tuple> <sender>santiago@cs.bu.edu</sender> <receiver>all@cs.bu.edu</receiver> This is an e-mail message. </dl:tuple>
Regardless of whether a tuple is implicit or explicit, its components can be selected using <dl:project>. For example, the expression
<dl:project index="2">
<dl:tuple>
<sender>santiago@cs.bu.edu</sender>
<receiver>all@cs.bu.edu</receiver>
This is an e-mail message.
</dl:tuple>
</dl:project>evaluates to <receiver>all@cs.bu.edu</receiver>. The projection index is specified by means of the (mandatory) attribute index, whose value must be a number greater or equal to 1.
As in the \delta\lambda-Calculus, lists in DL are defined using the standard constructors "nil" and "cons". The syntax for these constructors is the following:
<dl:nil/> <dl:cons>
<<dl-tuple>>
<<dl-expr>>
</dl:cons>Note that the first argument to <dl:cons> is (implicitly) a tuple. That is, everything but the last sub-expression of <dl:cons> is inserted into the list. For example, the following expression evaluates to a list whose only element is a tuple of two labeled expressions:
<dl:cons> <sender>santiago@cs.bu.edu</sender> <receiver>all@cs.bu.edu</receiver> <dl:nil/> </dl:cons>
It is also possible to use <dl:list> as a constructor, but this is just syntactic sugar for an expression containing nested <dl:cons>, in the same way [D1, ... , Dn] is sugar for D1 :: ... (Dn :: [ ]) in the \delta\lambda-Calculus. For example, the expression
<dl:list> <sender>santiago@cs.bu.edu</sender> <sender>all@cs.bu.edu</sender> </dl:list>
defines a list of two elements both of which are labeled expressions. Notice that the <dl:list> constructor does not group any sub-expressions into tuples; this effect can be achieve by the explicit use of <dl:tuple>.
Lists in DL can be accessed using the standard destructors "head" and "tail". The syntax for these destructors is the following:
<dl:head> <dl:tail> <<dl-expr>> <<dl-expr>> </dl:head> </dl:tail>
It is worth pointing out that the sub-expression of both <dl:head> and <dl:tail> is not allowed to be a tuple, as such an expression will inevitably generate a type error (or a run-time error in a dynamically-typed framework). In accordance to the operational semantics defined for the \delta\lambda-Calculus, a list must be fully evaluated before its head or its tail can be accessed.
Variables can be either global or local. The former are defined using <dl:define> and the latter using <dl:let>. The syntax of these expressions is shown next:
<dl:define name="x"> <dl:let name="x">
<<dl-tuple>> <<dl-tuple>>
</dl:define> <dl:in/>
<<dl-tuple>>
</dl:let>A <dl:define> expression evaluates to the value of its sub-expression, binding that value to the variable defined by the attribute name as a side effect.
The value of a variable named "x" can be accessed by writing <dl:variable name="x"/>. Since a variable is one of the base cases of our syntax, a <dl:variable> expression in DL is required to be an empty XML element (as indicated by the use of "/").
The expressions <dl:select>, <dl:project>, <dl:head> and <dl:tail> can be regarded as document destructors. Due to the inherent structure of XML documents, DL expressions encounter in practice often contain sub-expressions where these destructors appear nested. For example, suppose "D" is defined as follows:
<dl:define name="D">
<email>
<sender>santiago@cs.bu.edu</sender>
<dl:list>
<receiver>all@cs.bu.edu</receiver>
<receiver>santiago@cs.bu.edu</receiver>
</dl:list>
</email>
</dl:define>In order to select the e-mail address of the first receiver, we need an expression that traverses the tree denoted by D from the root and returns the second leaf. Namely,
<dl:select label="receiver">
<dl:head>
<dl:project index="2">
<dl:select label="email">
<dl:variable name="D"/>
</dl:select>
</dl:project>
</dl:head>
</dl:select>Since expressions such as the one shown above are common in DL, a special (more succint) syntax is also provided. Specifically, the last expression can also be written as <dl:expr value="D/email.2.hd/receiver"/>. The path expression "D/email.2.hd/receiver" is intended to be read from left to right: first select email, then project the second component, then take the head and finally select receiver. The syntax of path expressions is defined in Section 12.12.
As in the \delta\lambda-Calculus, DL provides ways of defining and applying lambda abstractions. The syntax for these two constructs is the following:
<dl:abstraction param="x" param-type="t"> <dl:application>
<<dl-tuple>> <<dl-expr>>
</dl:abstraction> <<dl-tuple>>
</dl:application>The attributes param and param-type are required in <dl:abstraction>. These two attributes are used, respectively, to declare the name and the type of the variable being bound. Recall that t ranges over a set of variable names; the reader is referred to Section 12.8 for further details on how these type variables are declared.
A <dl:application> expression expects at least two sub-expressions. Notice that, according to the syntax shown above, all but the leftmost sub-expression of <dl:application> are regarded as an implicit tuple. For example, for an appropriate definition of the type variable "t", the following expression shows how the identity function is applied to a binary tuple.
<dl:application>
<dl:abstraction param="x" param-type="t">
<dl:variable name="x"/>
</dl:abstraction>
<email>santiago@cs.bu.edu</email>
<email>all@cs.bu.edu</email>
</dl:application>Since, in practice, abstractions are often given names, DL provides special constructs for defining and applying named functions. The syntax for these two constructs is the following:
<dl:function name="f" param="x" param-type="t"> <dl:function-call name="f"> <<dl-tuple>> <<dl-tuple>> </dl:function> </dl:function-call>
An additional advantage of the use of <dl:function> over <dl:abstraction> is that the former allows for definitions to be recursive. In fact, the syntax of <dl:function> shown above can be regarded as sugar for
<dl:define name="f">
<dl:fix-point param="f" param-type="t'">
<dl:abstraction param="x" param-type="t">
<<dl-tuple>>
</dl:abstraction>
</dl:fix-point>
</dl:define>where <dl:fix-point> is the DL construct that corresponds to (fix f : \sigma.D) in the \delta\lambda-Calculus, and where "t'" denotes an arrow type whose domain is "t" and whose codomain is the type of <<dl-tuple>>.
The type system of DL is based on that presented in Chapter 8 for the \delta\lambda-Calculus. In addition to the type constructors presented in that chapter, DL includes (i) type variables and (ii) a <ty:void/> type. The reader is referred to Section 12.12 for the complete syntax of all the type constructors available in DL. As in the case of expressions, a sequence of types with no separators or delimiters defines an implicit tuple type. For example, the following type denotes lists whose components are binary tuples of labeled expressions:
<ty:list> <ty:email><ty:string/></ty:email> <ty:email><ty:string/></ty:email> </ty:list>
Using the syntax from Chapter 8, this type would be written as (email<string>, email<string>)*. Notice that the syntax of labeled types is <ty:email>...</ty:email> instead of the more intuitive syntax <email>...</email>. Thus, the label of a labeled type also belongs the namespace defined by the prefix ty, a requirement that simplifies the task of the parser.
Type variables can be globally defined using the <ty:define> construct. Type variables play an important role in DL since they are needed to define the value of the param-type attribute in expressions such as <dl:abstraction> and <dl:function>. For example, the following fragment of DL code shows how to define a type variable and then a function whose domain is the type assigned to the variable.
<ty:define name="Email"> <ty:email><ty:string/></ty:email> </ty:define> <dl:abstraction param="x" param-type="Email"> <dl:expr value="x/email"/> </dl:abstraction>
Types in DL can also be evaluated. Every type constructor that is not a type variable evaluates to itself; bound type variables evaluate to the types introduced via <ty:define>. Thus, as evaluation is inductive on the structure of types, it is possible to define types using type variables. To exemplify, the list type shown above can also be written as
<ty:list> <ty:variable name="Email"/> <ty:variable name="Email"/> </ty:list>
provided the type variable Email is defined as in the last example. The evaluation of a type fails only if an unbound type variable is referenced via <ty:variable>; the type of every type expression is <ty:kind/>.
There is an alternative way of assigning a name to a type: every element that has ty as prefix also accepts an optional attribute name. This feature is particularly useful when defining union types since the subcomponents of these types must be named as well (cf. Section 12.9). As an example, lets define the type Recipient as follows:
<ty:union name="Recipient">
<ty:email name="Email">
<ty:string/>
</ty:email>
<ty:newsgroup name="Newsgroup">
<ty:string/>
</ty:newsgroup>
</ty:union>Injections and Cases in DL are similar in structure to their \delta\lambda-Calculus counterparts, except that instead of using types we use type variables --as in other typed constructs like <dl:abstraction> and <dl:function>-- to annotate the terms. The syntax for these two constructs is shown next.
<dl:inject type="x" name="t"> <dl:case bind="x">
<<dl-tuple>> <<dl-expr>>
</dl:inject> <dl:match name="t1">
<<dl-tuple>>
</dl:match>
...
<dl:match name="tn">
<<dl-tuple>>
</dl:match>
</dl:case>The notation "..." that is part of the syntax of <dl:case> indicates that the number of <dl:match>'s is unbounded. In fact, the number of <dl:match>'s must coincide with the number of types in the union type in question (cf. Figure 8.1).
DL provides a few additional contructs that are not part of (and cannot be de-sugared into) the underlying calculus. In this section we cover <dl:load> and <dl:display>.
The <dl:load> construct is used to load definitions into the interpreter's environment. The syntax is <dl:load filename="<<file-name>>"/>. Expressions in <<file-name>> are evaluated in order, and the result of the evaluation is <dl:void/> (and, hence, the type of a <dl:load> is <ty:void/>).
The <dl:display> construct is used to pretty print the value of an expression. The syntax of this expression is:
<dl:display> <<dl-tuple>> </dl:display>
As <dl:load>, the evaluation of <dl:display> produces a side effect, namely, adding one or more characters to the standard output. The result of evaluating a <dl:display> is also <dl:void/> (and, hence, the type of a <dl:display> is also <ty:void/>).
Let us show how Example 8.2.2 from Section 8.2 can written using the syntax of DL. We begin by defining the type of an XML e-mail, the type of an HTML e-mail and the types of the functions F and G.
<ty:define name="XMLEmail">
<ty:email>
<ty:sender><ty:string/></ty:sender>
<ty:list name="RecsList">
<ty:receiver><ty:string/></ty:receiver>
</ty:list>
<ty:subject><ty:string/></ty:subject>
<ty:message><ty:string/></ty:message>
</ty:email>
</ty:define>
<ty:define name="HTMLEmail">
<ty:html>
<ty:head>
<ty:h3><ty:string/></ty:h3>
</ty:head>
<ty:body>
<ty:list>
<ty:p><ty:string/></ty:p>
</ty:list>
</ty:body>
</ty:html>
</ty:define>
<ty:define name="Type-G">
<ty:arrow>
<ty:variable name="RecsList"/> <ty:string/>
</ty:arrow>
</ty:define>
<ty:define name="Type-F">
<ty:arrow>
<ty:variable name="XMLEmail"/>
<ty:variable name="HTMLEmail"/>
</ty:arrow>
</ty:define>Notice how the type of F and the type of G, respectively Type-F and Type-G, are defined in terms of the type variables XMLEmail, HTMLEmail and RecsList, and also how the latter names a subpart of the type bound to XMLEmail. Given these type definitions, document d1 and functions F and G are defined as follows:
<dl:define name="d1">
<email>
<sender>santiago@cs.bu.edu</sender>
<dl:list>
<receiver>all@cs.bu.edu</receiver>
<receiver>santiago@cs.bu.edu</receiver>
</dl:list>
<subject>An e-mail message as an XML document</subject>
<message>This is an e-mail message.</message>
</email>
</dl:define>
<dl:function name="G" param="z" name-type="Type-G">
<dl:if>
<dl:null>
<dl:variable name="z"/>
</dl:null>
<dl:then/>
<dl:string/> <!-- null string -->
<dl:else/>
<dl:concat>
<dl:expr value="z.hd/receiver"/>
<dl:function-call name="G">
<dl:expr value="z.tl"/>
</dl:function-call>
</dl:concat>
</dl:if>
</dl:function>
<dl:function name="F" param="x" name-type="Type-F">
<dl:let name="y">
<dl:expr value="x/email"/>
<dl:in/>
<html>
<head>
<h3><dl:expr value="y.3/subject"/></h3>
</head>
<body>
<dl:list>
<p><dl:expr value="y.1/sender"/></p>
<p>
<dl:function-call name="G">
<dl:expr value="y.2"/>
</dl:function-call>
</p>
<p><dl:expr value="y.4/message"/></p>
</dl:list>
</body>
</html>
</dl:let>
</dl:function>This example also illustrates the use of <dl:if> and <dl:let>. The <dl:if> expression is used in conjunction with the empty DL expressions <dl:then/> and <dl:else/>, and is evaluated in the standard way (i.e. if the value of its first sub-expression is <dl:true/> then the "then" case is evaluated, if it is <dl:false/> then the "else" case is evaluated). The evaluation of <dl:let> is also standard, and follows from the way let expressions are de-sugared into applications.
<<tuple>> ::= <<dl-tuple>> | <<ty-tuple>>
<<dl-tuple>> ::= <<dl-expr>> | <<dl-expr>> <<dl-tuple>>
<<dl-expr>> ::= s
| <dl:nil/>
| <dl:cons>
<<dl-tuple>>
<<dl-expr>>
</dl:cons>
| <dl:tuple>
<<dl-tuple>>
</dl:tuple>
| <l>
<<dl-tuple>>
</l>
| <dl:head>
<<dl-expr>>
</dl:head>
| <dl:tail>
<<dl-expr>>
</dl:tail>
| <dl:project index="n">
<<dl-tuple>>
</dl:project>
| <dl:select label="l">
<<dl-expr>>
</dl:select>
| <dl:variable name="x"/>
| <dl:abstraction param="x" param-type="t">
<<dl-tuple>>
</dl:abstraction>
| <dl:application>
<<dl-expr>>
<<dl-tuple>>
</dl:application>
| <dl:true/>
| <dl:false/>
| <dl:concat>
<<dl-expr>>
<<dl-expr>>
</dl:concat>
| <dl:fix-point param="x" param-type="t">
<<dl-tuple>>
</dl:concat>
| <dl:if>
<<dl-expr>>
<dl:then/>
<<dl-tuple>>
<dl:else/>
<<dl-tuple>>
</dl:if>
| <dl:null>
<<dl-tuple>>
</dl:null>
| <dl:labeled label="l">
<<dl-tuple>>
</dl:labeled>
| <dl:inject type="x" name="t">
<<dl-tuple>>
</dl:inject>
| <dl:case bind="x">
<<dl-expr>>
<dl:match name="t1">
<<dl-tuple>>
</dl:match>
...
<dl:match name="tn">
<<dl-tuple>>
</dl:match>
</dl:case>
| <dl:string>s</dl:string>
| <dl:define name="x">
<<dl-tuple>>
</dl:define>
| <dl:function name="f" param="x" param-type="t">
<<dl-tuple>>
</dl:function>
| <dl:function-call name="f">
<<dl-tuple>>
</dl:function-call>
| <dl:expr value="<<path-expr>>"/>
| <dl:let name="x">
<<dl-tuple>>
<dl:in/>
<<dl-tuple>>
</dl:let>
| <dl:load filename="s"/>
| <dl:list>
<<dl-tuple>>
</dl:list>
| <dl:display>
<<dl-tuple>>
<dl:display>
| <dl:void/>
<<path-expr>> ::= x
| <<path-expr>>.n
| <<path-expr>>/l
| <<path-expr>>.hd
| <<path-expr>>.tl
<<ty-tuple>> ::= <<type>>
| <<type>> <<ty-tuple>>
<<type>> ::= <ty:void/>
| <ty:bool/>
| <ty:string/>
| <ty:variable name="t"/>
| <ty:l>
<<ty-tuple>>
</ty:l>
| <ty:list>
<<ty-tuple>>
</ty:list>
| <ty:tuple>
<<ty-tuple>>
</ty:tuple>
| <ty:union>
<<ty-tuple>>
</ty:union>
| <ty:arrow>
<<ty-tuple>>
<<type>>
</ty:arrow>
| <ty:define name="t">
<<ty-tuple>>
</ty:define>