% File: tl-report.tex % Date: 08-JAN-1993 % Author: Florian Matthes % % Change Log: % 6-NOV-92 FM Renamed type rule ``Subtype Var Elim'' into ``Subtype Var'' % Removed bug two other type rules: replaced ``a:A'' by ``a:X'' % 8-NOV-92 FM Changed syntax of modules / imports % 22-NOV-92 FM Fixed incorrect signatures syntax % Changes syntax of interfaces [no bindings] % Changed syntax of type signatures [allow Let] % Introduced colonInfix % Removed restriction on conditions % Removed valueBinding restriction from arrays % % 08-JAN-1993 A. Rudloff % Preparation for FB-Report: % - ``Zusammenfassung'' % - titlepage % - \LARGE section headings % - small decorations % %--------------------------------------------------------------------- % Uses art11.sty on same directory for \LARGE section headings %--------------------------------------------------------------------- % %\documentstyle[tycoon,florian-named,epsf,declarations]{article} % %\newcommand{\dq}{\verb$"$} % %\title{Definition of the Tycoon Language \TL\ -- A Preliminary Report} %\titleid{DBIS Tycoon Report 062-92} %\titlestatus{Revised} %\date{22-NOV-1992} %\author{Florian Matthes\\Joachim W.~Schmidt} % %\titledescription{This document defines the language \TL\ that is used %as the application and system programming language in the Tycoon %database environment. The Tycoon project follows an \e{add-on} approach %to generic database programming that emphasizes type-safe system %scalability and extensibility. \\ %\TL\ is a polymorphic second-order functional language with imperative %features and inductively defined subtyping rules over types and type %operator, extended by language constructs motivated by the needs of %database programming.} % %\titlerelated{Using the Tycoon Compiler Toolkit \cite{SchMa92} %} \documentstyle[11pt,a4,florian-named,epsf,declarations,twoside]{article} \pagestyle{headings} \topmargin -0.5cm % seems to be necessary ??? % also defined in tycoon.sty \newcommand{\e}[1]{{\em #1\/}} \newcommand{\k}[1]{{\bf #1}} \newcommand{\comment}[1]{\par{[*** #1 ***]}\par} \newcommand{\p}[1]{{\frenchspacing\sl{}#1}} \newcommand{\reply}[1]{{\bf$\Rightarrow$} #1} \def\longhrule{\par\hbox to \linewidth{\hss \hbox to \textwidth{\hrulefill}}\par} \newcommand{\dq}{\verb$"$} \title{\vspace*{5.5cm} \normalsize Bericht Nr. 160\\[6ex] \Large\bf Definition of the Tycoon Language \TL\ \\[0.2cm] A Preliminary Report} \author{Florian Matthes \and Joachim W.~Schmidt} \date{$ $ \\[0.4cm] \hspace*{8.5cm} \normalsize FBI-HH-B-160/92\\[5cm] Dezember 1992\\[3ex] Fachbereich Informatik\\ Universit\"at Hamburg\\ Vogt-K\"olln-Str. 30\\ D-W-200 Hamburg 54\\ Federal Republic of Germany} \begin{document} \maketitle \thispagestyle{empty} \newpage $ $ \\[6cm] \begin{abstract} \thispagestyle{empty} \noindent This document defines the language \TL\ that is used as the application and system programming language in the Tycoon database environment. The Tycoon project follows an \e{add-on} approach to generic database programming that emphasizes type-safe system scalability and extensibility. \vspace*{5pt} \noindent \TL\ is a polymorphic second-order functional language with imperative features and inductively defined subtyping rules over types and type operator, extended by language constructs motivated by the needs of database programming. \vspace*{1cm} \begin{center} \bf{Zusammenfassung} \end{center} \noindent Dieses Dokument definiert die Sprache \TL\ \hspace{-1mm}, die sowohl als Anwendungs- als auch Systemprogrammiersprache in der Tycoon Datenbankumgebung verwendet wird. Das Tycoon Projekt folgt dem \e{add-on}-Ansatz zur generischen Datenbankprogrammierung, der besonders die typsichere Systemskalierbarkeit und -erweiterbarkeit unterst\"{u}tzt. \vspace*{5pt} \noindent \TL\ ist eine polymorphe funktionale Programmiersprache zweiter Ordnung mit imperativen Eigenschaften und induktiv definierten Subtypisierungsregeln \"{u}ber Typen und Typoperatoren, erweitert um Sprachkonstrukte, die durch die Anforderungen der Datenbankprogrammierung begr\"{u}ndet sind. \end{abstract} \newpage \pagenumbering{roman} \tableofcontents \thispagestyle{plain} \newpage \section{The Rationale behind \TL} \thispagestyle{plain} \pagenumbering{arabic} The functionality of data-intensive applications is provided by a heterogeneous mix of tools and servers that have been developed independently and that typically communicate only via narrow, ad-hoc interfaces. Examples of commercially available \e{generic} servers are relational database systems, object stores, transaction monitors, deduction engines, graphical user interface generators or communication subsystems. The \e{Tycoon}\footnote{Tycoon: Typed COmmunicating Objects in Open eNvironmens} project aims at a substantially improved server exploitation and database programmer productivity by providing an integrated linguistic and architectural framework for the \e{flexible integration of generic services} into an open database programming environment. The Tycoon project activities towards this goal include \cite{Matt92} \begin{itemize} \item the development and formal definition of a highly generic language kernel supporting naming, binding and typing of objects and services required for data-intensive applications in a way that is not biased towards a specific data model. \item the extension of this language kernel to a fully-fledged strongly-typed polymorphic programming language (\TL, \e{Tycoon Language}) that also includes specific language concepts for integrating, extending, tailoring and using the generic database servers mentioned above; \item the definition of the data and program representation as well as the evaluation semantics of an untyped intermediate language (\TML, \e{Tycoon Machine Language}) that not only supports an efficient host-specific target code generation but also portability, interoperability in heterogeneous environments and dynamic optimizations analogous to query optimization in database systems; \item the definition of a data-model-independent object store protocol (\TSP, \e{Tycoon Store Protocol}) that decouples \TML\ evaluators from object stores and their components for access optimization, storage reclamation, persistence, concurrency, recovery or distribution. \end{itemize} The overall Tycoon system architecture is sketched in Fig.~\ref{Fig:Tycoon-Architecture} on page~\pageref{Fig:Tycoon-Architecture}. This report presents the design of \TL, an integrated application and system programming language that \begin{itemize} \item provides uniform and expressive naming, binding and scoping rules for all language entities (values, functions, types, type operators), \item is not restricted to a particular modeling or programming style (e.g. purely functional, relational or strictly object-oriented), \item minimizes built-in language functionality in favor of flexible system add-ons \cite{MaSc91b}, \item is equipped with powerful type abstraction mechanisms like (bounded) type parameterization, (parital) type hiding and run-time type discrimination \cite{MaSc91}, \item supports the operational requirements of todays data-intensive environments (longevity, evolution, distribution, merging of independently developed system components) \cite{ScMa90b}. \end{itemize} A first prototypical set of the \TL\ language processors (scanner, parser, unparser, type checker, variable allocator, \TL\ to \TML\ translator , \TML\ to C translator, \TML\ interpreter, dynamic object code linker) is currently being implemented at Hamburg University using the \mbox{P-Quest} system, a persistent version of the Quest language developed by Luca Cardelli \cite{Card89,Card90} on top of the Napier Persistent Object Store develped at the University of St.~Andrews \cite{BrRo90}. Much emphasis is put on the exchangability and reusability of the individual compiler components by using (wherever possible) compiler generator technology \cite{SchMa92}. \begin{figure} %\begin{maxipage} \begin{center}\leavevmode \epsfxsize=0.7\textwidth \epsfbox{Tycoon-Layers-Engl.ps} \end{center} \caption{Layers and interfaces of the Tycoon system} \label{Fig:Tycoon-Architecture} %\end{maxipage} \end{figure} \newpage \section{\TL: A Language Overview} \thispagestyle{plain} The type-theoretic core of \TL\ is \fsub, a second-order lambda calculus with subtyping \cite{CMMS91}. This core is extended by a rather small set of standard programming concepts (base types, tuples, arrays, control structures and exceptions) as found in other functional or imperative programming languages. Some of the characteristic features of \TL\ are sketched below. \begin{description} \item[Syntax] The regular LL(1) grammar for the concrete syntax of \TL\ is heavily influenced by languages like Modula-2 , Modula-3 and Quest that all give preference to notations that are easy to read and understand over concise or cryptic notations that are easy to write . \TL\ provides adequate notations for the non-trivial bindings and signatures that occur in highly polymorphic library code. It emphasizes the symmetry between constructs at the value and type level and supports the easy discrimination between value and type expressions to simplify type inference in bindings. \item[Base Types] \TL\ carefully avoids any non-standard treatment (like static binding, pervasive scoping, non-standard associativity, precedence or overloading) of the usually built-in functions on base types (integers, reals, strings, etc.). In order to achieve maximum system flexibility, these functions are provided by modules in the standard programming environment. The module implementations are written in C (resp.~Modula-2) and are dynamically or statically linked to the generated \TML\ or C code. Standard optimization techniques in the C backend (i.e.\ inlining) eliminate most of the possible overhead implied by this approach. Flexible handling of the base types is also supported by the treatment of integer, real, character and string \e{literals} within the relevant \TL\ language processor components (scanner, type checker, code generator). \item[Mutability] Value variables in a \TL\ binding or signature can be marked with a \k{var} keyword. The phrase \p{\k{let var} i = 1}) introduces a \e{mutable} binding between the variable \p{i} and the value 1. The variable \p{i} can be re-bound using a polymorphic assignment function in the Tycoon programming environment. This function has the signature \p{:=(A $<$:\k{Ok} \k{var} lhs :A rhs :A)} and can redeclared locally (e.g.~to attach recovery code to the destructive assignment). Mutable bindings cover the the concepts of local and global imperative variables, mutable components in aggregate values and also variable parameters as found in imperative programming languages. Variable parameters introduce \e{l-value} bindings (\e{aliasing}). Modifiability in \TL\ is therefore not captured by first-class type and value constructors (like \k{ref} in ML) but is a property of bindings and signatures. Imperative and functional realms of \TL\ cannot be strictly separated since it is possible to view a mutable binding through a signature that defines the binding as immutable. The latter language design decision is motivated by the desire to provide both, flexible subtyping and assignment in a statically typed programming language (for an in-depth discussion of alternative approaches see \cite{CMR91}). \item[Bindings and Signatures] \TL\ recognizes the importance of naming, scoping and binding concepts in large-scale programming. Therefore, the main semantic building blocks of \TL\ are not values and types in isolation but bindings (ordered associations of types to type variables and of values to value variables) and signatures (ordered associations of types to type bounds and values to types) (see also \cite{BuLa84,Card89}). The scoping rules for type and variable names, the matching rules between bindings and their signatures and the refinement relation on signatures can all be specified without reference to the paticular context in which bindings or signatures occur. Possible contexts for signatures include formal function parameters, module interfaces as well as function types, tuple, record and exception types. Possible contexts for bindings include actual function parameters, module implementations, tuple, record and exception values and top level phrases entered interactively. \TL\ allows to \k{Repeat} another named signature in the definition of a new signature and to \k{open} (a projection of) existing bindings for the definition of new bindings. These language mechanisms can substantially improve the understandability and consistency of large-scale systems by factoring-out common subsignatures and subbindings. In the context of tuples and records they also cover aspects of \e{inheritance} as found in object-oriented languages. \item[Higher-Order Subtyping] Type judgements in \TL\ are understood as \e{partial} specifications. For example, the signature \p{x :A} asserts that a value bound to the variable \p{x} satisfies \e{at least} the specification given by the type expression \p{A}. An actual value binding \p{\k{let} x = a} may satisfy a more precise specification \p{x :B}. The idea that a value satisfying a stronger specification \p{B} also satisfies a weaker specification \p{A} is captured by an inductively defined subtyping relationship on types (\TL\ notation: \p{B $<:$ A}). For aggregate values, this view coincides with the notion of subtyping based on information content \cite{OBBT89}. For example, the type \p{\k{Let} A = \k{Tuple} name :String \k{end}} provides less information than the type \p{\k{Let} B = \k{Tuple} name :String age :Int \k{end}}. The view of types as partial specifications generalizes to first-class function values and leads to the well-known contravariance rule for the function type constructor. \TL\ provides two type constants to denote the trivial specification (\k{Ok}, top type) and the unsatisfiable specification (\k{Nok}, bottom type). The latter appears naturally in the typing rules for exceptions and empty arrays (see~\refpar{Keyword:Array-Empty}). In \TL\ it is necessary to specify a \e{bound} for a type variable that appears in a signature (e.g., \p{X $<:$A}). Again, this bound is to be understood as a partial specification of the actual type that appears in the matching binding \p{\k{Let} X = B} and may involve the constants \k{Ok} and \k{Nok}. Finally, \TL\ extends the subtyping relation to type operators, i.e. parameterized specifications (see~\refpar{Keyword:Subtype-Oper}) \define{Subtype Oper}{ \dedtwoh{ \judge{S}{\tlsubsig{S''}{S'}} } { \judge{\tlconssig{S}{S''}}{\tlsubtype{A}{B}} } { \judge{S}{\tlsubtype{\tlOper{S'}{A}}{\tlOper{S''}{B}}} }} For example, given \begin{xple} \k{Let} F = \k{Oper}(X $<:$\k{Tuple} name :String \k{end}) \k{Tuple} x :X y :X \k{end} \k{Let} G = \k{Oper}(X $<:$\k{Tuple} name :String age :Int \k{end}) \k{Tuple} x :X \k{end} \end{xple} \p{F $<:$G} is derivable, since any specification \p{F(X)} obtained by instantiating \p{F} with an actual type parameter \p{X} that is admissable for \p{G} yields a specification that is at least as strong as \p{G(X)}. The introduction of a top type \k{Ok} and the generalization of the subtyping relation to type operators also covers the notion of \e{kinds} (types of types), as introduced in \cite{Card89}. For example, all unbounded unary type operators (e.g.\ \p{List, Array}) are subtypes of \p{\k{Oper}(X $<:$\k{Ok}) \k{Ok}}. \item[Abstract Types] \TL\ follows the tradition of modular languages like Modula-2, Modula-3, Oberon and Quest and uses the dot notation to denote the witness type in an abstract data type, for example: \begin{xple} \k{Let} Nat = \k{Tuple} T$<$:\k{Ok} zero :T succ(:T) :T eq(:T :T) :T \k{end} \k{let} nat1 = \k{Tuple} \k{Let} T = Int \ldots \k{end} \k{let} nat2 = \k{Tuple} \k{Let} T = String \ldots \k{end} \k{let} null(x :nat1.T) = nat1.eq(x nat1.zero) \k{let} null2(rep :Nat x :rep.T) = rep.eq(x rep.zero) \end{xple} Bound specifications in the signature of an abstract data type allow to reveal partial type information about the witness type \p{T} (e.g.~compatibility with other witness types). Special (path name equivalence) rules are introduced for a flexible handling of ADT values in complex data structures. \item[Recursive Type Operators] The subtyping rules for recursive types and type operators in \TL\ violate the concept of purely structural subtyping. For example, given \begin{xple} \k{Let Rec} List(A $<:$ \k{Ok}) = \k{Tuple} hd :A tl :List(A) \k{end} \k{Let Rec} List2(A $<:$ \k{Ok}) = \k{Tuple} hd :A tl :\k{Tuple} hd :A tl :List(A) \k{end} \k{end} \end{xple} none of the following subtype relationships is derivable: \begin{xple} List(\k{Ok}) $<:$List2(\k{Ok}) List2(\k{Ok}) $<:$List(\k{Ok}) List $<:$List2 List2$<:$List \end{xple} On the other hand, a single step ``unfolding'' of \p{List(A)} in the definition of \p{List} yields a type operator that is structurally equivalent to \p{List2}: Since the equality between two recursive types in \TL\ is therefore not based on the equality of their infinite expansions (two regular tree) but on a more restrictive compatibility notion (see also \cite{Card92}), the problem of checking the equivalence between parameterized recursive type expressions becomes decidable (compare \cite{Solo78}) and a class of subtype relationships that play an important role in object-oriented programming can be handled within \TL. For example, given \begin{xple} \k{Let Rec} List(E $<:$\k{Ok}) = \k{Tuple} cons(:E) :List(E) hd() :E tl() :List(E) map(E2 $<:$\k{Ok} f(:E) :E2) :List(E2) \k{end} \k{Let Rec} List2(E $<:$\k{Ok}) = \k{Tuple} cons(:E) :List2(E) hd() :E tl() :List2(E) map(E2 $<:$\k{Ok} f(:E) :E2) :List2(E2) powerset(p(:E) :Bool) :List2(List(E)) \k{end} \end{xple} \p{List2(Int) $<:$List(Int)} and \p{List2 $<:$List} are derivable type judgements in \TL. \item[Tuples and Variants] The concepts of discriminated union and labeled cartesian product types are both captured by tuples with variants in \TL. A pure discriminated union type is represented by a tuple type with variants that do not share common fields while a pure cartesian product type is represented by a tuple type with a single variant and an anonymous variant label. A prime motivation behind this unification is to simplify the handling of discriminated unions that share common attributes between their variants. Another motivation is to provide a type-safe solution to a common problem in persistent systems, namely the need for unforeseen extensions and variations of data structures without invalidating existing persistent bindings (in databases, files or possibly compiled programs). For example, an early system version may introduce the following binding \begin{xple} \k{Let} Address = \k{Tuple} city :String zip :Int \k{end} \k{let} a :Address = \k{tuple} \k{let} city = "Hamburg" \k{let} zip = 2000 \k{end} \end{xple} that is still usable in an extended system version with the following type and function definitions: \begin{xple} \k{Let} NewAddress = \k{Tuple} city :String \k{case} national \k{with} zip :Int \k{case} international \k{with} country :String zip :String \k{end} \k{let} print(adr :NewAddress) :\k{Ok} = \ldots print(a) \end{xple} \item[Extensible Records] As argued in \cite{AtMo85,MAD87,ScMa90b}, long-lived data-intensive applications require naming schemes that are capable of handling \e{dynamic} collections of bindings as they are found, for example, in directory structures of operating systems or in data dictionaries of databases. Extensible records address this need and provide a particular combination of static type safety and dynamicity that blends well with the subtyping rules of \TL. Record extension operations are also useful for modelling object-oriented programming concepts like objects with an immutable identity or method dictionaries. In contrast with other bindings and signatures in \TL, record bindings are unordered. Neither duplicate nor anonymous variable names are permitted in record bindings and record signatures. \begin{xple} \k{let} db = \k{record} \k{let} parts = \ldots \k{let} suppliers = \ldots \k{end} \end{xple} The selection of a field in a record value \p{db.parts} is checked statically against the signature of the record type and never fails at run-time. The extension of a record value with additional bindings \p{\k{let} newDB = \k{extend} db \k{with} \k{let} assembly = \ldots \k{end}} yields a record value with the same identity as \p{db} and additional static type information. However, the extension operation may fail at run-time by raising an exception due to name clashes (e.g.\ in cases where \p{db} is already extended by a field \p{assembly}). In contrast to Napier88 \cite{DCBM89}, there is no mechanism to remove an existing binding from a record. There are several proposals to also check the record extension operation statically, essentially by encoding \e{negative} information in record type expressions (e.g.\ values of record type \p{X} are defined not have an \p{assembly} field) \cite{Card92a,Wand87,Stan88,CaMi89,Remy91}. The usefulness of the these type rules in type system that make heavy use of the subsumption rule is not yet clear. Therefore, the design of \TL gives up some static type safety in favor of language simplicity. Since record types are subject to more flexible type rule than plain tuple types, they are also of interest even if the dynamicity provided by the \k{extend} operator is not required: The record type \p{\k{Record} S \k{end}} is a subtype of \p{\k{Record} S' \k{end}} if the signatures \p{S} can be obtained by dropping subsignatures at arbitrary positions from \p{S'} (see \refdef{Subsig Rcd} in \refpar{Keyword:Subsig-Rcd}). The subtype graph for record types can therefore form a DAG (\e{multiple inheritance}) and not just a tree (\e{single inheritance}) like for tuple types. \item[Modules and Libraries] The modularization facilities in \TL\ are \k{interface}, \k{module} and \k{library}. An interface is a named tuple type. A module is a named parameterless function. The evaluation of that function during module linkage returns a tuple value of its interface type. There may be more than one module implementing the same interface. The scope for interface and module names is defined by a library. The scope for interface, module and library names is flat. A library may contain other libraries as its component. All components of a nested library except those explicitly listed in a \k{hide} phrase are visible in the surrounding library. A library, an interface and a module may refer to other libraries, interfaces or evaluated modules only through \k{import} statements. Cyclic import dependencies are not allowed. If a module \p{m1} is imported into a module \p{m2}, the evaluation of \p{m1} precedes the evaluation of \p{m2}. The modularization facilities in \TL\ do not introduce \e{new} naming, typing and binding concepts into the language, they simply \e{restrict} the orthogonality of the existing concepts (functions, tuple types, nesting of scopes, sequential evaluation). These restrictions are designed to simplify the tool-supported maintenance of large (possibly persistent and partially bound) software systems (component replacement, incremental interface extension, type specialization). \item[Dynamic Types] In analogy to the mutability attribute for value variables, a dynamic (\k{Dyn}) attribute can be assigned to type variables in bindings and signatures. The only difference between dynamic and non-dynamic type variables is the possibility to inspect the type associated with a type variable at run-time by means of a structured \k{typecase} statement. Compared with other proposals \cite{ACPP90,ACPR92} this approach to dynamic types does not require to explicitly inject and project individual values into infinite union types and blends well with automatic inference mechanisms for type components in bindings. Furthermore, it allows to perform reflective type analysis even in cases where no value of the dynamic type is available\footnote{The semantics of the subtype test at run-time, in particular the equivalence of abstract data types, still needs to be studied in further detail.}. \item[Locality Control] The evaluation of a \TL\ program can depend on bindings in a pre-populated (persistent) store and typically establishes new bindings or produces side-effects in the store. The syntax for value constructors (functions, tuples, records, arrays) allows the specification of an object \e{locality}. This provides an abstract mechanism to control the allocation of structured values in a non-homogeneous (partitioned) object store. This explicit control is required by applications that are sensitive to differences in the operational support provided by different store partitions (e.g.\ recovery, concurrency control mechanisms). Locality specifications are run-time values of the abstract type \p{Locality} defined in the Tycoon standard library. Future versions of \TL\ may introduce (parital) locality specifications at the type level to statically control the side effects of \TL\ programs on object store partitions \cite{MOS91}. \end{description} With respect to decidability, \TL\ is in the same position as \fsub \cite{Pier92}. Decidability problems arise through the subtyping rule \refdef{Subtype Fun} in combiation with the subsignature rule \refdef{Subsig Ide}. More precisely, there exist syntactically well-formed, but ill-typed \TL\ programs for which the \TL\ type checker does not terminate. By disallowing the specialization of bound types assigned to type variables in polymorphic procedures (rule \refdef{Subsig Ide}) in the context of rule \refdef{Subtype Fun}, termination of the subtype algorithm can be guaranteed \cite{Pier92}. \newpage \section{The \TL\ Grammar} \thispagestyle{plain} The following notation is used for the definition of syntactical and lexical elements. \p{Id} denotes a non-terminal symbol (a meta variable) and \p{A} and \p{B} denote syntactic expressions. \begin{center} \begin{tabular}{ll} \\ \p{Id$_1$, \ldots, Id$_n$::= A;} & the non-terminal symbols \p{Id$_i$} are defined as \p{A} ($n\geq1$) \\ \p{Id} & a non-terminal symbol \\ \k{if} & a terminal symbol \\ \synquot{x} & the character \p{x} (\synquot{} is the empty string \synquot{\dq} is a double quote) \\ \synbrack{A} & means \p{A} \\ \p{A B} & means \p{A} followed by \p{B} (binds strongest) \\ \p{A $|$ B} & means \p{A} or \p{B} \\ \synopt{A} & means \synbrack{\synquot{} $|$ A} \\ \synrep{A} & means \synbrack{\synquot{} $|$ A \synrep{A}} \end{tabular} \end{center} \subsection{Symbols}\label{Sec:TL-Symbols} \label{Sec:TL-Grammar} The source text of a \TL\ program consists of a sequence of characters that is converted into a sequence of symbols of the categories \p{int, real, longreal, char, string, identifier, infix, colonInfix} and \p{delimiter}. The set of formatting characters is an implementation-dependent subset of the non-printable characters and includes at least the characters space, tab, carriage return, line feed and vertical tab. Comments are sequences of arbitrary printable or formatting characters that are enclosed by \mbox{\p{(* *)}}. Comments can be nested. To read a symbol, all formatting characters are skipped and then the longest sequence of characters that forms a symbol is read. Therefore, a space in the source text is only required between two identifiers or two (colon-) infix symbols that appear in direct succession. \begin{xple} int::= \verb$["~"]$ digit \synrep{digit} ; real::= int \synquot{.} digit \synrep{digit} $|$ int \synopt{\synquot{.} digit \synrep{digit}} \synquot{E} int ; longreal::= int \synopt{\synquot{.} digit \synrep{digit}} \synquot{D} int ; char::= \synquot{'} \synbrack{digit $|$ alpha $|$ special $|$ escape $|$ delimiter $|$ reserved} \synquot{'} ; string::= \synquot{\dq} \synrep{digit $|$ alpha $|$ special $|$ escape $|$ delimiter $|$ reserved} \synquot{\dq} ; infix::= special \synrep{special} ; colonInfix::= \synquot{:} \synrep{special} ; identifier::= alpha \synrep{digit $|$ alpha} ; delimiter::= \synquot{(} $|$ \synquot{)} $|$ \synquot{\{} $|$ \synquot{\}} $|$ \synquot{[} $|$ \synquot{]} $|$ \synquot{.} $|$ \synquot{,} $|$ \synquot{;} ; digit::= \synquot{0} $|$ \synquot{1} $|$ \synquot{2} $|$ \synquot{3} $|$ \synquot{4} $|$ \synquot{5} $|$ \synquot{6} $|$ \synquot{7} $|$ \synquot{8} $|$ \synquot{9} ; alpha::= \synquot{A} $|$ \synquot{B} $|$ ... $|$ \synquot{Z} $|$ \synquot{a} $|$ \synquot{b} $|$ ... $|$ \synquot{z} ; reserved::= \verb$"~"$ $|$ \synquot{ } ; special::= \verb^"@" | "#" | "$" | "%" | "&" | "*" | "_" | "+" | "=" | "-" |^ \verb$"|" | "\" | "`" | ":" | "<" | ">" | "/" | "^" | "?" | "!" $ ; escape::= \verb$"\"$ $($\synquot{n} $|$ \synquot{t} $|$ \synquot{r} $|$ \synquot{f} $|$ \verb$"\"$ $|$ \verb$"'"$ $|$ \synquot{\dq} $|$ digit digit digit$)$ ; \end{xple} Escape characters in character and string literals are interpreted as follows: \begin{center} \begin{tabular}{|l|l|} \hline \verb$\n$ & new line \\ \verb$\t$ & tab\\ \verb$\r$ & carriage return \\ \verb$\f$ & form feed \\ \verb$\'$ & \verb$'$ \\ \verb$\"$ & \verb$"$ \\ \verb$\\$ & \verb$\$ \\ \verb$\nnn$ & A single character with the code \p{nnn} \\ & (three decimal digits that denote an integer in the interval [0,255]\\ \verb$\$f \ldots f\verb$\$ & The sequence of formatting characters \p{f} is ignored\\ \hline \end{tabular} \end{center} The last rule enables the definition of string literals that exceed the length of a single source line. The above definitions allow a scanner implementation that requires just a single character lookahead. \subsection{Reserved Keywords} \label{Sec:TL-Keywords} The following identifiers and (colon-) infix symbols are reserved keywords and cannot be used as user-defined identifiers in \TL\ programs. \begin{xple} \k{and andif begin case do downto else elsif end exception exit export extend fun hide if import in interface let library loop module of ok open orif raise reraise rec then try tuple typecase upto var when while with Dyn Exception Fun Let Nok Ok Oper Rec Repeat Tuple} = $<:$ : ? ! \end{xple} \subsection{Compilation Units} Based on the symbols and keywords defined in the previous sections, the grammar of \TL\ is described by the following productions that define a non-ambiguous LL(1) grammar. \p{Unit} is the root production for the language. \label{Keyword:Unit-Syntax} \begin{xple} Unit::= \synbrack{Library $|$ Interface $|$ Module $|$ Import $|$ Bindings} \synquot{;} ; Library::= \k{library} identifier Import \k{with} \synrep{ComponentSignatures} \synopt{\k{hide} \synrep{identifier}} \k{end} ; ComponentSignatures::= \k{library} \synrep{identifier} $|$ \k{interface} \synrep{identifier} $|$ \k{module} \synrep{identifier \synquot{:} identifier} ; Interface::= \k{interface} identifier Import \k{export} Signatures \k{end} ; Module::= \k{module} identifier Import \k{export} Bindings \k{end} ; Import::= \synopt{\k{import} \synrep{\synopt{\synquot{:}} identifier}} ; \end{xple} \subsection{Bindings} \begin{xple} Bindings::= \synrep{TypeBindings $|$ ValueBindings $|$ \k{open} ValueIde \synopt{\synquot{:} Type} \synquot{:} \synopt{\k{Dyn}} Type $|$ \synopt{\k{var}} Value} ; TypeBindings::= \synrep{\k{Let} \synopt{\k{Rec}} TypeBinding \synrep{\k{and} TypeBinding}} ; TypeBinding::= \synopt{\k{Dyn}} TypeIde Parameters \synopt{\synquot{$<:$} Type} \synquot{=} Type ; ValueBindings::= \synrep{\k{let} \synopt{\k{rec}} ValueBinding \synrep{\k{and} ValueBinding}} ; ValueBinding::= \synopt{\k{var}} ValueIde Parameters \synopt{\synquot{:} Type} \synquot{=} Value ; \end{xple} \subsection{Values} \begin{xple} Value::= Value$_1$ \synrep{\synbrack{\k{orif} $|$ \k{andif} $|$ colonInfix} Value$_1$} ; Value$_1$::= Value$_2$ \synrep{infix Value$_2$} ; Value$_2$::= Value$_3$ \synrep{\synquot{(} Bindings \synquot{)} $|$ \synquot{?} CaseIde $|$ \synquot{!} CaseIde $|$ \synquot{.} FieldIde $|$ \synquot{[} Value \synquot{]} $|$ \k{of} Bindings Location \k{end}} ; Value$_3$::= \verb$"{"$ Value \verb$"}"$ $|$ ValueIde $|$ \k{ok} $|$ int $|$ char $|$ string $|$ real $|$ longreal $|$ \k{fun} \synquot{(} Signatures \synquot{)} \synopt{\synquot{:} Type} Location Value $|$ \k{tuple} Location \synopt{\k{case} CaseIde \k{of} Type \synopt{\k{with}}} Bindings \k{end} $|$ \k{record} Location Bindings \k{end} $|$ \k{extend} Value \k{with} Bindings \k{end} $|$ \k{array} Location Bindings \k{end} $|$ \k{exception} Value \synopt{\k{with} Signatures \k{end}} $|$ \k{begin} Location Bindings \k{end} $|$ \k{if} Value \k{then} Bindings \synrep{\k{elsif} Vakue \k{then} Bindings} \synopt{\k{else} Bindings} \k{end} $|$ \k{case} \synopt{\k{of}} Value \synrep{\k{when} CaseIdeList \synopt{\k{with} ValueIde} \k{then} Bindings} \synopt{\k{else} Bindings} \k{end} $|$ \k{typecase} \synrep{ValueIde \synquot{.}} TypeIde \synrep{\k{when} Type \k{then} Bindings} \synopt{\k{else} Bindings} \k{end} $|$ \k{loop} Bindings \k{end} $|$ \k{exit} $|$ \k{while} Value \k{do} Bindings \k{end} $|$ \k{for} ValueIde \synquot{=} Value \synbrack{\k{upto} $|$ \k{downto}} Value \k{do} Bindings \k{end} $|$ \k{try} Bindings \synrep{\k{when} Value \synopt{\k{with} ValueIde} \k{then} Bindings} \synopt{\k{else} Bindings} \k{end} $|$ \k{raise} Value \synopt{\k{with} Bindings \k{end}} $|$ \k{reraise} $|$ \k{assert} Value ; Location::= \synopt{\k{in} Value} ; \end{xple} \vspace*{-1mm} \subsection{Signatures} \begin{xple} Signatures::= \synrep{TypeSignatures $|$ ValueSignatures $|$ TypeBindings $|$ \k{Repeat} Type} ; TypeSignatures::= \synopt{\k{Dyn}} \synopt{TypeIdeList Parameters} \synquot{$<:$} Type ; ValueSignatures::= \synopt{\k{var}} \synopt{ValueIdeList Parameters} \synquot{:} Type ; Parameters::= \synrep{\synquot{(} Signatures \synquot{)}} ; \end{xple} \vspace*{-1mm} \subsection{Types} \begin{xple} Type::= Type$_1$ \synrep{colonInfix Type$_1$} ; Type$_1$::= Type$_2$ \synrep{infix Type$_2$} ; Type$_2$::= Type$_3$ \synrep{\synquot{(} \synrep{Type} \synquot{)}} ; Type$_3$::= \verb$"{"$ Type \verb$"}"$ $|$ \synrep{ValueIde \synquot{.}} TypeIde $|$ \k{Ok} $|$ \k{Nok} $|$ \k{Fun} \synquot{(} Signatures \synquot{)} \synquot{:} Type $|$ \k{Tuple} Signatures \synrep{\k{case} CaseIdeList \synopt{\k{with} Signatures}} \k{end} $|$ \k{Record} Signatures \k{end} $|$ \k{Exception} \synopt{\k{with} Signatures \k{end}} $|$ \k{Oper} \synquot{(} Signatures \synquot{)} \synopt{\synquot{$<:$} Type} Type ; \end{xple} \newpage \subsection{Identifier} \begin{xple} ValueIdeList, TypeIdeList, CaseIdeList::= Ide \synrep{\synquot{,} Ide} ; Ide, ValueIde, TypeIde, FieldIde, CaseIde::= identifier $|$ infix $|$ colonInfix $|$ \verb$"{"$ Ide \verb$"}"$ ; \end{xple} \newpage \section{The \TL\ Abstract Syntax} \thispagestyle{plain} The concrete syntax of \TL\ provides several abbreviating notations for values, types, bindings and signatures and makes heavy use of initial and final keywords. A compact abstract syntax provides a more adequate starting point for the definition of the static semantics of \TL. It also constitutes the canonical internal representation used by the \TL\ language processors. \subsection{Syntactic Objects of \TL} The definition of the abstract \TL\ syntax involves syntactic objects that are denoted by meta variables according to the following conventions: \begin{center} \begin{tabular}{ll} $S \in$ \p{Sig} & sequences of signatures \\ $D \in$ \p{Bind} & sequences of bindings \\ $E \in$ \p{BindElem} & single bindings \\ $A,B \in$ \p{Type} & types \\ $C \in$ \p{Case} & variants in tuple types \\ $z \in$ \p{CaseIde} & variant labels \\ $X,Y \in$ \p{Ide} & type identifiers \\ $x,y \in$ \p{ide} & value identifiers \\ $a,b,c \in$ \p{Value} & values \\ $p,q \in$ \p{Qualifier} & selectors of signature components\\ \end{tabular} \end{center} The infinite sets \p{Ide}, \p{ide} and \p{CaseIde} are built from the union of the symbols of the categories \p{identifier}, \p{infix} and \p{colonInfix} as defined in \refpar{Sec:TL-Symbols} extended by the symbol \k{?}, called the \e{anonymous} identifier. These sets and the set of literals (symbols of the categories \p{int, real, longreal, char, string}) constitute the basis for the inductive definition of the sets of the other syntactic objects as summarized in table \ref{Table:TL-Types} and table \ref{Table:TL-Values}. \subsection{Normalization of \TL\ Programs} The one-to-one translation from a parse tree of a phrase matching the concrete \TL\ syntax into an equivalent term in the abstract \TL\ syntax is rather straightforward. It is (conceptually) preceded by a normalization process that \begin{itemize} \item introduces the anonymous identifier \k{?} in bindings \begin{center} \begin{tabular}{lcl} \p{:A a} & $\Rightarrow$ & \p{\k{Let} \k{?} = A \k{let} \k{?} = a} \end{tabular} \end{center} and in signatures \begin{center} \begin{tabular}{lcl} \p{$<:$A :B} & $\Rightarrow$ & \p{\k{?} $<:$A \k{?} :B} \end{tabular} \end{center} An anonymous identifier \k{?} matches any other identifier $x,X$ in the subtyping rules for signature matching \refdef{Subsig ide, Subsig Ide, Subsig Ide Let} in \refpar{Sec:TL-Subsignatures}. \item expands abbreviating notations in bindings \begin{center} \begin{tabular}{lcl} \p{\k{let} x(S$_1$) \ldots (S$_n$) :A = a} & $\Rightarrow$ & \p{\k{let} x = \k{fun}(S$_1$) \ldots \k{fun}(S$_n$) :A = a} \\ \p{\k{let} x(S$_1$) \ldots (S$_n$) = a} & $\Rightarrow$ & \p{\k{let} x = \k{fun}(S$_1$) \ldots \k{fun}(S$_n$) = a} \\ \p{\k{Let} X(S$_1$) \ldots (S$_n$) $<:$A = B} & $\Rightarrow$ & \p{\k{Let} X = \k{Oper}(S$_1$) \ldots \k{Oper}(S$_n$) $<:$A = B} \\ \p{\k{Let} X(S$_1$) \ldots (S$_n$) = A} & $\Rightarrow$ & \p{\k{Let} X = \k{Oper}(S$_1$) \ldots \k{Oper}(S$_n$) = A} \end{tabular} \end{center} and in signatures \begin{center} \begin{tabular}{lcl} \p{x$_1$, \ldots, x$_n$ :A} & $\Rightarrow$ & \p{x$_1$ :A \ldots x$_n$ :A} \\ \p{\k{var} x$_1$, \ldots, x$_n$ :A} & $\Rightarrow$ & \p{\k{var} x$_1$ :A \ldots \k{var} x$_n$ :A} \\ \p{\k{Dyn} X$_1$, \ldots, X$_n$ $<:$A} & $\Rightarrow$ & \p{\k{Dyn} X$_1$ $<:$A \ldots \k{Dyn} X$_n$ $<:$A} \\ \p{x(S$_1$) \ldots (S$_n$) :A} & $\Rightarrow$ & \p{x :\k{Fun}(S$_1$) \ldots :\k{Fun}(S$_n$) :A} \\ \p{X(S$_1$) \ldots (S$_n$) $<:$A} & $\Rightarrow$ & \p{X :\k{Oper}(S$_1$) \ldots \k{Oper}(S$_n$) A} \end{tabular} \end{center} \item transforms infix and listfix function applications into a standard prefix notation \begin{center} \begin{tabular}{lcl} \p{x$_1$ \e{infix} x$_2$} & $\Rightarrow$ & \p{\{\e{infix}(x$_1$ x$_2$)\}} \\ \p{x$_1$ \e{colonInfix} x$_2$} & $\Rightarrow$ & \p{\{\e{colonInfix}(x$_1$ x$_2$)\}} \\ \p{f \k{of} x$_1$ \ldots x$_n$ \k{end}} & $\Rightarrow$ & \p{f(\k{array} x$_1$ \ldots x$_n$ \k{end})} \end{tabular} \end{center} \item transforms infix type operator applications into prefix notation \begin{center} \begin{tabular}{lcl} \p{X$_1$ \e{infix} X$_2$} & $\Rightarrow$ & \p{\{\e{infix}(X$_1$ X$_2$)\}} \\ \p{X$_1$ \e{colonInfix} X$_2$} & $\Rightarrow$ & \p{\{\e{colonInfix}(X$_1$ X$_2$)\}} \end{tabular} \end{center} \item replaces missing \k{else} branches in \k{if}, \k{try} and \k{typecase} expressions (but not in \k{case} expressions) by an empty expression sequence (that evaluates to \k{ok}, see \refdef{Value seq empty} in \refpar{Sec:TL-Values}), for example, \begin{center} \begin{tabular}{lcl} \p{\k{if} a \k{then} b \k{end}} & $\Rightarrow$ & \p{\k{if} a \k{then} b \k{else} \k{end}} \end{tabular} \end{center} \item normalizes \k{elsif} branches into nested \k{if} expressions \begin{center} \begin{tabular}{lcl} \begin{minipage}{5cm} \begin{xple} \k{if} a$_1$ \k{then} b$_1$ \k{elsif} a$_2$ \k{then} b$_2$ \ldots \k{end} \end{xple} \end{minipage} & $\Rightarrow$ & \begin{minipage}{5cm} \begin{xple} \k{if} a$_1$ \k{then} b$_1$ \k{else} \k{if} a$_2$ \k{then} b$_2$ \ldots \k{end} \k{end} \end{xple} \end{minipage} \end{tabular} \end{center} \item replaces assertions by conditionals \begin{center} \begin{tabular}{lcl} \k{assert} a & $\Rightarrow$ & \begin{minipage}{7cm} \begin{xple} \k{if} a \k{then} \k{ok} \k{else} \k{raise} \k{exception} ``Assertion in file \ldots at line \ldots failed'' \k{end} \k{end} \end{xple} \end{minipage} \end{tabular} \end{center} \end{itemize} \subsection{Signatures, Bindings and Types} Table~\ref{Table:TL-Types} summarizes the inductive definition of signatures, bindings and types in \TL. \begin{table} %\begin{maxipage} \begin{center} \begin{tabular}{rll} $S::=$ & $\tlemptysig$ & empty signature \\ $|$ & $\tlconssig{S}{\tlhastype{x}{A}}$ & value signature \\ $|$ & $\tlconssig{S}{\tlsubtype{X}{A}}$ & type signature \\ $|$ & $\tlconssig{S}{\tllettype{X}{A}}$ & type definition \\ $|$ & $\tlconssig{S}{\tlRepeat{A}}$ & signature inheritance \\ $;$ & $$ & \\ $D::=$ & $\tlemptybnd$ & empty binding \\ $|$ & $\tlconsbnd{D}{E}$ & sequential binding \\ $|$ & $\tlconsbnd{D}{E_1 | \ldots | E_n}$ & parallel binding\\ $|$ & $\tlconsbnd{D}{{\bf open}(x)}$ & binding inheritance\\ $|$ & $\tlconsbnd{D}{{\bf open}(x,A)}$ & binding projection \\ $;$ & $$ & \\ $E::=$ & $\tlbnd{x}{a}$ & value binding \\ $|$ & $\tlbndrestr{x}{A}{a}$ & constrained value binding \\ $|$ & $\tlbnd{X}{A}$ & type binding \\ $|$ & $\tlbndRestr{X}{A}{B}$ & constrained type binding \\ $;$ & $$ & \\ $A,B::=$& $\tlOk$ & supertype of all types (\engl{top})\\ $|$ & $\tlNok$ & subtype of all types (\engl{bottom})\\ $|$ & $X$ & type identifier\\ $|$ & $\tlDot{p}{X}$ & abstract type identifier\\ $|$ & $\tlBool\,|\,\tlInt\,|\,\tlString$ & base type identifiers\\ $|$ & $\tlArr{A}$ & array type\\ $|$ & $\tlFun{S}{A}$ & (polymorphic) function type\\ $|$ & $\tlTup{S}{C}$ & tuple type (with variants)\\ $|$ & $\tlRcd{S}$ & record type\\ $|$ & $\tlExc{S}$ & exception type\\ $|$ & $\tlRec{X}{X}{A}{B}{n}$ & recursive type ($1 \leq n$) \\ $|$ & $\tlVar{A}$ & type of mutable values\\ $|$ & $\tlDyn{A}$ & dynamic type\\ $|$ & $\tlOper{\tlconstwosig{\tlsubtype{X_1}{A_1}} {\ldots} {\tlsubtype{X_n}{A_n}}} {B}$ & type operator \\ $|$ & $\tlApply{A}{D}$ & type operator application \\ $;$ & $$ & \\ $C::=$ & $\tlCase{z_1}{S_1} \ldots \tlCase{z_n}{S_n}$ & variants in tuple types ($0 \leq n$)\\ $;$ & $$ & \\ $p::=$ & $x$& value signature selector \\ $|$ & $\tlDot{p}{x}$ & field signature selector \\ $;$ & $$ & \end{tabular} \end{center} \caption{Abstract syntax for signatures, bindings and types} \label{Table:TL-Types} %\end{maxipage} \end{table} The distinction between type signatures and type definitions in signatures reflects the fact that most type judgements provide a partial information ($\tlsubtype{X}{A}$) and that only in few cases (e.g.~\k{Let} type bindings in the local scope) the \e{exact} type associated with a type variable $X$ is available ($\tllettype{X}{A}$). The base type constants ($\tlInt$, $\tlBool$ \ldots) are required to denote the types of \TL\ literals and the argument types expected by built-in language constructs (e.g.~booleans for the conditional). They do not appear in the concrete \TL\ syntax since they are not hard-wired as keywords but bound to identifiers in the programming environment. The rather heavy notation for recursive types is required to directly represent mutually recursive type bindings, like \begin{xple} \k{Let Rec} X$<:$\k{Ok} = F(Y) \k{and} Y$<:$\k{Ok} = G(X); \end{xple} This binding is represented in the abstract syntax as a parallel binding of two type variables ($X$ and $Y$) to two \e{independent} recursive types that both describe the full recursive equation system: \[ \tllettype{X}{\tlRectwo{X_1}{X_1<:\tlOk=F(X_2), X_2<:\tlOk=G(X_1)}} \] and \[ \tllettype{Y}{\tlRectwo{X_2}{X_1<:\tlOk=F(X_2), X_2<:\tlOk=G(X_1)}} \] This representation proved to be advantageous for the definition of the scoping and typing rules and the implementation of the relevant checking algorithms. The bound specifications in recursive type bindings ($<:$\k{Ok} in the example above) are required to simplify the checking of type operator applications within the recursive binding, for example \begin{xple} \k{Let Rec} A1 = A2(A2) \k{and} A2 = A3(A3) \k{and} \ldots \k{and} An = \k{Oper}(X(Y $<$:\k{Ok}) $<$:\k{Ok}) X(Int) \end{xple} has to be written as \begin{xple} \k{Let} Unary = \k{Oper}(X(Y $<$:\k{Ok}) $<$:\k{Ok}) \k{Ok} \k{Let} A1 $<$:Unary = A2(A2) \k{and} A2 $<$:Unary = A3(A3) \k{and} \ldots \k{and} An $<$:Unary = \k{Oper}(X(Y $<$:\k{Ok}) $<$:\k{Ok}) X(Int) \end{xple} The \k{var} attribute of value bindings and signatures and the \k{Dyn} attribute of type bindings and signatures are both mapped to explicit type constructors. This implies that types like \tlVar{\tlVar{A}} do not appear in \TL\ programs. Finally, it should be noted that entities of the value level enter the type level via qualifiers for abstract data types. The syntax for qualifiers is restricted and just allows simple path expressions involving value variables. \subsection{Values} \begin{table} %\begin{maxipage} \begin{center} \begin{tabular}{rll} $a,b::=$& \k{ok} & the canonical value of type $\tlOk$\\ $|$ & \p{int} & integer literals (s.~\refpar{Sec:TL-Symbols})\\ $|$ & \p{real} & floating point literals (s.~\refpar{Sec:TL-Symbols})\\ $|$ & \p{longreal} & double precision floating point literals (s.~\refpar{Sec:TL-Symbols})\\ $|$ & \p{char} & character literals (s.~\refpar{Sec:TL-Symbols}) \\ $|$ & \p{string} & string literals (s.~\refpar{Sec:TL-Symbols}) \\ $|$ & $x$ & value identifier\\ $|$ & $\k{fun}(S) a$ & (polymorphic) function constructor\\ $|$ & $a(D)$ & function application\\ $|$ & $\k{arr}(D)$ & array constructor\\ $|$ & $a[b]$ & array element selection\\ $|$ & $\k{tup}(D, z, D')$ & tuple constructor (with variants)\\ $|$ & $\k{rcd}(D)$ & record constructor \\ $|$ & $a.x$ & tuple, record and execption field selection\\ $|$ & $a!z$ & variant projection\\ $|$ & $a?z$ & variant test\\ $|$ & $\k{extend}(a,D)$ & record extension\\ $|$ & $\k{exc}(a,D)$ & exception value generation\\ $|$ & $\k{seq}(D)$ & sequential evaluation\\ $|$ & $\k{if}(a,b_1,b_2)$ & conditional\\ $|$ & $\k{case}(a,$ & variant analysis ($0\leq n, 1\leq k_i$)\\ & $\medspc (z_{11} \ldots z_{1k_1}, y_1, b_1) \ldots$ & \\ & $\medspc (z_{n1} \ldots z_{nk_n}, y_n, b_n),b)$ & \\ $|$ & $\k{case}(a,$ & exhaustive variant analysis\\ & $\medspc (z_{11} \ldots z_{1k_1}, y_1, b_1) \ldots$ & ($1\leq n, 1\leq k_i$)\\ & $\medspc (z_{n1} \ldots z_{nk_n}, y_n, b_n))$ & \\ $|$ & $\k{typecase}(A,$ & dynamic type test ($0\leq n$)\\ & $\medspc (B_1, b_1) \ldots (B_n, b_n),b')$ & \\ $|$ & $\k{loop}(a_1)$ & loop\\ $|$ & $\k{exit}$ & loop exit\\ $|$ & $\k{while}(a,b)$ & pre-check loop\\ $|$ & $\k{for}(x,a_1,a_2,a_3)$ & integer iteration\\ $|$ & $\k{try}(a,$ & exception handling ($0\leq n$)\\ & $(a_1,y_1,b_1) \ldots (a_n,y_n,b_n),b)$ & \\ $|$ & $\k{raise}(a,D)$ & exception generation\\ $|$ & $\k{reraise}$ & exception propagation\\ $|$ & $\k{andif}(a,b)$ & conditional conjunction\\ $|$ & $\k{orif}(a,b)$ & conditional disjunction\\ $;$ & & \\ \end{tabular} \end{center} \caption{Abstract syntax for values} \label{Table:TL-Values} %\end{maxipage} \end{table} Table~\ref{Table:TL-Values} summarizes the inductive definition of values in \TL. The syntax is quite standard and therefore does not require further explanation. The syntax does not contain an assignment operator since assignments are provided by a polymorphic function in the programming environment with the following signature:\footnote{Different implementations of the assignment function may attach recovery or concurrency control functionality to the plain destructive update operator.} \begin{xple} := (A $<:$\k{Ok} \k{var} lhs :A rhs :A) \end{xple} There are two multi-branch case expressions. The type rules for one version requires an exhaustive enumeration of all possible variant values, while the other is equipped with a non-empty \k{else} branch. \newpage \section{The Static Semantics of \TL} \thispagestyle{plain} \label{Sec:Static-Semantics} A medium-term goal in the Tycoon project is to provide a formal definition of \e{all} static and dynamic aspects of the language. For the purpose of this preliminary language definition, only the static semantics of \TL\ have been captured formally (omitting modules, libraries, object locality, the enforcement of the proper nesting of exit statements in loops, and the inference rules for type arguments in function applications). The dynamic semantics of \TL\ are implicitly defined by a mapping of \TL\ terms to untyped terms of the underlying untyped Tycoon machine language \TML. The evaluation semantics of \TML\ in turn are defined w.r.t. the abstract operational semantics of the Tycoon store protocol \TSP. \subsection{Overview over the Type Notations} The following notations are used for the definition of the static semantics of \TL: \begin{center} \begin{tabular}{|l|l|l|} \hline $\tlcontractive{A}{X}$& The type $A$ is contractive in variable $X$ & \refpar{Sec:TL-Contractive} \\ $\tlissig{S} $ & The signatures $S$ are well-formed & \refpar{Sec:TL-Signatures}\\ $\tlisrcdsig{S} $ & The signatures $S$ are well-formed record signatures & \refpar{Sec:TL-Signatures} \\ $\tlistype{A} $ & The type $A$ is well-formed & \refpar{Sec:TL-Types} \\ $\tlsigtype{A}{S} $ & The type $A$ has signatures $S$ & \refpar{Sec:TL-Selectors} \\ $\tlselector{p}{S} $ & The selector $p$ identifies a value with signatures $S$ & \refpar{Sec:TL-Selectors} \\ $\tlsubsig{S}{S'} $ & $S$ are subsignatures of $S'$ & \refpar{Sec:TL-Subsignatures} \\ $\tltupsubsig{S}{S'} $& $S$ are tuple subsignatures of $S'$ & \refpar{Sec:TL-Subsignatures} \\ $\tlrcdsubsig{S}{S'} $& $S$ are record subsignatures of $S'$ & \refpar{Sec:TL-Subsignatures} \\ $\tlsubtype{A}{B} $ & $A$ is a subtype of $B$ & \refpar{Sec:TL-Subtypes} \\ $\tlhassig{D}{S} $ & The bindings $D$ have signatures $S$ & \refpar{Sec:TL-Bindings} \\ $\tlhastype{a}{A} $ & The value $a$ has type $A$ & \refpar{Sec:TL-Values} \\ \hline \end{tabular} \end{center} The last column indicates the section that contains the definition of each judgement. Note that virtually all definitions are mutually recursive and closely follow the structure of the inductive definition of the underlying syntactic objects given in the previous section. The order-preserving concatenation of signatures and bindings is denoted as follows: \begin{center} \begin{tabular}{ll} $\tlconssig{S}{S'}$ & the signatures in $S$ followed by signatures in $S'$ \\ $\tlconsbnd{D}{D'}$ & the bindings in $D$ followed by bindings in $D'$ \end{tabular} \end{center} Despite the fact that signatures are ordered sequences, the following notation treats them like finite mappings from value names to types resp.\ type names to type bounds: \begin{center} \begin{tabular}{ll} $x\in \mapdomain{S}$ & the value variable $x$ is defined in $S$ \\ $X\in \mapdomain{S}$ & the type variable $X$ is defined in $S$ \end{tabular} \end{center} The type rules of \TL\ are presented as a system of axioms and deduction rules where the judgements in the premises and consequences in general refer to a \e{static environment}. The environment itself is represented as an ordered list $S$ of signatures: \begin{center} \begin{tabular}{ll} $\judge{S}{J}$ & in the static environment $S$ the judgement $J$ is true \end{tabular} \end{center} \subsection{Substitutions} The type rules for the instantiation of polymorphic function \refdef{Value apply} in \refpar{Keyword:Value-Apply} and of type operators \refdef{Type apply} in \refpar{Keyword:Type-Apply} use the following notation to denote the variable capture avoiding \e{substitution} of free type variables in a type expression by an actual type parameter: \begin{center} \begin{tabular}{ll} $\tlsubsttype{A}{X}{B}$ & $A$ where each free occurence of $X$ is substituted by $B$ \end{tabular} \end{center} This substitution operation could be made more explicit by replacing the applied occurence of a variable name by the (relative) index of its defining occurence witin the static environment and thereby reducing the substitution operation to a mere index manipulation \cite{deBr72,ACCL90}\footnote{This is also the mechanism used in the \TL\ type checker.}. A sequence of bindings $D$ passed as actual parameters to a polymorphic function or a type operator defines an \e{iterated substitution} of the type variables $X$ defined in $D$ by their associated type expressions: \begin{center} \begin{tabular}{ll} $\tlsubstbind{A}{D}$ & $A$ where all $X,x\in\mapdomain{D}$ are substituted as follows \end{tabular} \end{center} \define{Subst empty}{ \axiom{ \judge{S}{\tlsubstbind{A}{\tlemptybnd} = A} }} % \define{Subst Ide}{ \dedtwoh{ \judge{S}{\tlhassig{D}{S'}} } { \judge{\tlconssig{S}{S'}}{\tlhassig{D'}{\tlsubtype{X}{B}}} } { \judge{S}{\tlsubstbind{A}{\tlconsbnd{D}{D'}} = \tlsubsttype{\tlsubstbind{A}{D}}{X}{B}} }} \define{Subst Let}{ \dedtwoh{ \judge{S}{\tlhassig{D}{S'}} } { \judge{\tlconssig{S}{S'}}{\tlhassig{D'}{\tllettype{X}{B}}} } { \judge{S}{\tlsubstbind{A}{\tlconsbnd{D}{D'}} = \tlsubsttype{\tlsubstbind{A}{D}}{X}{B}} }} % \define{Subst ide}{ \dedtwoh{ \judge{S}{\tlhassig{D}{S'}} } { \judge{\tlconssig{S}{S'}}{\tlhassig{D'}{\tlhastype{x}{B}}} } { \judge{S}{\tlsubstbind{A}{\tlconsbnd{D}{D'}} = \tlsubstbind{A}{D}} }} \subsection{Qualified Type Variables} The access to the type information associated with individual type or value components in a tuple or a record \refdef{Subtype Dot} \refdef{Value tuple dot} \refdef{Value record dot} requires the qualification of type variables by a path that identifies the enclosing tuple or record value to avoid name conflicts with type variables in the global scope and to achieve the type abstraction implied by packaged type components. \begin{center} \begin{tabular}{ll} $\tlqualify{T}{p}{S}$ & substitute in $T$ each occurence of $X\in\mapdomain{S}$ by $p.X$ \end{tabular} \end{center} where $T\in \p{Sig}\cup \p{Type}$. This qualification is defined inductively as follows: \[ \tlqualify{T}{p}{\tlemptysig} = T \] \[ \tlqualify{T}{p}{\tlconssig{S}{\tlhastype{x}{B}}} = \tlqualify{\tlsubsttype{T}{x}{p.x}}{p}{S} \] \[ \tlqualify{T}{p}{\tlconssig{S}{\tlsubtype{X}{B}}} = \tlqualify{\tlsubsttype{T}{X}{p.X}}{p}{S} \] \[ \tlqualify{T}{p}{\tlconssig{S}{\tllettype{X}{B}}} = \tlqualify{\tlsubsttype{T}{X}{p.X}}{p}{S} \] \subsection{Contractive Types} \label{Sec:TL-Contractive} A final auxiliary notation is required in rule \refdef{Type Rec} in \refpar{Keyword:Type-Rec} to restrict the structure of recursive types to \e{contractive} type expressions. \begin{center} \begin{tabular}{ll} $\judge{S}{\tlcontractive{A}{X}}$ & In environment $S$ type $A$ is contractive in variable $X$ \end{tabular} \end{center} Systems of recursive type equations $\tlRec{X_i}{X}{A}{B}{n}$ that are contractive in their recursion variable $X_i$ define well-formed \e{regular trees}, the basis for semantic models of type structures \cite{MPS86} as well as termination proofs for type checking algorithms \cite{Ohor89}. The following judgements are independent of the identifiers occuring in the the static environment: \[\tlcontractive{Y}{X} \Leftrightarrow Y \not= X \] \[\tlcontractive{\tlOk}{X} \bigspc \tlcontractive{\tlNok}{X} \bigspc \tlcontractive{\tlBool}{X} \bigspc \tlcontractive{\tlInt}{X} \bigspc \tlcontractive{\tlString}{X} \] \[\tlcontractive{\tlDot{x}{Y}}{X} \bigspc \tlcontractive{\tlFun{S'}{B}}{X} \bigspc \tlcontractive{\tlTup{S'}{C}}{X} \bigspc \tlcontractive{\tlRcd{S'}}{X} \bigspc \tlcontractive{\tlExc{S'}}{X} \bigspc \tlcontractive{\tlArr{A}}{X} \] \[\tlcontractive{\tlVar{A}}{X} \Leftrightarrow \tlcontractive{A}{X} \] \[\tlcontractive{\tlDyn{A}}{X} \Leftrightarrow \tlcontractive{A}{X} \] The last three judgements refer to the static environment $S$: \define{Contractive Oper}{\ded{ \judge{\tlconssig{S}{S'}}{\tlcontractive{B}{X}} } { \judge{S}{\tlcontractive{\tlOper{S'}{B}}{X}} }} \define{Contractive Rec}{\ded{ \judge{S}{\tlistype{\tlRec{X_i}{X}{A}{B}{n}}} } { \judge{S}{\tlcontractive{\tlRec{X}{X}{A}{B}{n}}{Y}} }} \define{Contractive Apply}{\dedthreeh{ \judge{S}{\tlsubtype{A}{\tlOper{S'}{B}}} } { \judge{S}{\tlhassig{D}{S'}} } { \judge{S}{\tlcontractive{\tlsubstbind{B}{D}}{X}} } { \judge{S}{\tlcontractive{\tlApply{A}{D}}{X}} }} The above definition is well-founded although rule \refdef{Contractive Rec} itself requires the definition of well-founded types, since the syntax of \TL\ does not allow statically nested recursive type declarations. {\setlength{\parindent}{0pt} \raggedright \subsection{Well-formed Signatures} \label{Sec:TL-Signatures} \define{Sig empty}{ \axiom{\judge{}{\tlissig{\tlemptysig}}} } % \define{Sig ide}{ \ded{ \judge{S}{\tlistype{A}} } { \judge{}{\tlissig{\tlconssig{S}{\tlhastype{x}{A}}}} }} % \define{Sig Ide}{ \ded{ \judge{S}{\tlistype{A}} } { \judge{}{\tlissig{\tlconssig{S}{\tlsubtype{X}{A}}}} }} % \define{Sig Ide Let}{ \ded{ \judge{S}{\tlistype{A}} } { \judge{}{\tlissig{\tlconssig{S}{\tllettype{X}{A}}}} }} % \define{Sig Repeat}{ \dedtwoh{ \judge{S}{\tlsigtype{A}{S'}} } { \judge{}{\tlissig{S'}} } { \judge{}{\tlissig{\tlconssig{S}{\tlRepeat{A}}}} }} % \define{Rcdsig}{ \dedtwoh{ \judge{}{\tlissig{\tlconssig{S}{S'}}} } { (S'=\tlconssig{S_1}{S_2} \wedge X \in \mapdomain{S_1} \Rightarrow X\not\in \mapdomain{S_2}) } { \judge{S}{\tlisrcdsig{S'}} }} \subsection{Well-formed Types} \label{Sec:TL-Types} \define{Type Builtin}{ \dedtwoh{ \judge{}{\tlissig{S}} } { A \in \{ \tlOk, \tlNok, \tlBool, \tlInt, \tlString \} } { \judge{S}{\tlistype{A}} }} % \define{Type Ide}{ \ded{ \judge{}{\tlissig{\tlconstwosig{S}{\tlsubtype{X}{A}}{S'}}} \bigspc X \not\in \mapdomain{S'} } { \judge{\tlconstwosig{S}{\tlsubtype{X}{A}}{S'}}{\tlistype{X}} }} \define{Type Ide Let}{ \ded{ \judge{}{\tlissig{\tlconstwosig{S}{\tlsubtype{X}{A}}{S'}}} \bigspc X \not\in \mapdomain{S'} } { \judge{\tlconstwosig{S}{\tllettype{X}{A}}{S'}}{\tlistype{X}} }} % \define{Type Dot}{ \dedthreeh{ \judge{S}{\tlselector{p}{S'}} } { \judge{\tlconssig{S}{S'}}{\tlistype{X}} } { X \in \mapdomain{S'} } { \judge{S}{\tlistype{\tlDot{p}{X}}} }} % \define{Type Fun}{ \dedtwoh{ \judge{}{\tlissig{\tlconssig{S}{S'}}} } { \judge{\tlconssig{S}{S'}}{\tlsubtype{B}{\tlOk}} } { \judge{S}{\tlistype{\tlFun{S'}{B}}} }} % \define{Type Tup}{ \dedthreeh{ 1 \leq n \bigspc z_i \not= z_j \medspc i \not= j } { \judge{}{\tlissig{\tlconssig{S}{S'}}} } { \judge{}{\tlissig{\tlconstwosig{S}{S'}{S_i}}} \bigspc i = 1 \ldots n } { \judge{S}{\tlistype{\tlTup{S'}{\tlCase{z_1}{S_1} \ldots \tlCase{z_n}{S_n}}}} }} \define{Type Rcd}{ \ded{ \judge{S}{\tlisrcdsig{S'}} } { \judge{S}{\tlistype{\tlRcd{S'}}} }} % \define{Type Exc}{ \ded{ \judge{}{\tlissig{\tlconssig{S}{S'}}} } { \judge{S}{\tlistype{\tlExc{S'}}} }} % \define{Type Rec}{ \dedtwo{ \judge{\tlconssig{S}{\tlsubtype{X_1}{A_1}, \ldots, \tlsubtype{X_n}{A_n}}} {\tlsubtype{B_i}{A_i}} \bigspc i = 1 \ldots n \bigspc \bigspc 1 \leq j \leq n } { \judge{\tlconssig{S}{\tllettype{X_1}{B_1}, \ldots, \tllettype{X_n}{B_n}}} {\tlcontractive{B_i}{X_i}} \bigspc i = 1 \ldots n } { \judge{S}{\tlistype{\tlRec{X_j}{X}{A}{B}{n}}} }}\label{Keyword:Type-Rec} % \define{Type Var}{ \ded{ \judge{S}{\tlsubtype{A}{\tlOk}} } { \judge{S}{\tlistype{\tlVar{A}}} }} % \define{Type Dyn}{ \ded{ \judge{S}{\tlistype{A}} } { \judge{S}{\tlistype{\tlDyn{A}}} }} % \define{Type Arr}{ \ded{ \judge{S}{\tlsubtype{A}{\tlOk}} } { \judge{S}{\tlistype{\tlArr{A}}} }} % \define{Type Oper}{ \dedtwoh{ \judge{}{\tlissig{\tlconssig{S}{S'}}} } { \judge{\tlconssig{S}{S'}}{\tlistype{B}} } { \judge{S}{\tlistype{\tlOper{S'}{B}}} }} % \define{Type Apply}{ \dedtwoh{ \judge{S}{\tlsubtype{A}{\tlOper{S'}{B}}} } { \judge{S}{\tlhassig{D}{S'}} } { \judge{S}{\tlistype{\tlApply{A}{D}}} }}\label{Keyword:Type-Apply} \subsection{Signatures of Types and Values} \label{Sec:TL-Selectors} \define{Select ide}{ \dedtwoh{ \judge{S}{\tlhastype{x}{A}} } { \judge{S}{\tlsigtype{A}{S'}} } { \judge{S}{\tlselector{x}{S'}} }} % \define{Select dot}{ \dedthreeh{ \judge{S}{\tlselector{p}{S'}} } { x \in\mapdomain{S'} } { \judge{\tlconssig{S}{S'}}{\tlselector{x}{S''}} } { \judge{S}{\tlselector{\tlDot{p}{x}}{S''}} }} \define{Select Tup}{ \ded{ \judge{S}{\tlhastype{A}{\tlTup{S'}{C}}} } { \judge{S}{\tlsigtype{A}{S'}} }} % \define{Select Rcd}{ \ded{ \judge{S}{\tlhastype{A}{\tlRcd{S'}}} } { \judge{S}{\tlsigtype{A}{S'}} }} % \define{Select Exc}{ \ded{ \judge{S}{\tlhastype{A}{\tlExc{S'}}} } { \judge{S}{\tlsigtype{A}{S'}} }} \define{Select Fun}{ \ded{ \judge{S}{\tlhastype{A}{\tlFun{S'}{B}}} } { \judge{S}{\tlsigtype{A}{S'}} }} % \define{Select Oper}{ \ded{ \judge{S}{\tlhastype{A}{\tlOper{S'}{B}}} } { \judge{S}{\tlsigtype{A}{S'}} }} \subsection{Subsignatures} \label{Sec:TL-Subsignatures} \define{Subsig reflexive}{ \ded{ \judge{}{\tlissig{\tlconssig{S}{S'}}} } { \judge{S}{\tlsubsig{S'}{S'}} }} % \define{Subsig ide}{ \dedtwoh{ \judge{S}{\tlsubsig{S'}{S''}} } { \judge{\tlconssig{S}{S'}}{\tlsubtype{A}{B}} } { \judge{S}{\tlsubsig{\tlconssig{S'}{\tlhastype{x}{A}}} {\tlconssig{S''}{\tlhastype{x}{B}}}} }} % \define{Subsig Ide}{ \dedtwoh{ \judge{S}{\tlsubsig{S'}{S''}} } { \judge{\tlconssig{S}{S'}}{\tlsubtype{A}{B}} } { \judge{S}{\tlsubsig{\tlconssig{S'}{\tlsubtype{X}{A}}} {\tlconssig{S''}{\tlsubtype{X}{B}}}} }} % \define{Subsig Ide Let}{ \dedtwoh{ \judge{S}{\tlsubsig{S'}{S''}} } { \judge{\tlconssig{S}{S'}}{\tlsubtype{A}{B}} } { \judge{S}{\tlsubsig{\tlconssig{S'}{\tllettype{X}{A}}} {\tlconssig{S''}{\tlsubtype{X}{B}}}} }} % \define{Subsig Repeat}{ \dedtwoh{ \judge{S}{\tlsubsig{S'}{S''}} } { \judge{\tlconssig{S}{S'}}{\tlsigtype{A}{S'''}} } { \judge{S}{\tlsubsig{\tlconssig{S'}{\tlRepeat{A}}} {\tlconssig{S''}{S'''} }}}} % \define{Subsig Tup}{ \dedtwoh{ \judge{}{\tlissig{\tlconstwosig{S}{S_1}{S_2}}} } { \judge{S}{\tlsubsig{S_1}{S_1'}} } { \judge{S}{\tltupsubsig{\tlconssig{S_1}{S_2}}{S_1'}} }} % \label{Keyword:Subsig-Rcd} \define{Subsig Rcd}{ \dedthreeh{ \judge{S}{\tlisrcdsig{\tlconstwosig{S_1}{S_2}{S_3}}} } { \judge{S}{\tlrcdsubsig{\tlconssig{S_1}{S_3}}{S'_1}} } { \judge{\tlconssig{S}{S'_1}}{\tltupsubsig{S_2}{S'_2}} } { \judge{S}{\tlrcdsubsig{\tlconstwosig{S_1}{S_2}{S_3}}{\tlconssig{S'_1}{S'_2}}} }} \subsection{Subtypes} \label{Sec:TL-Subtypes} \define{Subtype reflexive}{ \ded{ \judge{S}{\tlistype{A}} } { \judge{S}{\tlsubtype{A}{A}} }} % \define{Subtype transitive}{ \dedtwoh{ \judge{S}{\tlsubtype{A}{A'}} } { \judge{S}{\tlsubtype{A'}{A''}} } { \judge{S}{\tlsubtype{A}{A''}} }} % \define{Subtype Nok}{ \ded{ \judge{S}{\tlsubtype{A}{\tlOk}} } { \judge{S}{\tlsubtype{\tlNok}{A}} }} % % \define{Subtype Ok Builtin}{ \dedtwoh{ \judge{}{\tlissig{S}} } { A \in \{ \tlBool, \tlInt, \tlString \} } { \judge{S}{\tlsubtype{A}{\tlOk}} }} % % Generic TeX Typing! \newcommand{\subtypeOk}[2]{\define{Subtype Ok #1}{ \ded{ \judge{S}{\tlistype{#2}} } { \judge{S}{\tlsubtype{#2}{\tlOk}} }}} % \subtypeOk{Fun}{\tlFun{S'}{B}} % \subtypeOk{Tup}{\tlTup{S'}{C}} % \subtypeOk{Rcd}{\tlRcd{S'}} % \subtypeOk{Exc}{\tlExc{S'}} % \subtypeOk{Arr}{\tlArr{A}} % \subtypeOk{Var}{\tlVar{A}} % \define{Subtype Ok Dyn}{ \ded{ \judge{S}{\tlsubtype{A}{\tlOk}} } { \judge{S}{\tlsubtype{\tlDyn{A}}{\tlOk}} }} \define{Subtype Ide}{ \dedtwoh{ \judge{}{\tlissig{\tlconstwosig{S}{\tlsubtype{X}{A}}{S'}}} } { X \not\in\mapdomain{S'} } { \judge{\tlconstwosig{S}{\tlsubtype{X}{A}}{S'}}{\tlsubtype{X}{A}} }} % \define{Subtype Ide Let}{ \dedtwoh{ \judge{}{\tlissig{\tlconstwosig{S}{\tlsubtype{X}{A}}{S'}}} } { X \not\in\mapdomain{S'} } { \judge{\tlconstwosig{S}{\tllettype{X}{A}}{S'}}{\tlsubtype{X}{A}} }} % \define{Subtype Ide Let2}{ \dedtwoh{ \judge{}{\tlissig{\tlconstwosig{S}{\tlsubtype{X}{A}}{S'}}} } { X \not\in\mapdomain{S'} } { \judge{\tlconstwosig{S}{\tllettype{X}{A}}{S'}}{\tlhastype{A}{X}} }} % \define{Subtype Dot}{ \dedtwoh{ \judge{S}{\tlselector{p}{\tlconstwosig{S'}{\tlsubtype{X}{A}}{S''}}} } { X \not\in\mapdomain{S''} } { \judge{S}{\tlsubtype{\tlDot{p}{X}}{\tlqualify{A}{p}{S'}}} }} % \define{Subtype Fun}{ \dedtwoh{ \judge{S}{\tlsubsig{S''}{S'}} } { \judge{\tlconssig{S}{S''}}{\tlsubtype{A}{B}} } { \judge{S}{\tlsubtype{\tlFun{S'}{A}}{\tlFun{S''}{B}}} }}\label{Keyword:Subtype-Fun} % \define{Subtype Arr}{ \ded{ \judge{S}{\tlsubtype{A}{B}} } { \judge{S}{\tlsubtype{\tlArr{A}}{\tlArr{B}}} }} % \define{Subtype Tup}{ \dedtwo{ \judge{S}{\tltupsubsig{\tlconssig{S_0}{S_i}}\tlconssig{S_0'}{S_i'}} \bigspc i = 1 \ldots n \bigspc 1 \leq n } { \judge{S}{\tlissig{\tlconssig{S_0'}{S_j''}}} \bigspc j = 1 \ldots m \bigspc 1 \leq m } { \begin{array}{ll} \judge{S}{} & \tlTup{S_0}{\tlCase{z_1}{S_1} \ldots \tlCase{z_n}{S_n}} \tlsubtype{}{} \\ & \tlTup{S_0'}{\tlCase{z_1}{S_1'} \ldots \tlCase{z_n}{S_n'}\, \tlCase{z_1'}{S_1''} \ldots \tlCase{z_m'}{S_m''}} \end{array} }} % \define{Subtype Rcd}{ \ded{ \judge{S}{\tlrcdsubsig{S'}{S''}} } { \judge{S}{\tlsubtype{\tlRcd{S'}}{\tlRcd{S''}}} }} % \define{Subtype Exc}{ \ded{ \judge{S}{\tltupsubsig{S'}{S''}} } { \judge{S}{\tlsubtype{\tlExc{S'}}{\tlExc{S''}}} }} % \define{Subtype Var}{ \ded{ \judge{S}{\tlistype{A}} } { \judge{S}{\tlsubtype{\tlVar{A}}{A}} }} % \define{Subtype Dyn Elim}{ \ded{ \judge{S}{\tlistype{A}} } { \judge{S}{\tlsubtype{\tlDyn{A}}{A}} }} % \define{Subtype Dyn}{ \ded{ \judge{S}{\tlsubtype{A}{B}} } { \judge{S}{\tlsubtype{\tlDyn{A}}{\tlDyn{B}}} }} % \define{Subtype Non-Rec Rec}{ \dedtwo{ A\not=\tlRectwo{Y}{D'} } { \judge{S}{\tlsubtype{A}{\tlsubstbind{B_j} {\tlconsbnd{\tlconsbnd{\tlbnd{X_1}{\tlRectwo{X_1}{D}}}{\ldots}} {\tlbnd{X_n}{\tlRectwo{X_n}{D}}}} }} } { \judge{S}{\tlsubtype{A}{\tlRec{X_j}{X}{A}{B}{n}}} }} % \define{Subtype Rec Non-Rec}{ \dedtwo{ A\not=\tlRectwo{Y}{D'} } { \judge{S}{\tlsubtype{\tlsubstbind{B_j} {\tlconsbnd{\tlconsbnd{\tlbnd{X_1}{\tlRectwo{X_1}{D}}}{\ldots}} {\tlbnd{X_n}{\tlRectwo{X_n}{D}}}}} {A}} } { \judge{S}{\tlsubtype{\tlRec{X_j}{X}{A}{B}{n}}{A}} }} % %\begin{maxipage} \define{Subtype Rec Rec}{ \dedtwoh{ \judge{S''}{\tlsubtype{A_i}{A'_j}} } { \judge{\tlconstwosig{S''}{S'}{S}}{\tlsubtype{B_i}{B'_j}} } { \judge{S''}{\tlsubtype{\tlRec{X_i}{X}{A}{B}{n}}{\tlRec{X'_j}{X'}{A'}{B'}{m}}} }} {\small where \begin{eqnarray*} S' & = & \tlsubtype{X'_1}{\tlRectwo{X'_1}{D'}}, \ldots \tlsubtype{X'_{j-1}}{\tlRectwo{X'_{j-1}}{D'}}, \tlsubtype{X'_j}{A'_j}, \\ & & \tlsubtype{X'_{j+1}}{\tlRectwo{X'_{j+1}}{D'}}, \ldots \tlsubtype{X'_{m}}{\tlRectwo{X'_{m}}{D'}} \\ S & = & \tlsubtype{X_1}{\tlRectwo{X_1}{D}}, \ldots \tlsubtype{X_{i-1}}{\tlRectwo{X_{i-1}}{D}}, \tlsubtype{X_i}{X'_j}, \\ & & \tlsubtype{X_{i+1}}{\tlRectwo{X_{i+1}}{D}}, \ldots \tlsubtype{X_{n}}{\tlRectwo{X_{n}}{D}} \\ D' & = & X'_1<:A'_1=B'_1, \ldots, X'_m<:A'_m=B'_m \\ D & = & X_1<:A_1=B_1, \ldots, X_n<:A_n=B_n \end{eqnarray*} } %\end{maxipage} % \define{Subtype Oper}{ \dedtwoh{ \judge{S}{\tlsubsig{S''}{S'}} } { \judge{\tlconssig{S}{S''}}{\tlsubtype{A}{B}} } { \judge{S}{\tlsubtype{\tlOper{S'}{A}}{\tlOper{S''}{B}}} }}\label{Keyword:Subtype-Oper} % \define{Subtype Apply}{ \dedtwoh{ \judge{S}{\tlsubtype{A}{\tlOper{S'}{B}}} } { \judge{S}{\tlhassig{D}{S'}} } { \judge{S}{\tlsubtype{A(D)}{\tlsubstbind{B}{D}}} }} \subsection{Signatures of Bindings} \label{Sec:TL-Bindings} \define{Bind empty}{ \ded{ \judge{}{\tlissig{S}} } { \judge{S}{\tlhassig{\tlemptybnd}{\tlemptysig}} }} % \define{Bind ide}{ \dedtwoh{ \judge{S}{\tlhassig{D}{S'}} } { \judge{\tlconssig{S}{S'}}{\tlhastype{a}{A}} } { \judge{S}{\tlhassig{\tlconsbnd{D}{\tlbnd{x}{a}}}{\tlconssig{S'}{\tlhastype{x}{A}}}} }} % \define{Bind ide restrict}{ \dedtwoh{ \judge{S}{\tlhassig{D}{S'}} } { \judge{\tlconssig{S}{S'}}{\tlhastype{a}{A}} } { \judge{S}{\tlhassig{\tlconsbnd{D}{\tlbndrestr{x}{A}{a}}}{\tlconssig{S'}{\tlhastype{x}{A}}}} }} % \define{Bind Ide}{ \dedtwoh{ \judge{S}{\tlhassig{D}{S'}} } { \judge{\tlconssig{S}{S'}}{\tlistype{A}} } { \judge{S}{\tlhassig{\tlconsbnd{D}{\tlbnd{X}{A}}}{\tlconssig{S'}{\tllettype{X}{A}}}} }} % \define{Bind Ide restrict}{ \dedtwoh{ \judge{S}{\tlhassig{D}{S'}} } { \judge{\tlconssig{S}{S'}}{\tlsubtype{B}{A}} } { \judge{S}{\tlhassig{\tlconsbnd{D}{\tlbndRestr{X}{A}{B}}}{\tlconssig{S'}{\tllettype{X}{B}}}} }} % \define{Bind and}{ \dedtwoh{ \judge{S}{\tlhassig{D}{S'}} } { \judge{\tlconssig{S}{S'}}{\tlhassig{E_i}{S_i}} \bigspc i = 1 \ldots n \bigspc 1 \leq n } { \judge{S}{\tlhassig{\tlconsbnd{D}{E_1 | \ldots | E_n}} {\tlconssig{S'}{\tlconstwosig{S_1}{\ldots}{S_n}}}} }} % \define{Bind rec}{ \dedtwoh{ \judge{S}{\tlhassig{D}{S'}} } { \judge{\tlconstwosig{S}{S'}{\tlconstwosig{x_1:A_1}{\ldots}{x_n:A_n}}} {\tlhastype{a_i}{A_i}} \bigspc i = 1 \ldots n \bigspc 1 \leq n } { \judge{S}{\tlhassig{\tlconsbnd{D}{{\bf rec}(x_1:A_1=a_1 | \ldots | x_n:A_n=a_n)}} {\tlconssig{S'}{\tlconstwosig{x_1:A_1}{\ldots}{x_n:A_n}}}} }} % \define{Bind open}{ \dedtwoh{ \judge{S}{\tlhassig{D}{S'}} } { \judge{\tlconssig{S}{S'}}{\tlselector{p}{S''}} } { \judge{S}{\tlhassig{\tlconsbnd{D}{{\bf open}(p)}} {\tlconssig{S'}{\tlqualify{S''}{p}{S''}}}} }} % \define{Bind open restrict}{ \dedfourh{ \judge{S}{\tlhassig{D}{S'}} } { \judge{\tlconssig{S}{S'}}{\tlselector{p}{S''}} } { \judge{S}{\tlsigtype{A}{S'''}} } { \judge{S}{\tlsubsig{S''}{S'''}} } { \judge{S}{\tlhassig{\tlconsbnd{D}{{\bf open}(p,A)}} {\tlconssig{S'}{\tlqualify{S'''}{p}{S''}}}} }} % \subsection{Types of Values} \label{Sec:TL-Values} \define{Value subsumption}{ \dedtwoh{ \judge{S}{\tlhastype{a}{A}} } { \judge{S}{\tlsubtype{A}{B}} } { \judge{S}{\tlhastype{a}{B}} }} % \define{Value ok}{ \ded{ \judge{}{\tlissig{S}} } { \judge{S}{\tlhastype{{\bf ok}}{\tlOk}} }} % \define{Value ide}{ \ded{ \judge{}{\tlissig{\tlconstwosig{S}{\tlhastype{x}{A}}{S'}}} \bigspc x \not\in \mapdomain{S'} } { \judge{\tlconstwosig{S}{\tlhastype{x}{A}}{S'}}{\tlhastype{x}{A}} }} \define{Value fun}{ \ded{ \judge{\tlconssig{S}{S'}}{\tlhastype{a}{A}} } { \judge{S}{\tlhastype{{\bf fun}(S') a}{\tlFun{S'}{A}}} }} % \define{Value apply}{ \dedtwoh{ \judge{S}{\tlhastype{a}{\tlFun{S'}{A}}} } { \judge{S}{\tlhassig{D}{S'}} } { \judge{S}{\tlhastype{a(D)}{\tlsubstbind{A}{D}}} }}\label{Keyword:Value-Apply} \define{Value array}{ \ded{ \judge{S}{\tlhassig{D}{\tlhastype{x_1}{A} \ldots \tlhastype{x_n}{A}}} \bigspc 1\leq n } { \judge{S}{\tlhastype{{\bf arr}(D)}{\tlArr{A}}} }} % \define{Value array empty}{ \ded{ \judge{}{\tlissig{S}} } { \judge{S}{\tlhastype{{\bf arr}()}{\tlArr{\tlNok}}} }}\label{Keyword:Array-Empty} % \define{Value index}{ \dedtwoh{ \judge{S}{\tlhastype{a}{\tlArr{A}}} } { \judge{S}{\tlhastype{b}{\tlInt}} } { \judge{S}{\tlhastype{a[b]}{A}} }} % \define{Value tuple}{ \ded{ \judge{S}{\tlhassig{D}{S'}} } { \judge{S}{\tlhastype{{\bf tup}(D)}{\tlTup{S'}{\tlemptyCase}}} }} % \define{Value tuple variant}{ \dedthreeh{ \judge{S}{\tlhastype{A}{\tlTup{S'} {\tlCase{z_1}{S_1} \ldots \tlCase{z_n}{S_n}}}} } { \judge{S}{\tlhassig{D}{\tlconssig{S'}{S_i}}} } { 1 \leq z_i \leq n } { \judge{S}{\tlhastype{{\bf tup}(D; z_i; A))}{A}} }} % \define{Value tuple dot}{ \dedtwoh{ \judge{S}{\tlhastype{a}{\tlTup{ \tlconstwosig{S'}{\tlhastype{x}{A}}{S''} }{C}}} } { x \not\in\mapdomain{S''} } { \judge{S}{\tlhastype{a.x}{\tlqualify{A}{a}{S'}}} }}\label{Keyword:Value-Tuple-Dot} % \define{Value variant project}{ \ded{ \judge{S}{\tlhastype{x}{\tlTup{S'}{ \tlCase{z_1}{S_1} \ldots \tlCase{z_n}{S_n} }}} } { \judge{S}{\tlhastype{x!z_i}{\tlTup{\tlconssig{S'}{S_i}}{\tlemptyCase}}} }} % \define{Value variant test}{ \ded{ \judge{S}{\tlhastype{x}{\tlTup{S'}{ \tlCase{z_1}{S_1} \ldots \tlCase{z_n}{S_n} }}} } { \judge{S}{\tlhastype{x?z_i}{\tlBool}} }} % \define{Value record}{ \dedtwoh{ \judge{S}{\tlhassig{D}{S'}} } { \judge{S}{\tlisrcdsig{S'}} } { \judge{S}{\tlhastype{{\bf rcd}(D)}{\tlRcd{S'}}} }} % \define{Value record dot}{ \ded{ \judge{S}{\tlhastype{a}{\tlRcd{ \tlconstwosig{S'}{\tlhastype{x}{A}}{S''} }}} } { \judge{S}{\tlhastype{a.x}{\tlqualify{A}{a}{S'}}} }} % \define{Value extend}{ \dedthreeh{ \judge{S}{\tlhastype{a}{\tlRcd{S'}}} } { \judge{\tlconssig{S}{S'}}{\tlhassig{D}{S''}} } { \judge{S}{\tlisrcdsig{\tlconssig{S'}{S''}}} } { \judge{S}{\tlhastype{{\bf extend}(a, D)}{\tlRcd{\tlconssig{S'}{S''}}}} }} % \define{Value exception}{ \dedtwoh{ \judge{S}{\tlhastype{a}{\tlString}} } { \judge{S}{\tlhassig{D}{S'}} } { \judge{S}{\tlhastype{{\bf exc}(a,D)}{\tlExc{S'}}} }} % \define{Value seq empty}{ \ded{ \judge{}{\tlissig{S}} } { \judge{S}{\tlhastype{{\bf seq}(\tlemptybnd)}{\tlOk}} }} % \define{Value seq ide}{ \dedtwoh{ \judge{S}{\tlhassig{D}{S'}} } { \judge{\tlconssig{S}{S'}}{\tlhastype{a}{A}} } { \judge{S}{\tlhastype{{\bf seq}(\tlconsbnd{D}{\tlbnd{x}{a}})}{A}} }} % \define{Value seq ide restrict}{ \dedtwoh{ \judge{S}{\tlhassig{D}{S'}} } { \judge{\tlconssig{S}{S'}}{\tlhastype{a}{A}} } { \judge{S}{\tlhastype{{\bf seq}(\tlconsbnd{D}{\tlbndrestr{x}{A}{a}})}{A}} }} % \define{Value seq Ide}{ \dedtwoh{ \judge{S}{\tlhassig{D}{S'}} } { \judge{\tlconssig{S}{S'}}{\tlistype{A}} } { \judge{S}{\tlhastype{{\bf seq}(\tlconsbnd{D}{\tlbnd{X}{A}})}{\tlOk}} }} % \define{Value seq Ide restrict}{ \dedtwoh{ \judge{S}{\tlhassig{D}{S'}} } { \judge{\tlconssig{S}{S'}}{\tlsubtype{B}{A}} } { \judge{S}{\tlhastype{{\bf seq}(\tlconsbnd{D}{\tlbndRestr{X}{A}{B}})}{\tlOk}} }} % \define{Value if}{ \dedthreeh{ \judge{S}{\tlhastype{a}{\tlBool}} } { \judge{S}{\tlhastype{b}{B}} } { \judge{S}{\tlhastype{b'}{B}} } { \judge{S}{\tlhastype{{\bf if}(a,b,b')}{B}} }} % \define{Value case}{ \dedfive{ \judge{S}{\tlhastype{a}{\tlTup{S'}{ \tlCase{z'_1}{S_1} \ldots \tlCase{z'_m}{S_m} }}} } { \judge{S}{\tlhastype{b}{B}} } { \judge{\tlconssig{S}{\tlhastype{y_i}{\tlTup{\tlconssig{S'}{S''}}{\tlemptyCase}}}} {\tlhastype{b_i}{B}} \bigspc 0 \leq n \bigspc i = 1 \ldots n } { \judge{\tlconssig{S}{S'}}{\tlsubsig{S''}{S_{z_{ij}}}} \bigspc j = 1 \ldots k_{i} } { \bigcup_{i=1}^{n} \bigcup_{j=1}^{k_i} z_{ij} \subseteq \bigcup_{l=1}^{m} z'_l \bigspc z_{ij} \not= z_{i'j'} \medspc i\not=i', j\not=j' } { \judge{S}{\tlhastype{{\bf case}(a, (z_{11} \ldots z_{1k_1}, y_1, b_1) \ldots (z_{n1} \ldots z_{nk_n}, y_n, b_n) ,b)}{B}} }} % \define{Value case exhaustive}{ \dedfour{ \judge{S}{\tlhastype{a}{\tlTup{S'}{ \tlCase{z'_1}{S_1} \ldots \tlCase{z'_m}{S_m} }}} } { \judge{\tlconssig{S}{\tlhastype{y_i}{\tlTup{\tlconssig{S'}{S''}}{\tlemptyCase}}}} {\tlhastype{b_i}{B}} \bigspc 1 \leq n \bigspc i = 1 \ldots n } { \judge{\tlconssig{S}{S'}}{\tlsubsig{S''}{S_{z_{ij}}}} \bigspc j = 1 \ldots k_{i} } { \bigcup_{i=1}^{n} \bigcup_{j=1}^{k_i} z_{ij} = \bigcup_{l=1}^{m} z'_l \bigspc z_{ij} \not= z_{i'j'} \medspc i\not=i', j\not=j' } { \judge{S}{\tlhastype{{\bf case}(a, (z_{11} \ldots z_{1k_1}, y_1, b_1) \ldots (z_{n1} \ldots z_{nk_n}, y_n, b_n) )}{B}} }} % \define{Value typecase}{ \dedfour{ \judge{S}{\tlsubtype{X}{\tlDyn{\tlOk}}} } { \judge{S}{\tlhastype{b}{B}} } { \judge{S}{\tlsubtype{B_i}{X}} \bigspc i = 1 \ldots n \bigspc 0 \leq n } { \judge{\tlconssig{S}{\tlsubtype{X}{\tlDyn{B_i}}}} {\tlhastype{b_i}{B}} \bigspc i = 1 \ldots n } { \judge{S}{\tlhastype{{\bf typecase}(X, (B_1, b_1) \ldots (B_n, b_n) ,b)}{B}} }} % \define{Value loop}{ \ded{ \judge{S}{\tlhastype{a}{\tlOk}} } { \judge{S}{\tlhastype{{\bf loop}(a)}{\tlOk}} }} % \define{Value exit}{ \ded{ \judge{}{\tlissig{S}} } { \judge{S}{\tlhastype{{\bf exit}}{\tlNok}} }} % \define{Value while}{ \dedtwoh{ \judge{S}{\tlhastype{a}{\tlBool}} } { \judge{S}{\tlhastype{b}{\tlOk}} } { \judge{S}{\tlhastype{{\bf while}(a,b)}{\tlOk}} }} % \define{Value for}{ \dedthreeh{ \judge{S}{\tlhastype{a}{\tlInt}} } { \judge{S}{\tlhastype{b}{\tlInt}} } { \judge{\tlconssig{S}{\tlhastype{x}{\tlInt}}}{\tlhastype{c}{\tlOk}} } { \judge{S}{\tlhastype{{\bf for}(x,a,b,c)}{\tlOk}} }} % \define{Value try}{ \dedfour{ \judge{S}{\tlhastype{a}{B}} } { \judge{S}{\tlhastype{b}{B}} } { \judge{S}{\tlhastype{a_i}{\tlExc{S_i}}} \bigspc i = 1 \ldots n \bigspc 0 \leq n } { \judge{\tlconssig{S}{\tlhastype{x_i}{\tlTup{S_i}{\tlemptyCase}}}} {\tlhastype{b_i}{B}} \bigspc i = 1 \ldots n } { \judge{S}{\tlhastype{{\bf try}(a, (a_1,x_1,b_1) \ldots (a_n,x_n,b_n) ,b)}{B}} }} \define{Value raise}{ \dedtwoh{ \judge{S}{\tlhastype{a}{\tlExc{S'}}} } { \judge{S}{\tlhassig{D}{S'}} } { \judge{S}{\tlhastype{{\bf raise}(a,D)}{\tlNok}} }} % \define{Value reraise}{ \ded{ \judge{}{\tlissig{S}} } { \judge{S}{\tlhastype{{\bf reraise}}{\tlNok}} }} } % raggedright ... \subsection{Restrictions} The rule \refdef{Subtype Var} is not applicable in function signatures since the implementation of variable parameters (l-value bindings) is incompatible with the implementation of value parameters (r-value bindings). This restriction is checked statically. \bibliographystyle{enamed} \bibliography{../bib/florian} \end{document}