Bericht Nr. 160

Definition of the Tycoon Language Tl

A Preliminary Report

Florian Matthes  Joachim W. Schmidt

FBI-HH-B-160/92

Dezember 1992 (revidiert August 1995)

Fachbereich Informatik Universität Hamburg Vogt-Kölln-Str. 30

D-W-200 Hamburg 54 Federal Republic of Germany

Abstract

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 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.

Zusammenfassung

Dieses Dokument definiert die Sprache Tl, die sowohl als Anwendungs- als auch Systemprogrammiersprache in der Tycoon Datenbankumgebung verwendet wird. Das Tycoon Projekt folgt dem add-on-Ansatz zur generischen Datenbankprogrammierung, der besonders die typsichere Systemskalierbarkeit und -erweiterbarkeit unterstützt.

Tl ist eine polymorphe funktionale Programmiersprache zweiter Ordnung mit imperativen Eigenschaften und induktiv definierten Subtypisierungsregeln über Typen und Typoperatoren, erweitert um Sprachkonstrukte, die durch die Anforderungen der Datenbankprogrammierung begründet sind.

Contents

1 The Rationale behind Tl 1

2 Tl: A Language Overview 3

3 The Tl Grammar 9 3.1 Symbols . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9 3.2 Reserved Keywords . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10 3.3 Compilation Units . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11 3.4 Bindings . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11 3.5 Values . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12 3.6 Signatures . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13 3.7 Types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13 3.8 Identifier . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14

4 The Tl Abstract Syntax 15 4.1 Syntactic Objects of Tl . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15 4.2 Normalization of Tl Programs . . . . . . . . . . . . . . . . . . . . . . . . . . 15 4.3 Signatures, Bindings and Types . . . . . . . . . . . . . . . . . . . . . . . . . . 18 4.4 Values . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 18

5 The Static Semantics of Tl 21 5.1 Overview over the Type Notations . . . . . . . . . . . . . . . . . . . . . . . . 21 5.2 Substitutions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 22 5.3 Qualified Type Variables . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 22 5.4 Contractive Types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 23 5.5 Well-formed Signatures . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 23 5.6 Well-formed Types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24 5.7 Signatures of Types and Values . . . . . . . . . . . . . . . . . . . . . . . . . . 25 5.8 Subsignatures . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25 5.9 Subtypes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25 5.10 Signatures of Bindings . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 27 5.11 Types of Values . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 5.12 Restrictions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29

1 The Rationale behind Tl

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 generic servers are relational database systems, object stores, transaction monitors, deduction engines, graphical user interface generators or communication subsystems.

The Tycoon^{1} project aims at a substantially improved server exploitation and database programmer productivity by providing an integrated linguistic and architectural framework for the flexible integration of generic services into an open database programming environment. The Tycoon project activities towards this goal include [Matthes 1992]

▷ 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.

▷ the extension of this language kernel to a fully-fledged strongly-typed polymorphic programming language (Tl, Tycoon Language) that also includes specific language concepts for integrating, extending, tailoring and using the generic database servers mentioned above;

▷ the definition of the data and program representation as well as the evaluation semantics of an untyped intermediate language (Tml, 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;

▷ the definition of a data-model-independent object store protocol (Tsp, Tycoon Store Protocol) that decouples Tml evaluators from object stores and their components for access optimization, storage reclamation, persistence, concurrency, recovery or distribution.

The overall Tycoon system architecture is sketched in Fig. 1 on page 2. This report presents the design of Tl, an integrated application and system programming language that

▷ provides uniform and expressive naming, binding and scoping rules for all language entities (values, functions, types, type operators),

▷ is not restricted to a particular modeling or programming style (e.g. purely functional, relational or strictly object-oriented),

▷ minimizes built-in language functionality in favor of flexible system add-ons [Matthes and Schmidt 1991a],

▷ is equipped with powerful type abstraction mechanisms like (bounded) type parameterization, (parital) type hiding and run-time type discrimination [Matthes and Schmidt 1991b],

1Tycoon: Typed COmmunicating Objects in Open eNvironmens

Figure 1: Layers and interfaces of the Tycoon system

▷ supports the operational requirements of todays data-intensive environments (longevity, evolution, distribution, merging of independently developed system components) [Schmidt and Matthes 1991].

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 P-Quest system, a persistent version of the Quest language developed by Luca Cardelli [Cardelli 1989; Cardelli 1990] on top of the Napier Persistent Object Store develped at the University of St. Andrews [Brown and Rosenberg 1991]. Much emphasis is put on the exchangability and reusability of the individual compiler components by using (wherever possible) compiler generator technology [Schröder and Matthes 1992].

2 Tl: A Language Overview

The type-theoretic core of Tl is F_{≤}, a second-order lambda calculus with subtyping [Cardelli et al. 1991]. 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.

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.

Base Types Tl carefully avoids any non-standard treatment (like static binding, pervasive scoping, non-standard associativity, precedence or overloading) of the usually builtin 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 literals within the relevant Tl language processor components (scanner, type checker, code generator).

Mutability Value variables in a Tl binding or signature can be marked with a var keyword. The phrase let var i = 1) introduces a mutable binding between the variable i and the value 1. The variable i can be re-bound using a polymorphic assignment function in the Tycoon programming environment. This function has the signature :=(A <:Ok 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 l-value bindings (aliasing). Modifiability in Tl is therefore not captured by first-class type and value constructors (like 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 [Connor et al. 1991]).

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 [Burstall and Lampson 1984; Cardelli 1989]).

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 Repeat another named signature in the definition of a new signature and to 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 inheritance as found in objectoriented languages.

Higher-Order Subtyping Type judgements in Tl are understood as partial specifications. For example, the signature x :A asserts that a value bound to the variable x satisfies at least the specification given by the type expression A. An actual value binding let x = a may satisfy a more precise specification x :B. The idea that a value satisfying a stronger specification B also satisfies a weaker specification A is captured by an inductively defined subtyping relationship on types (Tl notation: B <: A). For aggregate values, this view coincides with the notion of subtyping based on information content [Ohori et al. 1989]. For example, the type Let A = Tuple name :String end provides less information than the type Let B = Tuple name :String age :Int 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 (Ok, top type) and the unsatisfiable specification (Nok, bottom type). The latter appears naturally in the typing rules for exceptions and empty arrays (see § 5.11). In Tl it is necessary to specify a bound for a type variable that appears in a signature (e.g., X <:A). Again, this bound is to be understood as a partial specification of the actual type that appears in the matching binding Let X = B and may involve the constants Ok and Nok. Finally, Tl extends the subtyping relation to type operators, i.e. parameterized specifications (see § 5.9)

[Subtype Oper]

\frac{S ⊢ S′′ <:: S′ S, S′′ ⊢ A <: B}{S ⊢ Oper(S′)A <: Oper(S′′)B}

For example, given

Let F = Oper(X <:Tuple name :String end) Tuple x :X y :X end Let G = Oper(X <:Tuple name :String age :Int end) Tuple x :X end

F <:G is derivable, since any specification F(X) obtained by instantiating F with an actual type parameter X that is admissable for G yields a specification that is at least as strong as G(X).

The introduction of a top type Ok and the generalization of the subtyping relation to type operators also covers the notion of kinds (types of types), as introduced in [Cardelli 1989]. For example, all unbounded unary type operators (e.g. List, Array) are subtypes of Oper(X <:Ok) Ok.

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:

Let Nat = Tuple T<:Ok zero :T succ(:T) :T eq(:T :T) :T end let nat1 = Tuple Let T = Int … end let nat2 = Tuple Let T = String … end let null(x :nat1.T) = nat1.eq(x nat1.zero) let null2(rep :Nat x :rep.T) = rep.eq(x rep.zero)

Bound specifications in the signature of an abstract data type allow to reveal partial type information about the witness type 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.

Recursive Type Operators The subtyping rules for recursive types and type operators in Tl violate the concept of purely structural subtyping. For example, given

Let Rec List(A <: Ok) = Tuple hd :A tl :List(A) end Let Rec List2(A <: Ok) = Tuple hd :A

tl :Tuple hd :A tl :List(A) end end

none of the following subtype relationships is derivable:

List(Ok) <:List2(Ok) List2(Ok) <:List(Ok) List <:List2 List2<:List

On the other hand, a single step “unfolding” of List(A) in the definition of List yields a type operator that is structurally equivalent to 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 [Cardelli 1992b]), the problem of checking the equivalence between parameterized recursive type expressions becomes decidable (compare [Solomon 1978]) and a class of subtype relationships that play an important role in object-oriented programming can be handled within Tl. For example, given

Let Rec List(E <:Ok) = Tuple cons(:E) :List(E) hd() :E tl() :List(E) map(E2 <:Ok f(:E) :E2) :List(E2) end Let Rec List2(E <:Ok) = Tuple cons(:E) :List2(E) hd() :E tl() :List2(E) map(E2 <:Ok f(:E) :E2) :List2(E2) powerset(p(:E) :Bool) :List2(List(E)) end

List2(Int) <:List(Int) and List2 <:List are derivable type judgements in Tl.

Tuples and Variants The concepts of labeled cartesian product types and discriminated union types are captured by tuples and variants in Tlthat exhibit an interesting subtype relationship. A pure discriminated union type is represented by a variant type with variants that do not share common fields while a pure cartesian product type can be viewed a variant type with a single variant and an anonymous variant label. A prime motivation behind this view 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

Let Address = Tuple city :String zip :Int end let a :Address = tuple let city = ”Hamburg” let zip = 2000 end

that is still usable in an extended system version with the following type and function definitions:

Let NewAddress = Variant city :String case national with zip :Int case international with country :String zip :String end let print(adr :NewAddress) :Ok = … print(a)

Extensible Records As argued in [Atkinson and Morrison 1988; Morrison et al. 1987; Schmidt and Matthes 1991], long-lived data-intensive applications require naming schemes that are capable of handling 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.

let db = record let parts = … let suppliers = … end

The selection of a field in a record value 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 let newDB = extend db with let assembly = … end yields a record value with the same identity as 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 db is already extended by a field assembly). In contrast to Napier88 [Dearle et al. 1989], 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 negative information in record type expressions (e.g. values of record type X are defined not have an assembly field) [Cardelli 1992a; Wand 1987; Stansifer 1988; Cardelli and Mitchell 1989; Rémy 1991]. 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 Tlgives 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 extend operator is not required: The record type Record S end is a subtype of Record S’ end if the signatures S can be obtained by dropping subsignatures at arbitrary positions from S’ (see [Subsig Rcd] in § 5.8). The subtype graph for record types can therefore form a DAG (multiple inheritance) and not just a tree (single inheritance) like for tuple types.

Modules and Libraries The modularization facilities in Tl are interface, module and 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 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 import statements. Cyclic import dependencies are not allowed. If a module m1 is imported into a module m2, the evaluation of m1 precedes the evaluation of m2.

The modularization facilities in Tl do not introduce new naming, typing and binding concepts into the language, they simply 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).

Dynamic Types In analogy to the mutability attribute for value variables, a dynamic (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. Compared with other proposals [Abadi et al. 1989; Abadi et al. 1992] 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.

With respect to decidability, Tl is in the same position as F_{≤}[Pierce 1992]. Decidability problems arise through the subtyping rule [Subtype Fun] in combiation with the subsignature rule [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 [Subsig Ide]) in the context of rule [Subtype Fun], termination of the subtype algorithm can be guaranteed [Pierce

3 The Tl Grammar

The following notation is used for the definition of syntactical and lexical elements. Id denotes a non-terminal symbol (a meta variable) and A and B denote syntactic expressions.

Id_{1}, …, Id_{n}::= A; the non-terminal symbols Id_{i} are defined as A (n ≥ 1)
Id  a non-terminal symbol
if  a terminal symbol
"x"  the character x ("" is the empty string """ is a double quote)
( A )  means A
A B  means A followed by B (binds strongest)
A | B  means A or B
[ A ]  means ( "" | A )
{ A }  means ( "" | A { A } )

3.1 Symbols

The source text of a Tl program consists of a sequence of characters that is converted into a sequence of symbols of the categories int, real, longreal, char, string, identifier, infix, colonInfix and delimiter.

The set of formatting characters is an implementation-dependent subset of the nonprintable 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 (* *). 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.

int::=

["~"] digit { digit } ; real::=

int "." digit { digit } |

int [ "." digit { digit } ] "E" int ; longreal::=

int [ "." digit { digit } ] "D" int ; char::=

"’" ( digit | alpha | special | escape | delimiter | reserved ) "’" ; string::=

""" { digit | alpha | special | escape | delimiter | reserved } """ ; infix::=

special { special } ; colonInfix::=

":" { special } ; identifier::=

alpha { digit | alpha } ; delimiter::=

     "(" | ")" | "{" | "}" | "[" | "]" | "." | "," | ";"

; digit::=

     "0" | "1" | "2" | "3" | "4" | "5" | "6" | "7" | "8" | "9"

; alpha::=

"A" | "B" | ... | "Z" | "a" | "b" | ... | "z" ; reserved::=

     "~" | " "

; special::=

     "@" | "#" | "$" | "%" | "&" | "*" | "_" | "+" | "=" | "-" |
     "|" | "\" | "`" | ":" | "<" | ">" | "/" | "^" | "?" | "!"

; escape::=

"\" ("n" | "t" | "r" | "f" | "\" | "'" | """ | digit digit digit) ;

Escape characters in character and string literals are interpreted as follows:

\n  new line
\t  tab
\r  carriage return
\f  form feed

  \'      '
  \"      "
  \\      \

\nnn  A single character with the code nnn

(three decimal digits that denote an integer in the interval [0,255]

\f … f\ The sequence of formatting characters f is ignored

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.

3.2 Reserved Keywords

The following identifiers and (colon-) infix symbols are reserved keywords and cannot be used as user-defined identifiers in Tl programs. and andif as begin case do downto dynamic new dynamic be else elsif end exception exit export extend fun hide infix if import in interface let library loop module of ok open orif raise reraise rec then try tuple typeRep new upto var variant when while with Dyn Exception Fun Let Nok Ok Oper Rec Repeat Tuple Variant = <: : ? !

3.3 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. Unit is the root production for the language.

Unit::=

( Library | Interface | Module | Import | Bindings ) ";" ; Library::=

library identifier Import with { ComponentSignatures } [ hide { identifier } ] end

; ComponentSignatures::=

library { identifier } | interface { identifier } | module { identifier ":" identifier }

; Interface::=

interface identifier Import export Signatures end ; Module::=

module identifier Import export Bindings end ; Import::=

[ import { [ ":" ] identifier } ] ;

3.4 Bindings

Bindings::=

{ TypeBindings | ValueBindings | open ValueIde [ as Type ]

":" [ Dyn ] Type | [ var ] Value } ; TypeBindings::=

{ Let [ Rec ] TypeBinding { and TypeBinding } } ; TypeBinding::=

[ Dyn ] TypeIde Parameters [ "<:" Type ] "=" Type ; ValueBindings::=

{ let [ rec ] ValueBinding { and ValueBinding } } ; ValueBinding::=

[ var ] ValueIde Parameters [ ":" Type ] "=" Value ;

3.5 Values

Value::= fun "(" Signatures ")" [ ":" Type ] Value | assert Value | Value_{1}

; Value_{1}::=

Value_{2} { ( orif | andif | colonInfix ) Value_{2} } ; Value_{2}::=

Value_{3} { infix Value_{3} } ; Value_{3}::=

Value_{4} { "(" Bindings ")" | "?" CaseIde | "!" CaseIde | "." FieldIde | "[" Value "]" | of Bindings end }

; Value_{4}::=

"{" Value "}" |

ValueIde | ok | int | char | string | real | longreal | tuple Bindings end | variant CaseIde of Type [ with Bindings ] end record Bindings end | extend Value [ with Bindings ] end | array Bindings end | exception Value [ with Signatures ] end | begin Bindings end | if Value then Bindings { elsif Value then Bindings }

[ else Bindings ] end | case [ of ] Value { when CaseIdeList [ with ValueIde ] then Bindings }

[ else Bindings ] end | loop Bindings end | exit | while Value do Bindings end | for ValueIde "=" Value ( upto | downto ) Value do Bindings end | try Bindings { when Value [ with ValueIde ] then Bindings }

[ else Bindings ] end | raise Value [ with Bindings ] end | reraise | typeRep new "(" ":" Type ")" | dynamic new "(" Value ")" | dynamic be "(" Value ":" Type ")"

;

3.6 Signatures

Signatures::=

{ TypeSignatures | ValueSignatures | TypeBindings | Repeat Type } ; TypeSignatures::=

[ Dyn ] [ TypeIdeList Parameters ] "<:" Type ; ValueSignatures::=

[ var ] [ ValueIdeList Parameters ] ":" Type ; Parameters::=

{ "(" Signatures ")" } ;

3.7 Types

Type::= Oper "(" Signatures ")" [ "<:" Type ] Type | Fun "(" Signatures ")" ":" Type | Type_{1}

; Type_{1}::=

Type_{2} { colonInfix Type_{2} } ; Type_{2}::=

Type_{3} { infix Type_{3} } ; Type_{3}::=

Type_{4} { "(" { Type } ")" } ; Type_{4}::=

"{" Type "}" |

{ ValueIde "." } TypeIde | Ok | Nok | Tuple Signatures end | Variant Signatures { case CaseIdeList [ with Signatures ] } end | Record Signatures end | Exception [ Signatures ] end

;

3.8 Identifier

ValueIdeList, TypeIdeList, CaseIdeList::=

Ide { "," Ide } ; Ide, ValueIde, TypeIde, FieldIde, CaseIde::=

identifier | infix ( infix | colonInfix ) ;

4 The Tl Abstract Syntax

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.

4.1 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:

S ∈ Sig  sequences of signatures
D ∈ Bind  sequences of bindings
E ∈ BindElem single bindings
A, B ∈ Type  types
C ∈ Case  variants in tuple types
z ∈ CaseIde  variant labels
X, Y ∈ Ide  type identifiers
x, y ∈ ide  value identifiers
a, b, c ∈ Value values
p, q ∈ Qualifier selectors of signature components

The infinite sets Ide, ide and CaseIde are built from the union of the symbols of the categories identifier, infix and colonInfix as defined in § 3.1 extended by the symbol ?, called the anonymous identifier. These sets and the set of literals (symbols of the categories int, real, longreal, char, string) constitute the basis for the inductive definition of the sets of the other syntactic objects as summarized in table 1 and table 2.

4.2 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

▷ introduces the anonymous identifier ? in bindings

:A a ⇒ Let ? = A let ? = a

and in signatures

<:A :B ⇒ ? <:A ? :B

An anonymous identifier ? matches any other identifier x, X in the subtyping rules for

signature matching [Subsig ide, Subsig Ide, Subsig Ide Let] in § 5.8.

▷ expands abbreviating notations in bindings

let x(S_{1}) … (S_{n}) :A = a  ⇒ let x = fun(S_{1}) … fun(S_{n}) :A = a
let x(S_{1}) … (S_{n}) = a  ⇒ let x = fun(S_{1}) … fun(S_{n}) = a
Let X(S_{1}) … (S_{n}) <:A = B ⇒ Let X = Oper(S_{1}) … Oper(S_{n}) <:A = B
Let X(S_{1}) … (S_{n}) = A  ⇒ Let X = Oper(S_{1}) … Oper(S_{n}) = A

and in signatures

x_{1}, …, x_{n} :A  ⇒ x_{1} :A … x_{n} :A
var x_{1}, …, x_{n} :A  ⇒ var x_{1} :A … var x_{n} :A
Dyn X_{1}, …, X_{n} <:A ⇒ Dyn X_{1} <:A … Dyn X_{n} <:A
x(S_{1}) … (S_{n}) :A  ⇒ x :Fun(S_{1}) …:Fun(S_{n}) :A
X(S_{1}) … (S_{n}) <:A  ⇒ X :Oper(S_{1}) … Oper(S_{n}) A

▷ transforms infix and listfix function applications into a standard prefix notation

x_{1} infix x_{2}  ⇒ {infix(x_{1} x_{2})}
x_{1} colonInfix x_{2} ⇒ {colonInfix(x_{1} x_{2})}
f of x_{1} … x_{n} end ⇒ f(array x_{1} … x_{n} end)

▷ transforms infix type operator applications into prefix notation

X_{1} infix X_{2}  ⇒ {infix(X_{1} X_{2})}
X_{1} colonInfix X_{2} ⇒ {colonInfix(X_{1} X_{2})}

▷ replaces missing else branches in if and try expressions (but not in case expressions) by an empty expression sequence (that evaluates to ok, see [Value seq empty] in § 5.11), for example,

if a then b end ⇒ if a then b else end

▷ normalizes elsif branches into nested if expressions

if a_{1} then b_{1}

elsif a_{2} then b_{2}

…

end

⇒

if a_{1} then b_{1} else

if a_{2} then b_{2}

… end

end

▷ replaces assertions by conditionals

assert a ⇒ if a then ok else

raise exception “Assertion in file … at line … failed”

end end

S ::= ⊘  empty signature
| S, x : A  value signature
| S, X <: A  type signature
| S, X = A  type definition
| S, Repeat(A)  signature inheritance

;

D ::= ⊘  empty binding
| D, E  sequential binding
| D, E_{1}| … |E_{n}  parallel binding
| D, open(x)  binding inheritance
| D, open(x, A)  binding projection

;

E ::= x = a  value binding
| x : A = a  constrained value binding
| X = A  type binding
| X <: A = B  constrained type binding

;

A, B ::= Ok  supertype of all types (top)
| Nok  subtype of all types (bottom)
| X  type identifier
| p.X  abstract type identifier
| Bool | Int | String  base type identifiers
| Arr(A)  array type
| Fun(S) : A  (polymorphic) function type
| Tup(S; C)  tuple type (with variants)
| Rcd(S)  record type
| Exc(S)  exception type
| Rec(X, X_{1} <: A_{1} = B_{1} … X_{n} <: A_{n} = B_{n}) recursive type (1 ≤ n)
| Var(A)  type of mutable values
| Dyn(A)  dynamic type
| Oper(X_{1} <: A_{1}, …, X_{n} <: A_{n})B  type operator
| A(D)  type operator application

;

C ::= Case(z_{1}, S_{1}) … Case(z_{n}, S_{n})  variants in tuple types (0 ≤ n)

;

p ::= x  value signature selector
| p.x  field signature selector

; Table 1: Abstract syntax for signatures, bindings and types

4.3 Signatures, Bindings and Types

Table 1 summarizes the inductive definition of signatures, bindings and types in Tl.

The distinction between type signatures and type definitions in signatures reflects the fact that most type judgements provide a partial information (X <: A) and that only in few cases (e.g. Let type bindings in the local scope) the exact type associated with a type variable X is available (X = A).

The base type constants (Int, Bool …) 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

Let Rec X<:Ok = F(Y) and Y<:Ok = G(X);

This binding is represented in the abstract syntax as a parallel binding of two type variables (X and Y) to two independent recursive types that both describe the full recursive equation system:

X = Rec(X_{1}, X_{1} <: Ok = F (X_{2}), X_{2} <: Ok = G(X_{1}))

and

Y = Rec(X_{2}, X_{1} <: Ok = F (X_{2}), X_{2} <: Ok = 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 (<:Ok in the example above) are required to simplify the checking of type operator applications within the recursive binding, for example

Let Rec A1 = A2(A2) and A2 = A3(A3) and …

and An = Oper(X(Y <:Ok) <:Ok) X(Int)

has to be written as

Let Unary = Oper(X(Y <:Ok) <:Ok) Ok

Let A1 <:Unary = A2(A2) and A2 <:Unary = A3(A3) and … and An <:Unary = Oper(X(Y <:Ok) <:Ok) X(Int)

The var attribute of value bindings and signatures and the Dyn attribute of type bindings and signatures are both mapped to explicit type constructors. This implies that types like Var(Var(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.

4.4 Values

Table 2 summarizes the inductive definition of values in Tl. The syntax is quite standard and therefore does not require further explanation.

a, b ::= ok  the canonical value of type Ok
| int  integer literals (s. § 3.1)
| real  floating point literals (s. § 3.1)
| longreal  double precision floating point literals (s. § 3.1)
| char  character literals (s. § 3.1)
| string  string literals (s. § 3.1)
| x  value identifier
| fun(S)a  (polymorphic) function constructor
| a(D)  function application
| arr(D)  array constructor
| a[b]  array element selection
| tup(D, z, D′)  tuple constructor (with variants)
| rcd(D)  record constructor
| a.x  tuple, record and execption field selection
| a!z  variant projection
| a?z  variant test
| extend(a, D)  record extension
| exc(a, D)  exception value generation
| seq(D)  sequential evaluation
| if(a, b_{1}, b_{2})  conditional
| case(a,  variant analysis (0 ≤ n, 1 ≤ k_{i})

(z_{11} … z_{1k_{1}}, y_{1}, b_{1}) … (z_{n1} … z_{nk_{n}}, y_{n}, b_{n}), b)

| case(a,  exhaustive variant analysis
(z_{11} … z_{1k_{1}}, y_{1}, b_{1}) …  (1 ≤ n, 1 ≤ k_{i})

(z_{n1} … z_{nk_{n}}, y_{n}, b_{n}))

| loop(a_{1})  loop
| exit  loop exit
| while(a, b)  pre-check loop
| for(x, a_{1}, a_{2}, a_{3})  integer iteration
| try(a,  exception handling (0 ≤ n)

(a_{1}, y_{1}, b_{1}) … (a_{n}, y_{n}, b_{n}), b)

| raise(a, D)  exception generation
| reraise  exception propagation
| andif(a, b)  conditional conjunction
| orif(a, b)  conditional disjunction

; Table 2: Abstract syntax for values

The syntax does not contain an assignment operator since assignments are provided by a polymorphic function in the programming environment with the following signature:^{2}

:= (A <:Ok var lhs :A rhs :A)

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 else branch.

2Different implementations of the assignment function may attach recovery or concurrency control functionality to the plain destructive update operator.

5 The Static Semantics of Tl

A medium-term goal in the Tycoon project is to provide a formal definition of 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.

5.1 Overview over the Type Notations

The following notations are used for the definition of the static semantics of Tl:

A↓X  The type A is contractive in variable X  § 5.4
S sig  The signatures S are well-formed  § 5.5
S rcdsig The signatures S are well-formed record signatures § 5.5
A type The type A is well-formed  § 5.6
A ::^{Sig} S The type A has signatures S  § 5.7
p ::^{Sig} S The selector p identifies a value with signatures S § 5.7
S <:: S′ S are subsignatures of S′  § 5.8
S <::^{T up} S′ S are tuple subsignatures of S′  § 5.8
S <::^{Rcd} S′ S are record subsignatures of S′  § 5.8
A <: B A is a subtype of B  § 5.9
D :: S  The bindings D have signatures S  § 5.10
a : A  The value a has type A  § 5.11

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:

S, S′ the signatures in S followed by signatures in S′
D, D′ the bindings in D followed by bindings in D′

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:

x ∈ Dom(S) the value variable x is defined in S
X ∈ Dom(S) the type variable X is defined in S

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 static environment. The environment itself is represented as an ordered list S of signatures:

S ⊢ J in the static environment S the judgement J is true

5.2 Substitutions

The type rules for the instantiation of polymorphic function [Value apply] in § 5.11 and of type operators [Type apply] in § 5.6 use the following notation to denote the variable capture avoiding substitution of free type variables in a type expression by an actual type parameter:

A{X ← B} A where each free occurence of X is substituted by B

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 [de Bruijn 1972; Abadi et al. 1990]^{3}.

A sequence of bindings D passed as actual parameters to a polymorphic function or a type operator defines an iterated substitution of the type variables X defined in D by their associated type expressions:

A{⇐ D} A where all X, x ∈ Dom(D) are substituted as follows

[Subst empty]

\overline{S ⊢ A\{⇐ ⊘\} = A}

[Subst Ide]

\frac{S ⊢ D :: S′ S, S′ ⊢ D′ :: X <: B}{S ⊢ A\{⇐ D, D′\} = A\{⇐ D\}\{X ← B\}}

[Subst Let]

\frac{S ⊢ D :: S′ S, S′ ⊢ D′ :: X = B}{S ⊢ A\{⇐ D, D′\} = A\{⇐ D\}\{X ← B\}}

[Subst ide]

\frac{S ⊢ D :: S′ S, S′ ⊢ D′ :: x : B}{S ⊢ A\{⇐ D, D′\} = A\{⇐ D\}}

5.3 Qualified Type Variables

The access to the type information associated with individual type or value components in

a tuple or a record [Subtype Dot] [Value tuple dot] [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.

qualify(T; p; S) substitute in T each occurence of X ∈ Dom(S) by p.X

where T ∈ Sig ∪ Type. This qualification is defined inductively as follows:

qualify(T; p; ⊘) = T
qualify(T; p; S, x : B) = qualify(T {x ← p.x}; p; S)
qualify(T; p; S, X <: B) = qualify(T {X ← p.X}; p; S)
qualify(T; p; S, X = B) = qualify(T {X ← p.X}; p; S)

3This is also the mechanism used in the Tl type checker.

5.4 Contractive Types

A final auxiliary notation is required in rule [Type Rec] in § 5.6 to restrict the structure of recursive types to contractive type expressions.

S ⊢ A↓X In environment S type A is contractive in variable X

Systems of recursive type equations Rec(X_{i}, X_{1} <: A_{1} = B_{1} … X_{n} <: A_{n} = B_{n}) that are contractive in their recursion variable X_{i} define well-formed regular trees, the basis for semantic models of type structures [MacQueen et al. 1986] as well as termination proofs for type checking algorithms [Ohori 1989].

The following judgements are independent of the identifiers occuring in the the static environment:

Y ↓X ⇔ Y ≠ X
Ok↓X Nok↓X Bool↓X Int↓X String↓X

x.Y ↓X Fun(S′) : B ↓X Tup(S′; C)↓X Rcd(S′)↓X Exc(S′)↓X Arr(A)↓X

Var(A)↓X ⇔ A↓X
Dyn(A)↓X ⇔ A↓X

The last three judgements refer to the static environment S:

[Contractive Oper]

\frac{S, S′ ⊢ B ↓X}{S ⊢ Oper(S′)B ↓X}

[Contractive Rec]

\frac{S ⊢ Rec(X_{i}, X_{1} <: A_{1} = B_{1} … X_{n} <: A_{n} = B_{n}) type}{S ⊢ Rec(X, X_{1} <: A_{1} = B_{1} … X_{n} <: A_{n} = B_{n})↓Y}

[Contractive Apply]

\frac{S ⊢ A <: Oper(S′)B S ⊢ D :: S′ S ⊢ B\{⇐ D\}↓X}{S ⊢ A(D)↓X}

The above definition is well-founded although rule [Contractive Rec] itself requires the definition of well-founded types, since the syntax of Tl does not allow statically nested recursive type declarations.

5.5 Well-formed Signatures

[Sig empty] ; \overline{⊢ ⊘ sig} [Sig ide] ; \frac{S ⊢ A type}{⊢ S, x : A sig} [Sig Ide] ; \frac{S ⊢ A type}{⊢ S, X <: A sig} [Sig Ide Let]

\frac{S ⊢ A type}{⊢ S, X = A sig}

[Sig Repeat]

\frac{S ⊢ A ::^{Sig} S′ ⊢ S′ sig}{⊢ S, Repeat(A) sig}

[Rcdsig] ; \frac{⊢ S, S′ sig (S′ = S_{1}, S_{2} ∧ X ∈ Dom(S_{1}) ⇒ X ∉ Dom(S_{2}))}{S ⊢ S′ rcdsig}

5.6 Well-formed Types

[Type Builtin]

\frac{⊢ S sig A ∈ \{Ok, Nok, Bool, Int, String\}}{S ⊢ A type}

[Type Ide] ; \frac{⊢ S, X <: A, S′ sig X ∉ Dom(S′)}{S, X <: A, S′ ⊢ X type}

[Type Ide Let]

\frac{⊢ S, X <: A, S′ sig X ∉ Dom(S′)}{S, X = A, S′ ⊢ X type}

[Type Dot] ; \frac{S ⊢ p ::^{Sig} S′ S, S′ ⊢ X type X ∈ Dom(S′)}{S ⊢ p.X type} [Type Fun]

\frac{⊢ S, S′ sig S, S′ ⊢ B <: Ok}{S ⊢ Fun(S′) : B type}

[Type Tup]

\frac{1 ≤ n z_{i} ≠ z_{j} i ≠ j ⊢ S, S′ sig ⊢ S, S′, S_{i} sig i = 1 … n}{S ⊢ Tup(S′; Case(z_{1}, S_{1}) … Case(z_{n}, S_{n})) type}

[Type Rcd]

\frac{S ⊢ S′ rcdsig}{S ⊢ Rcd(S′) type}

[Type Exc]

\frac{⊢ S, S′ sig}{S ⊢ Exc(S′) type}

[Type Rec]

S, X_{1} <: A_{1}, …, X_{n} <: A_{n} ⊢ B_{i} <: A_{i} i = 1 … n 1 ≤ j ≤ n

S, X_{1} = B_{1}, …, X_{n} = B_{n} ⊢ B_{i} ↓X_{i} i = 1 … n

S ⊢ Rec(X_{j}, X_{1} <: A_{1} = B_{1} … X_{n} <: A_{n} = B_{n}) type

[Type Var]

\frac{S ⊢ A <: Ok}{S ⊢ Var(A) type}

[Type Dyn]

\frac{S ⊢ A type}{S ⊢ Dyn(A) type}

[Type Arr]

\frac{S ⊢ A <: Ok}{S ⊢ Arr(A) type}

[Type Oper]

\frac{⊢ S, S′ sig S, S′ ⊢ B type}{S ⊢ Oper(S′)B type}

\frac{S ⊢ A <: Oper(S′)B S ⊢ D :: S′}{S ⊢ A(D) type}

[Type Apply]

5.7 Signatures of Types and Values

[Select ide]

\frac{S ⊢ x : A S ⊢ A ::^{Sig} S′}{S ⊢ x ::^{Sig} S′}

[Select dot]

\frac{S ⊢ p ::^{Sig} S′ x ∈ Dom(S′) S, S′ ⊢ x ::^{Sig} S′′}{S ⊢ p.x ::^{Sig} S′′}

[Select Tup]

\frac{S ⊢ A : Tup(S′; C)}{S ⊢ A ::^{Sig} S′}

[Select Rcd]

\frac{S ⊢ A : Rcd(S′)}{S ⊢ A ::^{Sig} S′}

[Select Exc]

\frac{S ⊢ A : Exc(S′)}{S ⊢ A ::^{Sig} S′}

[Select Fun]

\frac{S ⊢ A : Fun(S′) : B}{S ⊢ A ::^{Sig} S′}

[Select Oper]

\frac{S ⊢ A : Oper(S′)B}{S ⊢ A ::^{Sig} S′}

5.8 Subsignatures

[Subsig reflexive]

\frac{⊢ S, S′ sig}{S ⊢ S′ <:: S′}

[Subsig ide]

\frac{S ⊢ S′ <:: S′′ S, S′ ⊢ A <: B}{S ⊢ S′, x : A <:: S′′, x : B}

\frac{S ⊢ S′ <:: S′′ S, S′ ⊢ A <: B}{S ⊢ S′, X <: A <:: S′′, X <: B}

\frac{S ⊢ S′ <:: S′′ S, S′ ⊢ A <: B}{S ⊢ S′, X = A <:: S′′, X <: B}

\frac{S ⊢ S′ <:: S′′ S, S′ ⊢ A ::^{Sig} S′′′}{S ⊢ S′, Repeat(A) <:: S′′, S′′′}

\frac{⊢ S, S_{1}, S_{2} sig S ⊢ S_{1} <:: S′_{1}}{S ⊢ S_{1}, S_{2} <::^{T up} S′_{1}}

\frac{S ⊢ S_{1}, S_{2}, S_{3} rcdsig S ⊢ S_{1}, S_{3} <::^{Rcd} S′_{1} S, S′_{1} ⊢ S_{2} <::^{T up} S′_{2}}{S ⊢ S_{1}, S_{2}, S_{3} <::^{Rcd} S′_{1}, S′_{2}}

5.9 Subtypes

\frac{S ⊢ A type}{S ⊢ A <: A}

\frac{S ⊢ A <: A′ S ⊢ A′ <: A′′}{S ⊢ A <: A′′}

\frac{S ⊢ A <: Ok}{S ⊢ Nok <: A}

\frac{⊢ S sig A ∈ \{Bool, Int, String\}}{S ⊢ A <: Ok}

\frac{S ⊢ Fun(S′) : B type}{S ⊢ Fun(S′) : B <: Ok}

[Subsig Ide]

[Subsig Ide Let] [Subsig Repeat]

[Subsig Tup] [Subsig Rcd] [Subtype reflexive]

[Subtype transitive]

[Subtype Nok] [Subtype Ok Builtin]

[Subtype Ok Fun]

[Subtype Ok Tup]

\frac{S ⊢ Tup(S′; C) type}{S ⊢ Tup(S′; C) <: Ok}

[Subtype Ok Rcd]

\frac{S ⊢ Rcd(S′) type}{S ⊢ Rcd(S′) <: Ok}

[Subtype Ok Exc]

\frac{S ⊢ Exc(S′) type}{S ⊢ Exc(S′) <: Ok}

[Subtype Ok Arr]

\frac{S ⊢ Arr(A) type}{S ⊢ Arr(A) <: Ok}

[Subtype Ok Var]

\frac{S ⊢ Var(A) type}{S ⊢ Var(A) <: Ok}

[Subtype Ok Dyn]

\frac{S ⊢ A <: Ok}{S ⊢ Dyn(A) <: Ok}

[Subtype Ide]

\frac{⊢ S, X <: A, S′ sig X ∉ Dom(S′)}{S, X <: A, S′ ⊢ X <: A}

[Subtype Ide Let]

\frac{⊢ S, X <: A, S′ sig X ∉ Dom(S′)}{S, X = A, S′ ⊢ X <: A}

[Subtype Ide Let2]

\frac{⊢ S, X <: A, S′ sig X ∉ Dom(S′)}{S, X = A, S′ ⊢ A : X}

[Subtype Dot]

\frac{S ⊢ p ::^{Sig} S′, X <: A, S′′ X ∉ Dom(S′′)}{S ⊢ p.X <: qualify(A; p; S′)}

[Subtype Fun]

\frac{S ⊢ S′′ <:: S′ S, S′′ ⊢ A <: B}{S ⊢ Fun(S′) : A <: Fun(S′′) : B}

[Subtype Arr]

\frac{S ⊢ A <: B}{S ⊢ Arr(A) <: Arr(B)}

[Subtype Tup]

S ⊢ S_{0}, S_{i} <::^{T up} S′_{0}, S′_{i} i = 1 … n 1 ≤ n

S ⊢ S′_{0}, S′′_{j} sig j = 1 … m 1 ≤ m

S ⊢ Tup(S_{0}; Case(z_{1}, S_{1}) … Case(z_{n}, S_{n})) <:

Tup(S′_{0}; Case(z_{1}, S′_{1}) … Case(z_{n}, S′_{n}) Case(z′_{1}, S′′_{1}) … Case(z′_{m}, S′′_{m}))

[Subtype Rcd]

\frac{S ⊢ S′ <::^{Rcd} S′′}{S ⊢ Rcd(S′) <: Rcd(S′′)}

[Subtype Exc]

\frac{S ⊢ S′ <::^{T up} S′′}{S ⊢ Exc(S′) <: Exc(S′′)}

[Subtype Var]

\frac{S ⊢ A type}{S ⊢ Var(A) <: A}

[Subtype Dyn Elim]

\frac{S ⊢ A type}{S ⊢ Dyn(A) <: A}

[Subtype Dyn]

\frac{S ⊢ A <: B}{S ⊢ Dyn(A) <: Dyn(B)}

[Subtype Non-Rec Rec]

A ≠ Rec(Y, D′)

S ⊢ A <: B_{j}{⇐ X_{1} = Rec(X_{1}, D), …, X_{n} = Rec(X_{n}, D)} S ⊢ A <: Rec(X_{j}, X_{1} <: A_{1} = B_{1} … X_{n} <: A_{n} = B_{n})

[Subtype Rec Non-Rec]

A ≠ Rec(Y, D′)

S ⊢ B_{j}{⇐ X_{1} = Rec(X_{1}, D), …, X_{n} = Rec(X_{n}, D)} <: A S ⊢ Rec(X_{j}, X_{1} <: A_{1} = B_{1} … X_{n} <: A_{n} = B_{n}) <: A

[Subtype Rec Rec]

\frac{S′′ ⊢ A_{i} <: A′_{j} S′′, S′, S ⊢ B_{i} <: B′_{j}}{S′′ ⊢ Rec(X_{i}, X_{1} <: A_{1} = B_{1} … X_{n} <: A_{n} = B_{n}) <: Rec(X′_{j}, X′_{1} <: A′_{1} = B′_{1} … X′_{m} <: A′_{m} = B′_{m})}

where

S′ = X′_{1} <: Rec(X′_{1}, D′), … X′_{j−1} <: Rec(X′_{j−1}, D′), X′_{j} <: A′_{j},
X′_{j+1} <: Rec(X′_{j+1}, D′), … X′_{m} <: Rec(X′_{m}, D′)
S = X_{1} <: Rec(X_{1}, D), … X_{i−1} <: Rec(X_{i−1}, D), X_{i} <: X′_{j},
X_{i+1} <: Rec(X_{i+1}, D), … X_{n} <: Rec(X_{n}, D)
D′ = X′_{1} <: A′_{1} = B′_{1}, …, X′_{m} <: A′_{m} = B′_{m}
D = X_{1} <: A_{1} = B_{1}, …, X_{n} <: A_{n} = B_{n}

[Subtype Oper]

\frac{S ⊢ S′′ <:: S′ S, S′′ ⊢ A <: B}{S ⊢ Oper(S′)A <: Oper(S′′)B}

[Subtype Apply]

\frac{S ⊢ A <: Oper(S′)B S ⊢ D :: S′}{S ⊢ A(D) <: B\{⇐ D\}}

5.10 Signatures of Bindings

[Bind empty] ; \frac{⊢ S sig}{S ⊢ ⊘ :: ⊘} [Bind ide] ; \frac{S ⊢ D :: S′ S, S′ ⊢ a : A}{S ⊢ D, x = a :: S′, x : A} [Bind ide restrict]

\frac{S ⊢ D :: S′ S, S′ ⊢ a : A}{S ⊢ D, x : A = a :: S′, x : A}

[Bind Ide] ; \frac{S ⊢ D :: S′ S, S′ ⊢ A type}{S ⊢ D, X = A :: S′, X = A} [Bind Ide restrict]

\frac{S ⊢ D :: S′ S, S′ ⊢ B <: A}{S ⊢ D, X <: A = B :: S′, X = B}

[Bind and] ; \frac{S ⊢ D :: S′ S, S′ ⊢ E_{i} :: S_{i} i = 1 … n 1 ≤ n}{S ⊢ D, E_{1}| … |E_{n} :: S′, S_{1}, …, S_{n}}

\frac{S ⊢ D :: S′ S, S′, x_{1} : A_{1}, …, x_{n} : A_{n} ⊢ a_{i} : A_{i} i = 1 … n 1 ≤ n}{S ⊢ D, rec(x_{1} : A_{1} = a_{1}| … |x_{n} : A_{n} = a_{n}) :: S′, x_{1} : A_{1}, …, x_{n} : A_{n}}

\frac{S ⊢ D :: S′ S, S′ ⊢ p ::^{Sig} S′′}{S ⊢ D, open(p) :: S′, qualify(S′′; p; S′′)}

\frac{S ⊢ D :: S′ S, S′ ⊢ p ::^{Sig} S′′ S ⊢ A ::^{Sig} S′′′ S ⊢ S′′ <:: S′′′}{S ⊢ D, open(p, A) :: S′, qualify(S′′′; p; S′′)}

[Bind rec] [Bind open] [Bind open restrict]

5.11 Types of Values

[Value subsumption]

\frac{S ⊢ a : A S ⊢ A <: B}{S ⊢ a : B}

[Value ok]

\frac{⊢ S sig}{S ⊢ ok : Ok}

[Value ide]

\frac{⊢ S, x : A, S′ sig x ∉ Dom(S′)}{S, x : A, S′ ⊢ x : A}

[Value fun]

\frac{S, S′ ⊢ a : A}{S ⊢ fun(S′)a : Fun(S′) : A}

[Value apply]

\frac{S ⊢ a : Fun(S′) : A S ⊢ D :: S′}{S ⊢ a(D) : A\{⇐ D\}}

[Value array]

\frac{S ⊢ D :: x_{1} : A … x_{n} : A 1 ≤ n}{S ⊢ arr(D) : Arr(A)}

[Value array empty]

\frac{⊢ S sig}{S ⊢ arr() : Arr(Nok)}

[Value index]

\frac{S ⊢ a : Arr(A) S ⊢ b : Int}{S ⊢ a[b] : A}

[Value tuple]

\frac{S ⊢ D :: S′}{S ⊢ tup(D) : Tup(S′; Case(?, ⊘))}

[Value tuple variant]

\frac{S ⊢ A : Tup(S′; Case(z_{1}, S_{1}) … Case(z_{n}, S_{n})) S ⊢ D :: S′, S_{i} 1 ≤ z_{i} ≤ n}{S ⊢ tup(D; z_{i}; A)) : A}

[Value tuple dot]

\frac{S ⊢ a : Tup(S′, x : A, S′′; C) x ∉ Dom(S′′)}{S ⊢ a.x : qualify(A; a; S′)}

\frac{S ⊢ x : Tup(S′; Case(z_{1}, S_{1}) … Case(z_{n}, S_{n}))}{S ⊢ x!z_{i} : Tup(S′, S_{i}; Case(?, ⊘))}

\frac{S ⊢ x : Tup(S′; Case(z_{1}, S_{1}) … Case(z_{n}, S_{n}))}{S ⊢ x?z_{i} : Bool}

[Value record]

\frac{S ⊢ D :: S′ S ⊢ S′ rcdsig}{S ⊢ rcd(D) : Rcd(S′)}

\frac{S ⊢ a : Rcd(S′, x : A, S′′)}{S ⊢ a.x : qualify(A; a; S′)}

\frac{S ⊢ a : Rcd(S′) S, S′ ⊢ D :: S′′ S ⊢ S′, S′′ rcdsig}{S ⊢ extend(a, D) : Rcd(S′, S′′)}

\frac{S ⊢ a : String S ⊢ D :: S′}{S ⊢ exc(a, D) : Exc(S′)}

\frac{⊢ S sig}{S ⊢ seq(⊘) : Ok}

\frac{S ⊢ D :: S′ S, S′ ⊢ a : A}{S ⊢ seq(D, x = a) : A}

\frac{S ⊢ D :: S′ S, S′ ⊢ a : A}{S ⊢ seq(D, x : A = a) : A}

\frac{S ⊢ D :: S′ S, S′ ⊢ A type}{S ⊢ seq(D, X = A) : Ok}

[Value variant project] [Value variant test] [Value record dot]

[Value extend] [Value exception]

[Value seq empty]

[Value seq ide] [Value seq ide restrict]

[Value seq Ide]

[Value seq Ide restrict]

\frac{S ⊢ D :: S′ S, S′ ⊢ B <: A}{S ⊢ seq(D, X <: A = B) : Ok}

[Value if]

\frac{S ⊢ a : Bool S ⊢ b : B S ⊢ b′ : B}{S ⊢ if(a, b, b′) : B}

[Value case]

S ⊢ a : Tup(S′; Case(z′_{1}, S_{1}) … Case(z′_{m}, S_{m}))

S ⊢ b : B

S, y_{i} : Tup(S′, S′′; Case(?, ⊘)) ⊢ b_{i} : B 0 ≤ n i = 1 … n

S, S′ ⊢ S′′ <:: S_{z_{ij}} j = 1 … k_{i}

⋃_{i=1}^{n} ⋃_{j=1}^{k_{i}} z_{ij} ⊆ ⋃_{l=1}^{m} z′_{l} z_{ij} ≠ z_{i′j′} i ≠ i′, j ≠ j′

S ⊢ case(a, (z_{11} … z_{1k_{1}}, y_{1}, b_{1}) … (z_{n1} … z_{nk_{n}}, y_{n}, b_{n}), b) : B

[Value case exhaustive]

S ⊢ a : Tup(S′; Case(z′_{1}, S_{1}) … Case(z′_{m}, S_{m})) S, y_{i} : Tup(S′, S′′; Case(?, ⊘)) ⊢ b_{i} : B 1 ≤ n i = 1 … n

S, S′ ⊢ S′′ <:: S_{z_{ij}} j = 1 … k_{i}

⋃_{i=1}^{n} ⋃_{j=1}^{k_{i}} z_{ij} = ⋃_{l=1}^{m} z′_{l} z_{ij} ≠ z_{i′j′} i ≠ i′, j ≠ j′

S ⊢ case(a, (z_{11} … z_{1k_{1}}, y_{1}, b_{1}) … (z_{n1} … z_{nk_{n}}, y_{n}, b_{n})) : B

[Value loop]

\frac{S ⊢ a : Ok}{S ⊢ loop(a) : Ok}

[Value exit]

\frac{⊢ S sig}{S ⊢ exit : Nok}

[Value while]

\frac{S ⊢ a : Bool S ⊢ b : Ok}{S ⊢ while(a, b) : Ok}

[Value for]

\frac{S ⊢ a : Int S ⊢ b : Int S, x : Int ⊢ c : Ok}{S ⊢ for(x, a, b, c) : Ok}

[Value try]

S ⊢ a : B
S ⊢ b : B
S ⊢ a_{i} : Exc(S_{i}) i = 1 … n 0 ≤ n

S, x_{i} : Tup(S_{i}; Case(?, ⊘)) ⊢ b_{i} : B i = 1 … n S ⊢ try(a, (a_{1}, x_{1}, b_{1}) … (a_{n}, x_{n}, b_{n}), b) : B

[Value raise]

\frac{S ⊢ a : Exc(S′) S ⊢ D :: S′}{S ⊢ raise(a, D) : Nok}

[Value reraise]

\frac{⊢ S sig}{S ⊢ reraise : Nok}

5.12 Restrictions

The rule [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.

References

Abadi et al. 1989: Abadi, M., Cardelli, L., Pierce, B. C., and Plotkin, G.D. Dynamic typing in a statically typed language. Digital Systems Research Center Reports 47, DEC SRC Palo Alto, Juni 1989.

Abadi et al. 1990: Abadi, M., Cardelli, L., Curien, P.-L., and Lévy, J.-J. Explicit substitutions. Digital Systems Research Center Reports 54, DEC SRC Palo Alto, Februar 1990.

Abadi et al. 1992: Abadi, M., Cardelli, L., Pierce, B., and Rémy, D. Dynamic typing in polymorphic languages. In Proceedings of the ACM SIGPLAN Workshop on ML and its Applications, Juni 1992.

Atkinson and Morrison 1988: Atkinson, M.P. and Morrison, R. Types, bindings and parameters in a persistent environment. In Atkinson, M.P., Buneman, P., and Morrison, R., editors, Data Types and Persistence, Topics in Information Systems. Springer-Verlag, 1988.

Brown and Rosenberg 1991: Brown, A.L. and Rosenberg, J. Persistent object stores: An implementation technique. In Proceedings of the Fourth International Workshop on Persistent Object Systems, Martha’s Vineyard, Massachusetts. Morgan Kaufmann Publishers, Januar 1991.

Burstall and Lampson 1984: Burstall, R. and Lampson, B. A kernel language for abstract data types and modules. In Semantics of Data Types, volume 173 of Lecture Notes in Computer Science. Springer-Verlag, 1984.

Cardelli and Mitchell 1989: Cardelli, L. and Mitchell, J.C. Operations on records. Digital Systems Research Center Reports 48, DEC SRC Palo Alto, August 1989.

Cardelli et al. 1991: Cardelli, L., Martini, S., Mitchell, J.C., and Scedrov, A. An extension of system F with subtyping. In Ito, T. and Meyer, A.R., editors, Theoretical Aspects of Computer Software, TACS’91, Lecture Notes in Computer Science, pages 750–770. Springer-Verlag, 1991.

Cardelli 1989: Cardelli, L. Typeful programming. Digital Systems Research Center Reports 45, DEC SRC Palo Alto, May 1989.

Cardelli 1990: Cardelli, L. The Quest language and system (tracking draft). Digital Systems Research Center, DEC SRC Palo Alto, 1990. (shipped as part of the Quest V.12 system distribution).

Cardelli 1992a: Cardelli, L. Extensible records in a pure calculus of subtyping. Digital Systems Research Center Reports 81, DEC SRC Palo Alto, Januar 1992.

Cardelli 1992b: Cardelli, L. F-sub, the system. Digital systems research center, DEC SRC Palo Alto, Februar 1992. (shipped as part of the Fsub 1.4 system distribution).

Connor et al. 1991: Connor, R., McNally, D., and Morrison, R. Subtyping and assignment in database programming languages. In Database Programming Languages: Bulk Types and Persistent Data, pages 363–382, Nafplion, Greece, 1991. Morgan Kaufmann Publishers. de Bruijn 1972: de Bruijn, N.G. Lambda-calculus notation with nameless dummies: a tool for automatic formula manipulation with application to the Church-Rosser theorem. Indag. Math., 34(5):381–392, 1972.

Dearle et al. 1989: Dearle, A., Connor, R., Brown, F., and Morrison, R. Napier88 – a database programming language? In Proceedings of the Second International Workshop on Database Programming Languages, Salishan, Oregon, Juni 1989.

MacQueen et al. 1986: MacQueen, D.B., Plotkin, G.D., and Sethi, R. An ideal model for recursive polymorphic types. Information and Control, 71:95–130, 1986.

Matthes and Schmidt 1991a: Matthes, F. and Schmidt, J.W. Bulk types: Built-in or add-on? In Proceedings of the Third International Workshop on Database Programming Languages, Nafplion, Greece. Morgan Kaufmann Publishers, September 1991. (also appeared as TR FIDE/91/27).

Matthes and Schmidt 1991b: Matthes, F. and Schmidt, J.W. Towards database application systems: Types, kinds and other open invitations. In Proceedings of the Kiev East/West Workshop on Next Generation Database Technology, volume 504 of Lecture Notes in Computer Science, April 1991.

Matthes et al. 1991: Matthes, F., Ohori, A., and Schmidt, J.W. Typing schemes for objects with locality. In Proceedings of the Kiev East/West Workshop on Next Generation Database Technology, volume 504 of Lecture Notes in Computer Science, April 1991. (also appeared as TR FIDE/91/12).

Matthes 1992: Matthes, F. Generic Database Programming: A Linguistic and Architectural Framework. PhD thesis, Fachbereich Informatik, Universität Hamburg, Germany, September 1992. (in German).

Morrison et al. 1987: Morrison, R., Atkinson, M.P., and Dearle, A. Flexible incremental bindings in a persistent object store. Persistent Programming Research Report 38, Univ. of St. Andrews, Dept. of Comp. Science, Juni 1987.

Ohori et al. 1989: Ohori, A., Buneman, P., and Breazu-Tannen, V. Database programming in Machiavelli – a polymorphic language with static type inference. In Proceedings of the ACM-SIGMOD International Conference on Management of Data, Portland, Oregon, pages 46–57, 1989.

Ohori 1989: Ohori, A. A Study of Semantics, Types and Languages for Databases and Object-Oriented Programming. PhD thesis, University of Pennsylvania, 1989.

Pierce 1992: Pierce, B. C. Bounded quantification is undecidable. In Proceedings of the Nineteenth ACM Symposium on Principles of Programming Languages, pages 305–315, Januar 1992.

Rémy 1991: Rémy, D. Type inference for records in a natural extension of ml. Rapport de Recherche 1431, INRIA, Domaine de Voluceau Rocquencourt 78153 Le Chesnay Cedex - France, May 1991.

Schmidt and Matthes 1991: Schmidt, J.W. and Matthes, F. Naming schemes and name space management in the DBPL persistent storage system. In Proceedings of the Fourth International Workshop on Persistent Object Systems, Martha’s Vineyard, Massachusetts. Morgan Kaufmann Publishers, Januar 1991.

Schröder and Matthes 1992: Schröder, G. and Matthes, F. Using the Tycoon compiler toolkit. DBIS Tycoon Report 061-92, Fachbereich Informatik, Universität Hamburg, Germany, May 1992.

Solomon 1978: Solomon, M. Type definitions with parameters. In Proceedings of the Fifth ACM Symposium on Principles of Programming Languages, Tucson, Arizona, pages 31–38, Januar 1978.

Stansifer 1988: Stansifer, R. Type inference with subtypes. In Proc. 15th ACM Symposium on Principles of Programming Languages, pages 88–97, 1988.

Wand 1987: Wand, M. Complete type inference for simple objects. In Proceedings of the Second Annual Symposium on Logic in Computer Science, pages 37–44, Ithaca, New York, Juni 1987.