Type-system extensions for object-oriented language based on coercive subtyping with restrictions

[0001] This application is related to co-pending U.S. patent application Ser. No. 10/903,761 entitled “COMPOSITIONAL LIFTING OF OPERATIONS OVER STRUCTURAL TYPES” filed on Jul. 30, 2004.

[0002] This invention is related to object-oriented (OO) languages, and more specifically, to data access using an OO language.

[0003] Programming languages need to continuously evolve to help programmers cope with complicated applications. These evolutionary steps are typically quite modest; most commonly, the provisioning of better or reorganized APIs (Application Program Interfaces). Occasionally, a more radical evolutionary step is taken. One such example is the addition of generic classes to languages such as both Java and C^#.

[0004] The time has come, however, for another large evolutionary step to be taken. Much software is now intended for distributed, web-based scenarios. It is typically structured using a three-tier model consisting of a middle tier containing the business logic that extracts relational data from a data services tier (a database) and processes it to produce semi-structured data (typically XML-eXtensible Markup Language) to be displayed in the user interface tier. These middle tier applications are most commonly written in an object-oriented language such as Java or C^# and have to deal with relational data (essentially SQL (Structured Query Language) tables), object graphs, and semi-structured data (e.g., XML, HTML).

[0005] Unfortunately support for such data access has barely evolved at all. All that exists is naive access via simple APIs. Consider the following fragment of Java that uses JDBC (Java DataBase Connectivity—which is an API that lets a Java application access a database via SQL) to query a SQL database (the user-supplied country is stored in variable input).

[0006] Connection con=DriverManager.getConnection( . . . );

[0007] Statement stmt=con. createconnection( );

[0008] String query=“SELECT * FROM COFFEES WHERE Country=‘“+input+” ’”;

[0009] ResultSet rs=stmt.executeQuery(query);

[0010] while (rs.next( )) {

[0011] String s=rs.getString(“Cof_Name”);

[0012] float n=rs.getFloat (“Price”);

[0013] System.out.println(s+“-”+n>;

}

[0014] Using strings to represent SQL queries is not only clumsy but also removes any possibility for static checking. The impedance mismatch between the language and the relational data is quite striking; e.g., a value is projected out of a row by passing a string denoting the column name and using the appropriate conversion function. Perhaps most seriously, the passing of queries as strings is often a security risk (the “script code injection” problem—e.g., consider the case when the variable input is the string “'OR 1=1 −”.

[0015] The future of e-commerce is largely dependant on development of what are referred to as Web Services, which are Internet-based APIs that provide valuable functions or services for users. For example, Microsoft Passport® is a Web Service that facilitates user interaction by transferring user profile information to designated websites. The broad idea behind Web Services is to loosely couple heterogeneous computer infrastructures together to facilitate data transmission and computation to provide the user with a simple yet powerful experience.

[0016] A significant component in functionality of Web Services is programmatic interaction with web data. However, the world of web data is presently quite disjunctive. In general, there are three major components that make up the world of web data relational data (e.g., SQL), semi-structured data (e.g., XML), and a runtime environment. FIG. 1 illustrates a Venn diagram 100 that depicts a conventional web data world. A popular method of implementing a relational data model is by means of SQL that facilitates accessing data of a relational database system which is typically stored in tables. An accepted standard for semi-structured data is XML. XML is a World Wide Web Consortium (W3C) standard language that describes data via a schema or Document Type Definition (DTD). XML data is stored through the use of tags. A runtime environment is a general-purpose multilanguage execution engine (e.g., Common Language Runtime (CLR)) that allows authors to write programs that use both relational data and self-describing data.

[0017] However, in common with the situation with relational data access, there is also an impedance mismatch between looseness of the “document world” from which XML evolved, and a more structured world of object-oriented (OO) programming languages, which dominate the applications world. Bridging these two worlds today is conventionally accomplished by employing specialized objects that model the XML world called “XML Document Object Model,” or by “XML Serialization” technologies, which intelligently map one world into the other at runtime. However, these bridging mechanisms are often cumbersome and/or limited in functionality.

[0018] Object-oriented languages like C++, Java, and C# provide a way of defining classes and/or structs, and then constructing instances of those types via “constructors” using the “new” operator. The objects being constructed and the arguments being passed to the constructors are all strongly typed. These languages usually also provide convenience mechanisms for initializing simply homogeneous arrays of objects. These constructs are designed to make programs written in these languages run fast.

[0019] XML, on the other hand, provides syntax for describing heterogeneous graph(s) of data where typing rules (usually called “schema validation”) are entirely optional and loosely bound to those type instances. Furthermore, the XML schemas associated with those documents can describe more complex structures with sequences, choices, unbounded type collections, and a combination of typed and untyped data using constructs like <xsd:any/> and <xsd:anyAtrribute/>. These constructs are designed to allow a loosely coupled architecture that minimizes hard dependencies between different parties that make up a complex distributed system and have proven to be the only way to make distributed systems scale up to a level of complexity required for today's interconnected business systems.

[0020] Seamless integration of data-access in an OO host language is an extremely tricky problem and many people have attempted to solve this problem in the past with varying degrees of success. At the heart of the problem are three different and distinct type systems: the semi-structured XML that is used to describe data elements on web page and business-to-business documents; the SQL language, that is used to interrogate and process data in a relational database; and, the CLR, which are OO services and security services that applications can use.

[0021] Dealing with the complexity of these disparate models is a major pain for programmers today, since mainstream programming languages like C, C++, VB, C#, or Java simply do not know anything about relational or semi-structured data, yet programmers need to deal with all three data models at once.

[0022] Most programming languages do not provide an integrated view of these three worlds, but typically provide a “hands off” API to access one domain from the other. However, data integration via APIs has reached its limits. Alternatively, various methods of so-called data-binding have been explored where concepts from an XML or relation world are mapped onto the OO world. However, without type-system and language extensions these attempts will only be of limited value because of the size of the impedance mismatch they are attempting to bridge.

[0023] Unfortunately API support in both Java and C# for XML and XPath/XQuery is depressingly similar. XPath has been widely used in the XML community as a query language to navigate and retrieve from an XML data source. Furthermore, XQuery uses XPath as its query language to retrieve data from an XML data source.

[0024] Due to the increasingly complex nature of software systems, programmers have been riddled by undetectable programmatic errors that oftentimes do not manifest until too late. Developers continue to try to expand power of programming languages by incorporating complex mathematical and philosophical concepts. Additionally, the software market is becoming increasingly platform independent and service oriented. Combining powerful object-oriented programmatic concepts into the new data centric and service based world causes programmers problems as they try and piece together best parts of a multitude of different technologies in an ad hoc fashion.

[0025] Type systems are a formal mechanism for ensuring that typed programs perform correctly and in a well-behaved manner. Typed programs or typed systems are generally programs or systems that assign types to variables (e.g., Boolean, integer, real, etc.) or objects. Types are classifications of data that describe how a programmer wants to use the data and how a compiler should interpret such data. However, many functions are only defined to work on particular types (e.g. integer addition or floating point addition). If a given function is defined to work with a certain data type and it receives a different type of data, a type error will be produced. A type system can prevent certain execution errors by utilizing a type-checking algorithm to determine whether a program is well behaved or ill behaved. This process is referred to as type checking. Type checking allows for early detection and therefore correction of errors that may often go undetected by programmers. If such errors are left uncorrected they may lurk in the code, only to become manifestly obvious at a most inopportune time.

[0026] In general there are two varieties of type systems—nominal and structural. A nominal type system is a system in which type names are used to determine whether types are equivalent. In a structural type system, names are not essential, because types are said to be equivalent if they have the same structure, as the name suggests. For example assume Type A=string of integers (1 . . . 10) and Type B=string of integers (1 . . . 10). Further assume that a is of Type A, b is of Type B, and the expression a=b is written into the same program. Under a nominal type system this expression would produce an error because a and b are of different types. Under a structural type system such an assignment would be legal because the types are equivalent.

[0027] There is an unmet need for common OO languages to evolve to support data access associated the rich structure of both relational and semi-structured data.

[0028] The following presents a simplified summary of the invention in order to provide a basic understanding of some aspects of the invention. This summary is not an extensive overview of the invention. It is not intended to identify key/critical elements of the invention or to delineate the scope of the invention. Its sole purpose is to present some concepts of the invention in a simplified form as a prelude to the more detailed description that is presented later.

[0029] The present invention disclosed and claimed herein, in one aspect thereof, comprises a type system that provides seamless integration of data-access in an object-oriented (OO) host language. The invention provides a type-system that works with a corresponding set of syntactic constructions to extend the OO paradigm to encompass semi-structured and relational data. The syntactic extensions are compiled via a type-directed translation method that lifts member-access on base types to the newly introduced types.

[0030] In another aspect of the present invention, the core language of the type system includes nominal types, discriminated unions, tuple types, intersection types, anonymous delegate types, streams, and array types.

[0031] In yet another aspect thereof, covariance is restricted to identity conversions.

[0032] In still another aspect of the present invention, congruence relationships are defined for certain types that induce an equivalence relation on the types. This allows the same underlying type to be denoted by a different type expression.

[0033] In another aspect of the present invention, the type system includes updates by introducing a type constructor of 1-values.

[0034] In another aspect thereof, generic classes are supported through the use of stratification. By way of a kind system, the types are partitioned into different buckets to prevent problematic instantiations. The partitions can be at different granularities.

[0035] To the accomplishment of the foregoing and related ends, certain illustrative aspects of the invention are described herein in connection with the following description and the annexed drawings. These aspects are indicative, however, of but a few of the various ways in which the principles of the invention can be employed and the present invention is intended to include all such aspects and their equivalents. Other advantages and novel features of the invention will become apparent from the following detailed description of the invention when considered in conjunction with the drawings.

[0050] The present invention is now described with reference to the drawings, wherein like reference numerals are used to refer to like elements throughout. In the following description, for purposes of explanation, numerous specific details are set forth in order to provide a thorough understanding of the present invention. It may be evident, however, that the present invention can be practiced without these specific details. In other instances, well-known structures and devices are shown in block diagram form in order to facilitate describing the present invention.

[0051] As used in this application, the terms “component” and “system” are intended to refer to a computer-related entity, either hardware, a combination of hardware and software, software, or software in execution. For example, a component can be, but is not limited to being, a process running on a processor, a processor, an object, an executable, a thread of execution, a program, and/or a computer. By way of illustration, both an application running on a server and the server can be a component. One or more components can reside within a process and/or thread of execution, and a component can be localized on one computer and/or distributed between two or more computers.

[0052] As used herein, the term to “infer” or “inference” refer generally to the process of reasoning about or inferring states of the system, environment, and/or user from a set of observations as captured via events and/or data. Inference can be employed to identify a specific context or action, or can generate a probability distribution over states, for example. The inference can be probabilistic—that is, the computation of a probability distribution over states of interest based on a consideration of data and events. Inference can also refer to techniques employed for composing higher-level events from a set of events and/or data. Such inference results in the construction of new events or actions from a set of observed events and/or stored event data, whether or not the events are correlated in close temporal proximity, and whether the events and data come from one or several event and data sources.

[0053] Referring now to FIG. 2, there is illustrated a block diagram of a system 200 that employs a data access component 202 that facilitates seamless data access of both semi-structured and relational data in an runtime environment 208 (e.g., object-oriented (OO)), in accordance with the present invention. The runtime environment 208, inter alia, compiles high level programming languages into machine instructions that can subsequently be executed by a processor. As illustrated, the present invention describes a language solution to bridge technological gaps rather than utilizing APIs (Application Programming Interfaces), like conventional technologies. The language solution integrates the worlds of relational data (e.g., SQL-Structured Query Language), semi-structured data (e.g., XML-eXtensible Markup Language), and the runtime environment 208 (e.g., CLR (Common Language Runtime) or JVM (Java Virtual Machine)) to present a coherent and unified interface to all three worlds. The amalgamation of worlds is accomplished by delving deeper than APIs and building a unified extended type system. Thus, the present invention facilitates incorporating some of the best features of many present day languages into a single cohesive language.

[0054] There exists semi-structured data 204 and relational data 206 for accessing by the runtime environment 208. Such interaction is desired in the conventional web data world. A popular method of implementing a relational data model 206 is by means of SQL that facilitates accessing data of a relational database system which is typically stored in tables, and an accepted standard for the semi-structured data 204 is XML. The OO runtime environment 208 allows an author to write programs that use both relational data and self-describing data.

[0055] Bridging the conventional impedance mismatch between the runtime environment 208 and both the semi-structured data 204 and the relational data 206 is the novel data access component 202, which includes a type system 210 and associated syntactic constructions 212 to facilitate seamless interaction therebetween in accordance with the present invention.

[0056] It is to be appreciated that the disclosed type system 210 and associated constructions 212 support independent interaction of the data sources (204 and 206) with the runtime environment 208, such that it is not required that both the data sources (204 and 206) be accessible to facilitate all interactions.

[0057] Referring now to FIG. 3, there is illustrated a type system 300 that provides relational and semi-structured data access in accordance with the present invention. While, for purposes of simplicity of explanation, the one or more methodologies shown herein, e.g., in the form of a flow chart, are shown and described as a series of acts, it is to be understood and appreciated that the present invention is not limited by the order of acts, as some acts may, in accordance with the present invention, occur in a different order and/or concurrently with other acts from that shown and described herein. For example, those skilled in the art will understand and appreciate that a methodology could alternatively be represented as a series of interrelated states or events, such as in a state diagram. Moreover, not all illustrated acts may be required to implement a methodology in accordance with the present invention.

[0058] At 302, the system 300 restricts covariance to identity conversions on the underlying element type. At 304, the system 300 defines a number of type congruencies between types that induce an equivalence, instead of using mutual convertibility. This allows the same underlying type to be denoted by a different type-expression. At 306, the system 300 provides type-directed lifting of member access and/or operators. At 308, the system 300 provides type-directed lifting of a receiver and/or some or all of the arguments. At 310, the system, 300 provides updates. At 312, the system 300 provides a “kind” system that facilitates stratification of types into different kinds.

[0059] Referring now to FIG. 4, there is illustrated core structural types 400 of the type system of the present invention. The core types 400 include nominal types 402, discriminated unions 404, tuple types 406, intersection types 408, anonymous delegate types 410, streams 412, and array types 414.

[0060] Referring now to FIG. 5, there is illustrated a table of types 500 that facilitate data access in accordance with the present invention. The types are defined by the following abstract syntax:

[0061]

	T : := N	nominal type
	| T [ ]	array with elements of type T
	| either{. . . ;L; . . . }	disjoint union
	| struct{. . . ;L; . . . }	labeled tuple
	| all {. . . ;L; . . . }	intersection
	| definitely<T>	non-null
	| maybe<T>	possibly null
	| sequence<T>	stream
	| delegate T( . . . , T, . . . )	anonymous delegate
	L : := T | T m	optionally labeled member

[0062] Referring now to FIG. 6, there is illustrated a table of operations 600 that can be applied to the types 500 of FIG. 5 to facilitate data access in accordance with the present invention. The operations on these types are defined by the following abstract syntax:

[0063]

	E : := e.f	normal field access
	| e . . . f	transitive field access
	| e.m( . . . , e, . . . )	method call
	| e.f( . . .  . , e, . . .  . )	delegate invocation
	| e. {s}	apply-to-all
	| e[e]	filter
	| new (N) ( . . . , (m:=)e, . . . )	construction

[0064] Note that the concrete syntax for these types and the set of operations can be different in any actual programming language that embodies the described invention.

[0065] Nominal types N are existing types such as value types, reference types, interfaces or (nominal) delegates that are either built-in or defined using some mechanism for introducing nominal types, e.g., class, value type, interface or delegate declarations:

[0066] class Point{int x; int y;}

[0067] class Punt{int x; int y;}

[0068] delegate int F(int n)

[0069] struct Person{string Name; int Age;}

[0070] Nominal types are called nominal because the equivalence and subtype relationship between these types is determined by their (fully qualified) name. For instance, while the types Point and Punt above both contain exactly the same members and hence, are structurally the same, they are considered as different types by the type system because they have a different declared name. The subtype relationship between nominal types is also determined from their declaration/name. For example, given a derived type ColorPoint defined as,

[0071] class ColorPoint: Point{Color color;}.

[0072] An implicit reference conversion is automatically obtained between ColorPoint and Point, which is written as ColorPoint <: Point→id. In general, the subtype relation is written S<: T→f, meaning that S is a subtype of T and f is a witness that coerces a value of type S to a value of type T.

[0073] Array types are also standard, but in contrast to nominal type, the equivalence of arrays is determined by their structure, a new array type is not declared each time one is used. For example, using the type Point[ ] in one program is the same as another use of the type Point[ ] as long as the two types Point are the same. Subtyping on arrays is covariant, which means that if the element types of two arrays are in a subtype relation, the two arrays created from these types are also in a subtype relation. A property of the covariance of arrays is that it is restricted to identity conversions on the underlying element type. This is written using the following rule:

[0074] $\frac{S<:T\mathrm{id}}{S\left[\right]<:T\left[\right]\mathrm{id}}$

[0075] The new types described herein are structural types such as discriminated unions, tuple types, intersection types, streams, and anonymous delegate types. The associated structural properties are defined next. In addition to subtype relationships between types, a number of type congruencies (≡) are introduced between types that induce an equivalence relation on types. This allows the same underlying type to be denoted by a different type-expression.

[0076] The value type tuple type struct { . . . ;T m_opt; . . . } is a heterogeneous ordered finite collection of optionally labeled members. For example, values of type struct{bool; int x; char c;} are triples containing an unlabeled Boolean, an integer labeled x, and a character labeled c.

[0077] Tuple types are covariant, provided the corresponding conversion on the members is an identity conversion

[0078] $\frac{\dots S<:T\mathrm{id}\dots }{\mathrm{struct}\left\{\dots ;Sm;\dots \right\}<:\mathrm{struct}\left\{\dots ;Tm;\dots \right\}}$

[0079] The members of a tuple type can be accessed by position, or when they are labeled by their label. For example, given a value s of the example tuple type, its members can be accessed using the following expressions:

[0080] struct{bool; int x; char c;} s=new(true, x=4711; c=‘a’);

[0081] bool b=s[0];

[0082] char d=s.c;

[0083] int y=s.x;

[0084] All label-based access on tuple types can be translated into positional access via a type-directed translation. This is especially relevant when member access is lifted over tuple types. For example, given a nested tuple type, the members of the nested inner struct can still be transparently accessed from the outer one

[0085] struct {

[0086] Button b;

[0087] struct{bool; int x; char c;};

[0088] } ns;

[0089] char d=ns.c; // ns[1].c, or ns[1] [2]

[0090] Note that while the tuple type has no direct member labeled c, the member c of the nested struct can be transparently accessed. The compiler uses the static type of the receiver ns in the expression ns.c to determine how to access the member c.

[0091] The types definitely<T>, maybe<T>, and sequence<T> denote streams of values, and are flattened. That is, the following types are considered equivalent:

[0092] definitely<definitely<T>>≡definitely<T>

[0093] definitely<maybe<T>>≡definitively<T>

[0094] definitely<sequence<T>>≡sequence<T>

[0095] maybe<definitely<T>>≡maybe<T>

[0096] maybe<maybe<T>>≡maybe<T>

[0097] maybe<sequence<T>>≡sequence<T>

[0098] sequence<definitely <T>>≡sequence<T>

[0099] sequence<maybe<T>>≡sequence<T>

[0100] sequence<sequence<T>>≡sequence<T>

[0101] Note that this kind of equivalence of types is usually implicit in other languages such as Java or C#. For example, in C#, the following two type declarations class C: IA, IB { } and class C: IB, IA { } are considered equivalent, i.e., class C: IA, IB { }≡class C: IB, IA { }.

[0102] Flattening of streams also works when there is an intervening either type.

[0103] definitely<either{definitely<either{ . . . }>; . . . }>≡

[0104] definitely<either{ . . . ; . . . }>

[0105] definitely<either{maybe<either{ . . . }>; . . . }>≡maybe<either{ . . . ; . . . }>

[0106] definitely<either{sequence<either{ . . . }; . . . }>≡sequence<either{ . . . ; . . . }>

[0107] maybe<either{definitely<either{ . . . }>; . . . }>≡maybe<either{ . . . ; . . . }>

[0108] maybe<either{maybe<either{ . . . }; . . . }>≡maybe<either{ . . . ; . . . }>

[0109] maybe<either{sequence<either{ . . . }>; . . . }>≡sequence<either{ . . . ; . . . }>

[0110] sequence<either{definitely<either{ . . . }>; . . . }>≡sequence<either{ . . . ; . . . }>

[0111] sequence<either{maybe<either{ . . . }>; . . . }>≡sequence<either{ . . . ; . . . }

[0112] sequence<either{sequence<either{ . . . }; . . . }>≡sequence<either{ . . . ; . . . }>

[0113] The stream types form the following hierarchy, where the conversions definitively<T> <: T and T <: maybe<T> are not identity conversions.

[0114] definitively<T> <: Tunwrap_definitely

[0115] T <: maybe<T>wrap_mayby

[0116] maybe<T> <: sequence<T>id (or alternatively a non-identity conversion wrap_sequence)

[0117] Stream types are covariant, provided again that the conversion on the underlying type is the identity for sequence and definitely. It is possible to allow a non-identity conversion for maybe.

[0118] $\frac{S<:T\mathrm{id}}{\mathrm{definitely}<S><:\mathrm{definitely}<T>\mathrm{id}}$ $\frac{S<:T\mathrm{id}\left(\mathrm{or}a\mathrm{nonidentity}\mathrm{conversion}f\right)}{\begin{array}{c}\mathrm{maybe}<S><:\mathrm{maybe}<T>\\ \mathrm{id}\left(e->e.\left\{\mathrm{return}f\left(\mathrm{it}\right);\right\}\right)\end{array}}$ $\frac{S<:T\mathrm{id}}{\mathrm{sequence}<S><:\mathrm{sequence}<T>\mathrm{id}}$

[0119] Member access is lifted over stream types. For example, given a stream of type sequence<Button> bs, the BackColor of each button can be selected in the stream using bs.BackColor. The compiler translates this into an explicit apply-to-all operation bs.{return it.BackColor;}. For definitely <T>, it is a little different. If definitely<Button> bs, then bs.BackColor has type Color, and translated into ((Button)bs).BackColor.

[0120] Binary (and unary) operators are also lifted over maybe and sequence.

[0121] $\frac{T\left(T,T\right)}{\mathrm{sequence}<T>\left(\mathrm{sequence}<T>,\mathrm{sequence}<T>\right)}$ $\frac{T\left(T,T\right)}{\mathrm{maybe}<T>\left(\mathrm{maybe}<T>,\mathrm{maybe}<T>\right)}$

[0122] The lifted operation applies the operation (¤) pairwise to each element in the argument streams.

[0123] The typing rules and syntax directed translation of all types except all{ } and delegate are described in detail herein.

[0124] An extension of this system is by the notion of 1-values and updates. Updates are an aspect of imperative programming. Current XML-based languages (e.g., XQuery, XDuce, and Xtatic) lack support for updates. Moreover, conventional languages (e.g., XJ) restrict 1-values to be singletons.

[0125] The disclosed invention allows updates where 1-values are arbitrary structured types. Updating is achieved by introducing a new type-constructor of 1-values of type T, written T, and defining a similar notion of lifting on 1-values. An assignment expression e1=e2 then applies the 1-value translation to e1, which results in a translated expression e1′ of type T, and the r-value translation to e2, which results in a translated expression e2 of some type S, where S <: Tf and then the r-value f(e2′) is assigned to the 1-value e1′.

[0126] The extension of this type-system uses generics. The type system described thus far does not support the construction of user-defined generic classes such as,

[0127] class Pair<A,B> {public A first; public B second;}.

[0128] More details on generics in general, is available in the C# language specification.

[0129] Consider an interaction between generics and the disclosed type systems. Define the following class Foo<A> as,

[0130] class Foo<A>{public maybe<A> a;}.

[0131] A problem is that when the type of the type-parameter A is unknown, no determination can be made of the type of the result of accessing the a member of an instance fa of the generic type Foo. Depending on what A is, the result type of fa.a can be sequence<B>, for example, when a is bound to sequence<B>, or maybe<C> when A is bound to either definitely<c> or maybe<C>.

[0132] This problem is solved by stratifying the type-system into several layers to prevent problematical instantiations like the above. One way to achieve such a stratification is by introducing a “kind” system for types, i.e., by partitioning types into different buckets. This partitioning can be at different granularities. For example, all types could be divided into two buckets; types that are not subject to congruencies; and,

[0133] types that are subject to congruencies. Type variables are restricted in types that are subject to congruencies to only types that are not subject to congruencies. Given the above example, it then follows that,

[0134] Foo<int>→OK

[0135] Foo<Foo<int>>→OK

[0136] Foo<sequence<int>>→Wrong, since sequence<int> is subject to congruences

[0137] In this way it can always be determined by looking at the structural types in isolation what congruencies apply.

[0138] In one sample implementation of stratification, a first level includes base types, int, float, class types, and a button string. A second level can include either or struct, that have component types of base types or the same level. A third level can include maybe, sequence, and definitely. A fourth level can include constraints for generic classes.

[0139] Referring now to FIG. 7, there is illustrated a block diagram of a system 700 that includes a runtime environment 702 that facilitates multi-data access in accordance with the present invention. The runtime environment 702 is operable to run one or more programs, here, a first program 704 (denoted PROGRAM₁) and a second program 706 (denoted PROGRAM₂). Each of the first and second programs (704 and 706) can be written by a different programming language. That is, the first program 704 can be written according to a first programming language 708 (also denoted PROGRAMMING LANGUAGE₁) and the second program 706 can be written according to a second programming language 710 (also denoted PROGRAMMING LANGUAGE₁). Given that the programming languages (708 and 710) are different, each employs a different type system where necessary to access the data sources. Thus, the first programming language 708 employs a first type system 712 (also denoted TYPE SYSTEM₁) and the second programming language 710 employs a second type system 714 (also denoted TYPE SYSTEM₂).

[0140] The first program 704 can be written using the first type system 712 to process either relational query expressions 716 or semi-structured expressions 718. In contrast, the second program 706 can be written using the second type system 714 to process both relational query expressions 720 and semi-structured expressions 722. Both the first and second programs (704 and 706) can be executed in the same runtime environment 702 according to conventional program execution architectures.

[0141] It is to be appreciated that where the same programming language is used for both the first and second programs (704 and 706) a common type system can be used to facilitate data access of both the data sources. It is further to be appreciated that the disclosed type system is not restricted to only two data sources, but can be implemented with suitable types and constructions to interface with a third data source (not shown) or even a fourth data source (not shown) that is different from the first three.

[0142] The programming languages (708 and 710) are run on top of the runtime environment 702. The runtime environment 702, inter alia, provides services to the programming languages (708 and 710) such as automatic memory management, code security, and debugging facilities, which allows authors to focus on an underling logic of their applications rather than details of implementation. The first programming language 708 provides a vocabulary and set grammatical rules that authors can use to implement desired functionality of their applications. In one implementation, the first programming language 708 can be is a strongly typed object-oriented language that is tightly integrated with a compiler and the first type system 712. This allows programs to be thoroughly error checked prior to execution.

[0143] The first program 704 employs the vocabulary and grammatical rules of the first programming language 708 to develop an application. Once the first program 704 is written, it is compiled. The first program 704 can be compiled into an intermediate language (IL) or directly to machine code. A processor 724 can then execute the first program 704 via the runtime environment 702. The processor 724 can also interact with a storage 726 to facilitate execution of the first program 704.

[0144] The semi-structured expression(s) 718 can be a part of the first program 704. When employed in the first program 704, the semi-structured expressions 718 are utilized to retrieve semi-structured data 732 (e.g., XML literals or object instances from XML documents). The semi-structured expressions 718 allow navigation to and retrieval of data in an XML document, for example, similar to the approach taken by the W3C recommended XML Path Language (XPath).

[0145] Alternatively, the relational query expressions 716 can be a part of the first program 704, and are comprised of query terms, logical operators, and special characters that allow authors to specify how and which data is to be retrieved from a relational database 728. The relational database 728 can store massive amounts of data in the form of tables that can be accessed, retrieved, or otherwise manipulated programmatically. The processor 724 is operably connected to database management system (DBMS) 730, and retrieves data from relational database 728 by requesting information from the DBMS 730 via the relational query expressions 716.

[0146] In an alternative implementation to the first program 704, the second program 706 utilizes both the relational query expressions 720 and the semi-structured expressions 722, which facilitates accessing both the relational database 728 and the semi-structured documents 732 as provided by the second type system 714.

[0147] FIG. 8 illustrates an example of the lifting of member access/field properties in accordance with the present invention. It is called lifting since it lifts the operation on the underlying types to the constructed types.

[0148] FIG. 9 illustrates an example of the lifting of operators in accordance with the present invention.

[0149] FIG. 10 illustrates an example of the lifting of receivers in accordance with the present invention.

[0150] FIG. 11 illustrates an example of the lifting of some or all of the arguments in accordance with the present invention.

[0151] FIG. 12 illustrates an example of the lifting of receivers and some or all of the arguments in accordance with the present invention. The method includes two parameters Control and bool, of which only Control gets lifted. The following sample code represents what is happening in FIG. 12.

[0152] public Control GetNextControl (

• • [0153] Control ctl,
  • [0154] bool, forward

[0155] );

[0156] Coercive subtyping implies that there is a subtype relationship between types. If it is desired to transfer a value from a first type to a second type, nothing additional needs to be done if the first type is a subset of the second type. However, it is to be appreciated that sometimes the values are different. Thus, some work or conversion must be performed. For example, integers are a subtype real numbers. By representation, however, integers are 23-bit and floating point numbers are 64-bit. Thus, when converting from integer to floating point, a change in representation of the value occurs (i.e., coercive subtyping). Coercive subtyping is costly because of the change in representation involved. All of the subtyping should be inexpensive because all of the subtyping is implicitly convertible. Thus, there is point at which a decision is made as to whether to convert the values based on cost. There is a way to restrict subtyping of a complicated type based on some criteria on the subtyping of the component types.

[0157] In one implementation, a heuristic is employed to determine when to make the conversion based on the costs associated therewith.

[0158] In another implementation, artificial intelligence (AI) can be employed to analyze the cost and make the decision to convert. The subject invention can employ various AI-based schemes for carrying out various aspects thereof. For example, a process for determining the cost associated with a conversion can be facilitated via an automatic classifier system and process.

[0159] A classifier is a function that maps an input attribute vector, x=(x1, x2, x3, x4, xn), to a confidence that the input belongs to a class, that is, f(x)=confidence(class). Such classification can employ a probabilistic and/or statistical-based analysis (e.g., factoring into the analysis utilities and costs) to prognose or infer an action that a user desires to be automatically performed.

[0160] A support vector machine (SVM) is an example of a classifier that can be employed. The SVM operates by finding a hypersurface in the space of possible inputs, which hypersurface attempts to split the triggering criteria from the non-triggering events. Intuitively, this makes the classification correct for testing data that is near, but not identical to training data. Other directed and undirected model classification approaches include, e.g., naïve Bayes, Bayesian networks, decision trees, neural networks, fuzzy logic models, and probabilistic classification models providing different patterns of independence can be employed. Classification as used herein also is inclusive of statistical regression that is utilized to develop models of priority.

[0161] As will be readily appreciated from the subject specification, the subject invention can employ classifiers that are explicitly trained (e.g., via a generic training data) as well as implicitly trained (e.g., via observing user behavior, receiving extrinsic information). For example, SVM's are configured via a learning or training phase within a classifier constructor and feature selection module. Thus, the classifier(s) can be used to automatically perform a number of functions, including but not limited to determining according to a predetermined criteria when to make the conversion based on the cost of conversion, when to convert based on the type of values, and when to make the conversion based on the kind of data being processed.

[0162] Application to C# Programming Language

[0163] Following is a description of a lightweight extension of the popular object-oriented language C# in accordance with the present invention. Notable features include type-theoretic integration of the three prevalent data models in web-based applications, namely the object-oriented, relational, and semi-structured models of data. This is achieved by extending the class-based type system of C# with streams, particular forms of tuple and discriminated union types, and content types. The type system and the operational semantics are described. Although C# is the basis for this example application, the disclosed extensions apply equally well to other OO languages, including Java.

[0164] The disclosed extension to C#, hereinafter referred to as “Xen”, is a coherent extension of C#. This means that there is no redesign of C#, but rather the language is worked as it currently exists. Moreover, the extensions do not conflict in any way with the underlying language; C# programs should be valid Xen programs with the same behavior.

[0165] The type system of Xen is intended to be as simple as possible (in contrast with, for example, regular expression types), and to line up closely with the underlying execution environment, in our case the CLR.

[0166] From a programming perspective, the real power of Xen comes from its elegant and coherent query-like capabilities. These have been carefully designed to mimic existing query languages, in particular XQuery and SQL, as closely as possible. This principal has had the most profound effect upon the overall design of Xen.

[0167] Extensions to the type system-streams, tuple types, discriminated unions, and content classes—and for each are considered the new query capabilities.

[0168] The first structural type added is a stream type. For example, sequence<int> is the type for homogeneous sequences of integers. Streams in Xen are aligned with iterators. Thus, streams are generated lazily using iterator blocks and consumed using the foreach statement. For example, given a stream zones of type sequence<int>, the following statement prints each element in that stream:

[0169] foreach(int zone in zones) Console.WriteLine(zone);

[0170] C# member access is generalized to map over streams, e.g., zones.ToString( ) implicitly maps the call over the elements of the stream and returns a value of type sequence<string>. Another difference between iterators in C# is that streams in Xen are automatically flattened. Consider a type CD that contains a member zones of type sequence<int>. Then, given a stream cds of type sequence<CD>, all zones are converted to strings by writing cds.zones.ToString( ). In other words, member access has been generalized so that it behaves like a path expression. Thus, a design goal of Xen was to add XPath-like query expressions to C# in a lightweight and coherent way.

[0171] The second structural types added are tuple types. A tuple type is like a tuple, and is written as struct {int i; Button;}, for example. A value of this type contains a member i of type int and an unlabeled member of type Button. A value of this type can be constructed with the following expression: new (i=42, new Button ( )). To access components of tuple types, the notion of member access is generalized. Thus, assuming a value x of the previous type, x.i is written to access the integer value. Unlabeled members are accessed by their position; for example, x [1] returns the Button member. As for streams, member access is lifted over unlabelled members of tuple types. To access the Backcolor property of the Button component in variable x it can be written x.Backcolor, which is equivalent to x[1].Backcolor.

[0172] Xen also allows repeated occurrences of the same member name within a tuple type, even at different types. For example, assume the following declaration: struct{int i; Button; float i;} z; Then z.i projects the two i members of z into a new tuple type that is equivalent to new (z[0], z[2]) and the type struct{int; float;}.

[0173] The third structural type added is a particular form of discriminated union type, called an either type. This is written, for example, either {int; bool;}. As the name suggests, a value of this type is either an integer or a Boolean. Like unions, discriminated unions in Xen inherently know their type. Again, member access has been generalized over discriminated unions. As either types have a disjunctive flavor, stream types are used to handle the possibility that the element is not of the required type. Consider a discriminated union value w of type either{int; Button;}. An attempt can be made to access the color of w using the lifted member access expression w.Backcolor. This will return a value of type sequence<Color>, which is either a singleton stream containing the color value when w contains a Button, or the null pointer (the empty stream) when w happens to be an integer. Again, the path expression behavior is representative of XPath.

[0174] Content classes are the fourth type-system extension added to C#. A content class is a normal class that has a single unlabelled type that describes the content of that class. From an XSD (XML Schema Definition) perspective, classes correspond to global element declarations, while the content type of classes correspond to complex types.

[0175] These type extensions form the essence of Xen. While being quite simple they are in fact sufficiently powerful to represent both relational and semi-structured data. Relational tables are merely streams of tuple types. For example, the relational table created with the SQL declaration:

[0176] CREATE TABLE Customer (name string, custid int);

[0177] can be represented as the Xen declaration:

[0178] sequence<struct{string name; int custid}> Customer;

[0179] Similarly, the following XSD schema,

[0180] <element name=“Address”><complexType><sequence>

• • [0181] <choice>
    • [0182] <element name=“Street” type=“string”/>
    • [0183] <element name=“POBox” type=“int90/>
  • [0184] </choice>
  • [0185] <element name=“City” type=“string”/>

[0186] </sequence></complexType></element>

[0187] can be represented as the Xen content class declaration:

[0188] class Address {

• • [0189] struct{either{string Street; int POBox;}; string City;}
    }

[0190] Core Language of Xen-InnerXen

[0191] An InnerXen program consists of one or more class declarations. Each class declaration defines zero or more methods and contains exactly one unlabeled type that is called the content type (collections of field declarations can be encoded). A class declaration with a content type is called a content class. InnerXen follows C# and requires methods to be explicitly marked as virtual or override. Given a program, it is assumed that there is a unique designated method within the class declarations that serves as the entry point.

[0192]

	Program	p ::= cd
	Class Definition	cd ::= class c : c{ τ; md }
	Method Definition	md ::= virtual τm( τx ){ s }
		| override τm( τx ){ s }

[0193] InnerXen supports two main kinds of types: value types and reference types. As usual, the distinguished type void is used for methods that do not return anything. Value types include the base types bool and int and the structural types: tuple types and discriminated unions. Reference types are either class types or streams. As usual, only reference types have object identity and are represented at runtime by references into the heap. A designated special class object is assumed.

[0194]

	Types	τ::= γ	Value types
		| ρ	Reference types
		| void  | null	Void and null types
	Value Types	γ::= b	Base types
		| struct{ fd }	Tuple types
		| either{ fd }	Disjoint union types
	Base Types	b ::= bool  | int
	Reference Types	ρ ::= c	Classes
		| sequence<τ>	Stream types
	Field Definition	fd ::= τƒ;	Named member
		| τ,	Unnamed member

[0195] InnerXen expressions, as for C#, are split into ordinary expressions and promotable expressions. Promotable expressions are expressions that can be used as statements. A number of built-in primitive operators are assumed, such as ==, | | and &&. In the grammar, it is written e⊕e, where ⊕ denotes an instance of one of these operators.

[0196] Explanation of these expressions that are new for InnerXen is deferred hereinbelow to where the InnerXen type system is considered.

[0197]

Expression	e ::= b | i	Literals
	| e ⊕ e	Built-in operation
	| x	Variable
	| null	Null
	| (τ) e	Cast
	| e is τ	Dynamic typecheck
	| e was τ	Static typecheck
	| new τ(e)	Object creation
	| new τ( s )	Closure creation
	| new ( be )	Tuple type creation
	| new τ(τ′, e)	Discriminated union
		and internal stream
		element creation
	| e.ƒ	Field access by name
	| e[i]	Field access by position
	| pe	Promotable expression
Promotable expression	pe ::= x = e	Variable assignment
	| e.m( ē )	Method invocation
	| e. { s }	Apply-to-all
	| ( { s })	Block expression
Binding expression	be ::= ƒ = e	Named binding
	| e	Unnamed binding

[0198] Statements in InnerXen are standard. The yield statement is an updated version used to generate streams.

[0199]

Statement	s ::= ;	Skip
	| pe;	Promoted expression
	| if (e) s else s	Conditional
	| τx = e;	Variable declaration
	| return e;	Return statement
	| return ;
	| yield return e;	Yield statement
	| yield break ;	End of stream statement
	| foreach (τ x in e) s	Foreach loop
	| while (e) s	While loop
	| { s }	Block

[0200] In what follows, it is assumed that InnerXen programs are well-formed, e.g., no cyclic class hierarchies, correct method body construction, etc.

[0201] Static Semantics

[0202] In this section, the InnerXen type system is formalized and some of the new language features are described. The type system and language extensions are designed to be unobtrusive to the programmer, and things (i.e., member access over structural types) should work as expected. Additionally, the extension to subtyping is as close as possible to the spirit of host language. A goal of Xen is to keep the type system extensions few and as simple as possible.

[0203] Subtyping

[0204] Normally, subtyping is formalized by defining a relation between a subtype and a supertype. However, for the formalization of InnerXen, subtyping is treated as a coercion. Hence, the subtype relation is written τ<: τ′f meaning that τ is a subtype of τ′ and f is a witness that coerces a value of type τ to a value of type τ′. To be more precise, f is a context, i.e., code with a designated ‘hole’, usually written C[ ] such that when a code fragment v of type τ is placed in the hole, the resulting code, written C[v], is of type τ′. For succinctness, rather than writing contexts, a functional notation is used, e.g., x e. When no coercion is necessary (e.g., when converting from a subclass to a superclass), the identity function id, is written.

[0205] In fact, the typing judgments translate InnerXen constructs to a strictly smaller subset of the language, which is then evaluated by the operational semantics. However, to increase readability and avoid clutter, the syntactic sugar of (promotable) block expressions and apply-to-all expressions are sometimes used in the target of the translations. The rules that use such sugar are marked with an asterisk (*).

[0206] Subtyping in InnerXen is reflexive and transitive, so the following rules are immediate.

[0207] $\stackrel{\_}{\tau <:{\tau }^{\prime }\mathrm{id}}$ $\frac{\tau <:{\tau }^{\prime }f{\tau }^{\prime }<:{\tau }^{″}g}{\tau <:{\tau }^{″}e\mapsto g\left(f\left(e\right)\right)}$

[0208] Much of the previous work on using coercions to represent subtyping focuses on the problem of coherence, i.e., if there is more than one coercion between two types then they are observationally equivalent. Building upon C# and Java-coherence is too strong a condition. First, because some coercions are side-effecting, e.g., boxing, and so coherence can never hold. The second concerns how overloading is resolved (and interestingly is independent of the first). Consider the following overloaded method f.

[0209] void f (object x){Console.WriteLine(“Ha”);}

[0210] void f (Control x){Console.WriteLine(“Ha, Ha”);}

[0211] In both C# and Java, the call f (new Button ( ) prints Ha, Ha, even though both Button <: Controlid and Button <: Control <: objectid. This is because C# and Java determine that the first conversion is better. Since a design goal was to build directly upon C#, it is also assumed that given any two conversions τ<: τf and τ<: τ′g (where r may be equal to r) the better conversion of the two can be determined. Whenever subsumption is used (for assignments and method calls) the best conversion is chosen. For example, the assignment x=new Button ( ) injects into control when x has type either{Control; object;}.

[0212] Value Types. Following C# a value of any value type can be coerced to the supertype object. Doing so will box the value, place it on the heap, and return the heap reference. Thus, the coercion witness is not a pure function (boxing the same value twice will not return the same reference). The following rule covers the base types and tuple types. The case for discriminated unions is described later.

[0213] γ<: object e new γ(e)

[0214] Reference types. Two rules are provided. Firstly, a nominal class type c is a subtype of another class type c′ if c extends c′. Secondly, null is a subtype of any reference type.

[0215] $\frac{\mathrm{class}c:c^{\prime }}{c<:c^{\prime }\mathrm{id}}$ $\stackrel{\_}{\mathrm{null}<:\rho \mathrm{id}}$

[0216] Streams. Streams represent ordered homogeneous collections of zero or more values. In Xen, streams are most commonly generated by yield blocks. The following method From generates the infinite stream of integers n, n+1, . . . :

[0217] virtual sequence<int> From(int n){for (;;) yield return n++;}

[0218] Given a stream, iteration over its elements can be performed using a foreach statement. However, Xen offers a convenient shorthand called an apply-to-all expression written as e. { s} which applies the method-body { s} to each element it in the stream e. The variable it plays a similar role as the implicit receiver argument this in methods and is bound to each successive element of the iterated stream. For instance, the apply-to-all expression below will convert the stream of natural numbers from 0 into the stream of even numbers, converts each of these into a string, and then prints them all:

[0219] From(0).{return it*it;}.ToString( ).{Console.WriteLine(it);};

[0220] Block expressions are a lightweight way to define finite streams without the need to define a generator method. For instance, the following block expression generates a stream of two strings:

[0221] sequence<string> greeting=({

• • [0222] yield return “Hello”; yield return “World!”;

[0223] });

[0224] Generator block expressions are translated into closures. Streams are covariant provided that the conversion on the element type is the identity. The rationale for this is that implicit conversions should limited to constant-time operations. Coercing a stream of type sequence<int> to a stream of type sequence<object>, for example, would be linear in the length of the stream, as the boxing conversion from int to object is not the identity. Coercing a stream to the object type simply requires the identity witness.

[0225] $\frac{\tau <:{\tau }^{\prime }\mathrm{id}}{\mathrm{sequence}<\tau ><:\mathrm{sequence}<{\tau }^{\prime }>\mathrm{id}}$ $\stackrel{\_}{\mathrm{sequence}<\tau ><:\mathrm{object}\mathrm{id}}$

[0226] A feature of Xen is that streams are always flattened. Thus, Xen types are subject to the following equivalence.

[0227] sequence<sequence<τ>>≅sequence<τ>

[0228] Consequently, there are no streams of streams, and embedded empty streams disappear. Since null is equated to the empty stream, it follows also that element of streams are never null.

[0229] Flattening of stream types is essential to efficiently deal with recursively defined streams. Consider the following recursive variation of the function From that was defined previously:

[0230] virtual sequence<int> From(int n){

• • [0231] yield return n++; yield return From(n);

[0232] }

[0233] The recursive call yield return From(n); yields a stream forcing the type of From to be a nested stream. The non-recursive call yield return n++; yields a single integer thus forcing the return type of From to be a normal stream. As the type system treats the types sequence<int> and sequence<sequence<int>> as equivalent, this is type-correct.

[0234] Without flattening, it would be required to copy the stream produced by the recursive invocation, leading to a quadratic instead of a linear number of yields:

[0235] virtual sequence<int> From(int n){

• • [0236] yield return n++; foreach(int it in From(n)) yield return it;

[0237] }

[0238] Note that flattening of stream types does not imply that the underlying stream is flattened via some coercion; every element in a stream is yield-ed at most once. Iterating over a stream will effectively perform a depth-first traversal over the n-ary tree produced by the stream generators.

[0239] Tuple types. Tuple types encapsulate heterogeneous ordered collections of values. Members of tuple types can be labeled or unlabeled, and labels can be duplicated, even at different types. Members of tuple types can be accessed by label or by position.

[0240] Tuple types, as for streams, are covariant provided that the upcast-conversion that would be applied is the identity:

[0241] $\frac{\stackrel{\_}{\mathrm{fd}}<:\stackrel{\_}{{\mathrm{fd}}^{\prime }}\mathrm{id}}{\mathrm{struct}\left\{\stackrel{\_}{\mathrm{fd}}\right\}<:\mathrm{struct}\left\{\stackrel{\_}{{\mathrm{fd}}^{\prime }}\right\}\mathrm{id}}$

[0242] Subtyping respects field names: let fd, fd′ be τf, and τ′f′; then

[0243] $\left(\mathrm{fd}<:{\mathrm{fd}}^{\prime }\right)\stackrel{\mathrm{def}}{=}\left(f=f^{\prime }\bigwedge \tau <:{\tau }^{\prime }\right).$
If only one of fd or fd′ has a field name, the fields are incomparable. If fd and fd′ have no field name then field subtyping trivially reduces to subtyping.

[0244] Either types. A value of an either type is a discriminated union that may hold (at different times) any of the values of its members. Unlike unions in C/C++ and variant records in Pascal where users have to keep track of which type is present, values of an discriminated unions in Xen are implicitly tagged with the static type of the chosen alternative. In other words, discriminated union values are essentially a pair of a value and its static type. The special member e.value retrieves the value component of a discriminated union value e. The type component can be tested with the conformity test e was τ. The expression e was T is true for exactly one τ in τ. This invariant is maintained by the type system.

[0245] Like tuple types, the members of discriminated unions can be labeled or unlabeled. The following absorption rule states that a labeled member in a discriminated union is just a nested singleton tuple type:

[0246] either {τ f; fd′}≅either{struct {τf;}; fd′}

[0247] Discriminated unions are idempotent, commutative, and associative; duplicated members are ignored, the order of the members is arbitrary, and nesting is irrelevant:

[0248] either{τ; τ; τ′}≅either{τ; τ′}

[0249] either{τ; τ′;}≅either{τ′; τ;}

[0250] either{either{ τ}; τ′}≅either{ τ τ′}

[0251] Associativity also works across streams.

[0252] sequence<either{sequence<either{ τ}>; τ′}>≅sequence<either{ τ τ′}>

[0253] Values of non-discriminated union types can be injected into a discriminated union:

[0254] $\frac{\tau \ne \mathrm{either}\left\{\stackrel{\_}{{\tau }^{″}}\right\}}{\tau <:\mathrm{either}\left\{\tau ;\stackrel{\_}{{\tau }^{\prime }}\right\}e\mapsto \mathrm{new}\mathrm{either}\left\{\tau ;\stackrel{\_}{{\tau }^{\prime }}\right\}\left(\tau ,e\right)}$

[0255] InnerXen allows width subtyping for discriminated unions. In this case the coercion is slightly more involved as it extracts the value from the source discriminated union before creating the target discriminated union.

[0256] ${\stackrel{\_}{\frac{\mathrm{either}\left\{\stackrel{\_}{{\tau }_i}\right\}<:\mathrm{either}\{\mathrm{either}\left\{\stackrel{\_}{{\tau }_i};\stackrel{\_}{{\tau }^{\prime }}\right\}}{e\mapsto \left(\left\{\mathrm{if}\left(e\mathrm{was}{\tau }_i\right)\mathrm{return}\mathrm{new}\mathrm{either}\left\{\stackrel{\_}{{\tau }_i}\stackrel{\_}{{\tau }^{\prime }}\right\}\left({\tau }_i,e.\mathrm{value}\right);\right\}\right)}}}^{\mathrm{(*})}$

[0257] Here, and in the following, the convention of indexing sequences is used, i.e., τ_i represents a sequence of types, where each type is indexed with its position. An element of this sequence at position i is referred to as τ_i.

[0258] The rules above are carefully crafted to allow alternative implementations that do not use types as tags for discriminated unions. They allow any implementation that maintains the stated invariant for the conformity test, e.g., integers tags used in the actual Xen implementation.

[0259] InnerXen follows the design of C# in allowing all values to be boxed, and hence, all value types are a subtype of the supertype object. For values of discriminated unions, boxing is a little more subtle as it should first strip off the type tag and then upcast to object.

[0260] $\frac{\stackrel{\_}{{\tau }_i<:\mathrm{object}{g}_i}}{\mathrm{either}\left\{\stackrel{\_}{{\tau }_i}\right\}<:\mathrm{object}e\mapsto \left(\left\{\mathrm{if}\left(e\mathrm{was}{\tau }_i\right)\mathrm{return}{g}_i\left(e.\mathrm{value}\right);\right\}\right)}\mathrm{(*})$

[0261] Generalized Member Access

[0262] The essence of Xen is that member access is uniformly lifted over all structural types. This gives the language much of the expressive power of query languages such as XPath. This generalized member access is treated in a similar way as subtyping in that it is replaced with explicit coercions.

[0263] Each type constructor is now considered in turn and for each, two new judgment forms are formalized:

[0264] The field access judgment τ.f<: τ′g returns a witness g: τ→τ′ that performs the lookup of field f on an instance of τ. Positional field access is analogous and omitted.

[0265] The method call judgment τ.m( τ′)<: T″g returns a witness g: (τ, τ′)→τ″ that calls the method with signature τ″ m( τ′) on a receiver of type τ.

[0266] Member access over streams. Lifting member access on streams is really just syntactic sugar for a simple apply-to-all expression of member access on the elements of the stream.

[0267] $\frac{\tau .f<:{\tau }^{\prime }g}{\mathrm{sequence}<\tau >.f<:\mathrm{sequence}<{\tau }^{\prime }>e\mapsto e.\left\{\mathrm{return}g\left(\mathrm{it}\right);\right\}}\mathrm{(*})$

[0268] Methods that return non-void results are lifted similarly to field-access. For example, each string can be converted to uppercase in the stream ss from earlier by simply writing ss.ToUpper( ). This expression is translated into the apply-to-all block ss.{return it.ToUpper( );}. Again, the witness for lifting general method invocation over streams introduces an apply-to-all block:

[0269] $\frac{\left(\tau .m\left(\stackrel{\_}{{\tau }^{\prime }}\right)<:{\tau }^{″}g\right)}{\begin{array}{c}\mathrm{sequence}<\tau >.m\left(\stackrel{\_}{{\tau }^{\prime }}\right)<:\\ \mathrm{sequence}<{\tau }^{″}>\left(e,\stackrel{\_}{a}\right)\mapsto e.\left\{\mathrm{return}g\left(\mathrm{it},\stackrel{\_}{a}\right);\right\}\end{array}}\mathrm{(*})$

[0270] Methods that return void are applied to each element of the stream. There is no stream of void.

[0271] $\frac{\tau .m\left(\stackrel{\_}{{\tau }^{\prime }}\right)<:\mathrm{void}g}{\begin{array}{c}\mathrm{sequence}<\tau >.m\left(\stackrel{\_}{{\tau }^{\prime }}\right)<:\\ \mathrm{void}\left(e,\stackrel{\_}{a}\right)\mapsto \mathrm{foreach}\tau \mathrm{it}\mathrm{in}g\left(\mathrm{it},\stackrel{\_}{a}\right);\end{array}}\mathrm{(*})$

[0272] Note that even members of object are lifted. Thus, for instance, the result of calling ss.GetType( ) on a stream ss has type sequence<Type>. In order to perform method invocation on the actual stream, it casts to object first, e.g., ((object)ss).GetType( ).

[0273] Member access over tuple types. Accessing tuple type members returns a new tuple type that contains as tuple members only those that were selected from the original tuple type. For example the selection s.x on a variable s of type struct {int x; string; bool x;} returns a new tuple type of type struct (int; bool;} that is created by the expression new (s[0],s[2]). This idea of projection is given by the following rule, where the premise uses a list comprehension to generate a list of triples (τ₀, g₀, i) for each member fd_i that has a member f. In the conclusion, one writes g_i(e[i]) to select only those elements from the given tuple type and apply the respective conversion on that member.

[0274] $\frac{\left[\left(\tau ,g_i,i\right)❘{\mathrm{fd}}_i.f<:\tau g_i\right]}{\mathrm{struct}\left\{\stackrel{\_}{{\mathrm{fd}}_i}\right\}.f<:\mathrm{struct}\left\{\stackrel{\_}{\tau }\right\}e\mapsto \mathrm{new}\left(\stackrel{\_}{g_i\left(e\left[i\right]\right)}\right)}$

[0275] The base case of member access is when the label of a field matches the label that is accessed.

[0276] τf.f<: τ id

[0277] Method calls are lifted over tuple types in a similar way as member selection.

[0278] $\begin{array}{cc}\frac{\left[\left({\tau }^{\prime },g_i,i\right)❘{\mathrm{fd}}_i.m\left(\stackrel{\_}{\tau }\right)<:{\tau }^{\prime }{g}_i\right]}{\begin{array}{c}\mathrm{struct}\left\{\stackrel{\_}{{\mathrm{fd}}_i}\right\}.m\left(\stackrel{\_}{\tau }\right)<:\mathrm{struct}\left\{\stackrel{\_}{{\tau }^{\prime }}\right\}e\mapsto \\ \mathrm{new}\left(\stackrel{\_}{g_i\left(e\left[i\right]\right)}\right)\end{array}}& \end{array}$

[0279] When member selection, or method calls succeeds for just one member, the struct is not created, but just the value of that member is returned. For example, given value p of type struct{int x; int y;}, selecting p.x returns a single value x[0] of type int. This refinement should be obvious and is omitted.

[0280] Member access over discriminated unions. It is known that a given value matches exactly one of the alternatives of a discriminated union. To lift member access over discriminated unions, a conformity test of the current value is performed, and the corresponding member selected. For example, given a value x of type either (string; Person; int) where both string and Person have a member Length of type int and Inch, respectively, lifting x.Length returns a value of type Sequence<either{int; Inch;}> via the translation:

[0281] ({if(x was string){yield return x.value.Length;}

• • [0282] if(x was Person){yield return x.value.Length;}})

[0283] The general rule for lifting field selection and method invocation over discriminated unions collects the alternatives for which the member lookup succeeds, and creates the conformity test to determine the member/method to actually select/invoke.

[0284] $\frac{\left[\left({\tau }^{\prime },g_i,i\right)❘{\tau }_i.f<:{\tau }^{\prime }{g}_i\right]}{\begin{array}{c}\mathrm{either}\left\{\stackrel{\_}{{\tau }_i}\right\}.f<:\mathrm{sequence}<\mathrm{either}\left\{\stackrel{\_}{{\tau }^{\prime }}\right\}>e\mapsto \\ \left(\left\{\stackrel{\_}{\mathrm{if}\left(e\mathrm{was}{\tau }_i\right)\mathrm{yield}\mathrm{return}{g}_i\left(e.\mathrm{value}\right);}\right\}\right)\end{array}}\mathrm{(*})$

[0285] $\frac{\left[\left({\tau }^{″},g_i,i\right)❘{\tau }_i.m\left(\stackrel{\_}{{\tau }^{\prime }}\right)<:{\tau }^{″}{g}_i\right]}{\begin{array}{c}\mathrm{either}\left\{\stackrel{\_}{{\tau }_i}\right\}.m\left(\stackrel{\_}{{\tau }^{\prime }}\right)<:\mathrm{sequence}<\mathrm{either}\left\{\stackrel{\_}{{\tau }^{″}}\right\}>e\mapsto \\ \left(\left\{\stackrel{\_}{\mathrm{if}\left(e\mathrm{was}{\tau }_i\right)\mathrm{yield}\mathrm{return}{g}_i\left(e.\mathrm{value}\right);}\right\}\right)\end{array}}\mathrm{(*})$

[0286] When member access succeeds for every alternative in the discriminated union, the return type can sometimes be improved. For example x.GetType( ) would return a value of type object instead of sequence<object>.

[0287] Member access over classes. Method invocation on classes, i.e., nominal types, searches the class hierarchy until a matching method is found. If a matching method τ′m( τ″) in class c is found, the actual types of the arguments are adjusted to the types expected by m:

[0288] $\frac{\mathrm{class}c:c^{\prime }\left\{\tau ,\stackrel{\_}{\mathrm{md}}\right\}{\tau }^{\prime }m\left(\stackrel{\_}{{\tau }^{″}}\right)\in \stackrel{\_}{\mathrm{md}}\stackrel{\_}{\tau }<:\stackrel{\_}{{\tau }^{″}}f}{c.m\left(\stackrel{\_}{\tau }\right)<:{\tau }^{\prime }\left(e.\stackrel{\_}{a}\right)\mapsto e.m\left(\stackrel{\_}{f\left(a\right)}\right)}$

[0289] When the method is not found in the current class, its superclass is searched. In this case, before performing the call, the receiver is upcasted. When calling a method defined on object on a base type, such as 5.GetType( ), this method invocation is translated into

[0290] $\frac{\begin{array}{c}\mathrm{class}c:c^{\prime }\left\{\tau ,\stackrel{\_}{\mathrm{md}}\right\}{\tau }^{\prime }m\left(\stackrel{\_}{{\tau }^{″}}\right)\notin \stackrel{\_}{\mathrm{md}}{c}^{\prime }.m\left(\stackrel{\_}{\tau }\right)<:\\ {\tau }^{\prime }gc<:c^{\prime }f\end{array}}{c.m\left(\stackrel{\_}{\tau }\right)<:{\tau }^{\prime }\left(e,\stackrel{\_}{a}\right)\mapsto g\left(f\left(e\right),\stackrel{\_}{a}\right)}$

[0291] Recall that InnerXen class declarations contain, in addition to the methods, just a single content type. Thus, one might expect that the rules for generalized member access can be blindly applied to access elements of classes. Recursion requires a different approach. Consider the following recursive class List of lists of integers:

[0292] class List {struct{int head; List;}}

[0293] Given an instance xs of type List, it is not desired that xs.head recursively select all head fields in xs. However, simply unfolding the content type and using the rules given above for generalized access over tuple types that is precisely what would happen. There are a number of solutions, but in order to keep the Xen type system as simple as possible, the recursive cycles are broken at nominal types. This means that member lookup is not performed on nominal members of the content of nominal types. Using these refined rules, the result type of xs.head is int.

[0294] Formalizing this is trivial, but time-consuming. Another family of generalized member access judgments are defined, written τ·fg, which is identical to the previous rules except they are not defined for nominal types.

[0295] To define field access on nominal types, the content type of a class is first defined as follows.

[0296] $\frac{\mathrm{class}c\left\{\tau ;\stackrel{\_}{\mathrm{md}}\right\}}{\mathrm{content}\left(c\right)=\tau }\frac{\mathrm{class}c:c^{\prime }\left\{\tau ;\stackrel{\_}{\mathrm{md}};\right\}\mathrm{content}\left(c^{\prime }\right)={\tau }^{\prime }}{\mathrm{content}\left(c\right)=\mathrm{struct}\left\{{\tau }^{\prime };\tau \right\}}$

[0297] InnerXen provides a special member on class values, e.content that returns the content type value. The rule for generalized field selection on classes searches for the member f on the content type of class c and then applies the witness to the content value of the instance.

[0298] $\frac{\mathrm{content}\left(c\right)=\tau \tau ·fg}{c.f<:\tau e\mapsto g\left(e.\mathrm{content}\right)}$

[0299] Typing InnerXen Programs

[0300] Building on the previous description subsections, the rules for forming typing judgments over InnerXen expressions, statements, method declarations and programs are now provided.

[0301] Typing expressions. For the most part, the typing judgments for InnerXen are straightforward. As subtyping is treated using coercions, a typing judgment for expressions is of the form E├e <: τe′, which means that in a typing context E (which is a map from variable names to types) expression e has type τ and is expanded to the expression e′.

[0302] The rules for expressions all follow the same pattern where the judgment on the level of expressions is defined in terms of a similar judgment on types. In addition to the member access and method call judgments described hereinabove, judgments for dynamic casting will be defined and used.

[0303] The typing judgments for literals, variables and null are standard and as follows.

[0304] $\begin{array}{cc}\stackrel{\_}{E⊢i<:\mathrm{int}}& \stackrel{\_}{E⊢b<:\mathrm{bool}}\\ \stackrel{\_}{E[x}& \stackrel{\_}{E⊢\mathrm{null}<:\mathrm{null}}\end{array}$

[0305] The judgments for casting involve the application of the upcasting judgment τ <: τ′f that was defined earlier and two new downcasting judgments (τ) τ′f and τis τ′f.

[0306] The downcasting rule (τ)τ′ recursively deconstructs the downcast from a value of static type τ′ to a value of dynamic type τ up to the point where τ′ is a reference type. In that case, a true dynamic downcast can be performed based on the fact that reference types carry their dynamic type. Downcasting from a reference type to a value type also unboxes the value at runtime.

[0307] (γ)ρ e ((γ)e).content (ρ)ρ′ e (ρ)e

[0308] Downcasting from one struct to another attempts the downcast on all the components of the struct. Here, downcasting is lifted over field declarations in the obvious way.

[0309] $\frac{\stackrel{\_}{\left({\mathrm{fd}}_i\right){\mathrm{fd}}_i^{\prime }}\stackrel{\_}{g_i}}{\left(\mathrm{struct}\left\{\stackrel{\_}{{\mathrm{fd}}_i}\right\}\right)\mathrm{struct}\left\{{\mathrm{fd}}_i^{\prime }\right\}e\mapsto \mathrm{new}\left(\stackrel{\_}{g_i\left(e\left[i\right]\right)}\right)}$

[0310] Downcasting from a discriminated union first removes the type tag and then attempts to downcast the resulting value. It is not permitted to downcast to an either type.

[0311] $\frac{\stackrel{\_}{\left(\tau \right){\tau }_i^{\prime }}\stackrel{\_}{g_i}}{\left(\tau \right)\mathrm{either}\left\{\stackrel{\_}{{\tau }_i^{\prime }}\right\}e\mapsto \stackrel{\_}{\left(\left\{\mathrm{if}\left(e\mathrm{was}{\tau }_i^{\prime }\right)\mathrm{return}{g}_i\left(e.\mathrm{value}\right);\right\}\right)}}\mathrm{(*})$

[0312] The typing judgments are now defined for both directions of casting of expressions in terms of these judgments on types:

[0313] $\frac{E⊢e<:{\tau }^{\prime }{e}^{\prime }{\tau }^{\prime }<:\tau f}{E⊢\left(\tau \right)e<:\tau f\left(e^{\prime }\right)}\left(\mathrm{upcast}\right)$ $\frac{E⊢e<:{\tau }^{\prime }{e}^{\prime }\tau <:{\tau }^{\prime }\left(\tau \right){\tau }^{\prime }f}{E⊢\left(\tau \right)e<:\tau f\left(e^{\prime }\right)}\left(\mathrm{downcast}\right)$

[0314] Note that in order to satisfy a type soundness property, a “stupid” cast rule is defined in the now familiar fashion, but avoided here for brevity.

[0315] InnerXen has the is operator from C# that performs a dynamic check if the runtime type of an object is compatible with a given type. For this, an auxiliary judgment form τ is τ′g is introduced that returns the witness g for testing whether a value of type τ is at runtime a value of type τ′. The first three judgments are standard.

[0316] $\frac{\gamma <:\tau }{\gamma \mathrm{is}\tau e\mapsto \mathrm{true}}\frac{\rho <:\tau }{\rho \mathrm{is}\tau e\mapsto e!=\mathrm{null}}$ $\frac{\tau <:\rho }{\rho \mathrm{is}\tau e\mapsto \left(e!=\mathrm{null}\right)\&\&\left(e\mathrm{is}\tau \right)}$

[0317] The judgments for tuple types and discriminated unions show a duality. For tuple types it is recursively checked whether the is relation holds for all the components of the struct, while for discriminated unions, it is checked if any of the components was of the required type. Here, the is relation is lifted over field declarations in the obvious way.

[0318] $\stackrel{\_}{{\mathrm{fd}}_i}\mathrm{is}\stackrel{\_}{{\mathrm{fd}}_i^{\prime }}\stackrel{\_}{g_i}$ $\stackrel{\_}{\mathrm{struct}\left\{\stackrel{\_}{{\mathrm{fd}}_i}\right\}\mathrm{is}\mathrm{struct}\left\{\stackrel{\_}{{\mathrm{fd}}_i^{\prime }}\right\}e\mapsto \stackrel{\_}{\&\&g_i\left(e\left[i\right]\right)}}$ $\stackrel{\_}{\mathrm{either}\left\{\stackrel{\_}{\tau }\right\}\mathrm{is}\mathrm{either}\left\{\stackrel{\_}{\tau }\stackrel{\_}{{\tau }^{\prime }}\right\}e\mapsto \stackrel{\_}{e\mathrm{was}{\tau }_i^{\prime }}}$

[0319] The typing judgment for an is expression can now be defined in terms of the judgment on types:

[0320] $\frac{E⊢e<:{\tau }^{\prime }{e}^{\prime }{\tau }^{\prime }\mathrm{is}\tau g}{E⊢e\mathrm{is}\tau <:\mathrm{bool}g\left(e^{\prime }\right)}$

[0321] The typing judgment for the expression e was τ ensures that static type of e is a discriminated union that includes τ, and generates the actual runtime conformity test to check if the dynamic value of e has type tag τ.

[0322] $\frac{E⊢e<:\mathrm{either}\left\{\tau ;\stackrel{\_}{{\tau }^{\prime }}\right\}{e}^{\prime }}{E⊢e\mathrm{was}\tau <:\mathrm{bool}{e}^{\prime }\mathrm{was}\tau }$

[0323] The type of an instance of a tuple type is derived from the type of the actual arguments of its constructor. The type of a binding expression f=e is derived from the binding expression e.

[0324] $\frac{E⊢\stackrel{\_}{\mathrm{be}}<:\stackrel{\_}{\mathrm{fd}}\stackrel{\_}{{\mathrm{be}}^{\prime }}}{E⊢\mathrm{new}\left(\stackrel{\_}{\mathrm{be}}\right)<:\mathrm{struct}\left\{\stackrel{\_}{\mathrm{fd}}\right\}\mathrm{new}\left(\stackrel{\_}{{\mathrm{be}}^{\prime }}\right)}$

[0325] The core subset of Xen supports one-argument constructors for classes that take an instance of the content type of that class:

[0326] $\frac{E⊢e<:\tau e^{\prime }\tau <:\mathrm{content}\left(c\right)f}{E⊢\mathrm{new}c\left(e\right)<:c\mathrm{new}c\left(f\left(e^{\prime }\right)\right)}$

[0327] Users never need to use the constructor for discriminated unions themselves, instead they can use subtyping to implicitly coerce a value into a discriminated union. Similarly, users never need to create closures explicitly, instead they use generating block expressions or methods. However, for completeness the type rules for these two constructors are provided:

[0328] $\frac{E⊢e<:\tau e^{\prime }}{\begin{array}{c}E⊢\mathrm{new}\mathrm{either}\left\{\tau ;\stackrel{\_}{{\tau }^{\prime }}\right\}\left(\tau ,e\right)<:\\ \mathrm{either}\left\{\tau ;\stackrel{\_}{{\tau }^{\prime }}\right\}\mathrm{new}\mathrm{either}\left\{\tau ;\stackrel{\_}{{\tau }^{\prime }}\right\}\left(\tau ,e^{\prime }\right)\end{array}}$

[0329] The following example uses coercion, tuple type, and class construction to build an instance of the Address type:

[0330] Address a=new Address(new(new(POBox=4711), City=“Atlantis”));

[0331] It is illustrated hereinbelow how XML literals in the full Xen language make constructing such values easy.

[0332] The typing judgment for member access e.f on expressions simply uses the judgment for generalized member lookup defined earlier:

[0333] $\frac{E⊢e<:}{E⊢e.f<:{\tau }^{\prime }g\left(e^{\prime }\right)}$

[0334] Positional access is not lifted; the receiver must be a tuple type:

[0335] $\frac{E⊢e<:\mathrm{struct}\left\{\stackrel{\_}{{\mathrm{fd}}_i}\right\}\tau e^{\prime }\mathrm{type}\left(\stackrel{\_}{{\mathrm{fd}}_i}\right)=\tau }{E⊢e\left[i\right]<:\tau e^{\prime }\left[i\right]}$

[0336] Typing promotable expressions. Promotable block expressions are the sinkholes of all new syntactic forms. Promotable block expressions are translated into closures when their bodies are generators; otherwise, they are translated into elementary block expressions. Typing of block expressions uses a conventional “repmin”-trick to feed the derived type of a statement list back as the required type. The function sort( τ) is used to infer the required type of block expressions and apply-to-all expressions from the derived types. It constructs a discriminated union of all the maximal types (or just the maximal type, if there is just one).

[0337] The maximal type of a set of types is their least upper bound, provided it can be reached with identity conversions only. When the block expression is a generator block, i.e., contains a yield statement (which is checked by the yields predicate), the inferred type is a stream of the inferred type. For the expression {yield return 47; yield return “Hello”;} the derived types for the block statements will be int, string and hence, the required type of the block will be sequence<either{int; string;)>. Note that Xen's syntactic context condition requires that any expression block must either have yield or return statements.

[0338] $\frac{E,\mathrm{sequence}<\mathrm{sort}\left(\stackrel{\_}{\tau }\right)>⊢\stackrel{\_}{s}<:\stackrel{\_}{\tau }\stackrel{\_}{s^{\prime }}\mathrm{yields}\left(\stackrel{\_}{s}\right)}{\left(\left\{\stackrel{\_}{s}\right\}\right)<:\mathrm{sequence}<\mathrm{sort}(\stackrel{\_}{\tau })>\mathrm{new}\mathrm{sequence}<\mathrm{sort}\left(\stackrel{\_}{\tau }\right)>\left(\stackrel{\_}{s^{\prime }}\right)}$ $\frac{\underset{\_}{E,\mathrm{sort}\left(\stackrel{\_}{\tau }\right)⊢\stackrel{\_}{s}<:\stackrel{\_}{\tau }\stackrel{\_}{s^{\prime }}⫬\mathrm{yields}\left(\stackrel{\_}{s}\right)}}{E⊢\left(\left\{\stackrel{\_}{s}\right\}\right)<:\mathrm{sort}\left(\stackrel{\_}{\tau }\right)\left(\left\{\stackrel{\_}{s^{\prime }}\right\}\right)}$

[0339] The typing of assignment is straightforward:

[0340] $\frac{E⊢x<:\tau E⊢e<:{\tau }^{\prime }{e}^{\prime }\tau <:{\tau }^{\prime }f}{E⊢x=e<:\tau x=f\left(e\right)}$

[0341] As for C# and Java, method resolution is based on the static types of the actual arguments and the receiver object. The generalized method invocation judgment defined earlier is used:

[0342] $\frac{E⊢e<:\tau }{E⊢e·m\left(\stackrel{\_}{a}\right)<:{\tau }^{″}f\left(e^{\prime },\stackrel{\_}{a^{\prime }}\right)}$

[0343] Apply-to-all blocks on streams are syntactic sugar for a promotable block expression that applies the block to each element of its receiver stream. Note, again, the derived type is passed back as the required type.

[0344] $\frac{\left(E⊢e<:\mathrm{sequence}\langle \tau \rangle e^{\prime }E\left[\mathrm{it}⊢\tau \right],\mathrm{sequence}<\mathrm{sort}\left(\stackrel{\_}{\tau }\right)>⊢\stackrel{\_}{s^{\prime }}<:\stackrel{\_}{{\tau }^{\prime }}\stackrel{\_}{s^{\prime }}\right)}{\begin{array}{c}(E⊢e.\left\{\stackrel{\_}{s}\right\}<:\mathrm{sequence}<\mathrm{sort}\left(\stackrel{\_}{{\tau }^{\prime }}\right)>\\ \left(\left\{\mathrm{foreach}\left(\tau \mathrm{it}\mathrm{in}{e}^{\prime }\right)\mathrm{yield}\mathrm{return}\left(\left\{\stackrel{\_}{s^{\prime }}\right\}\right);\right\}\right))\end{array}}$

[0345] Typing statements. The empty statement does not contribute anything to the result of a statement block; neither does a nested block:

[0346] $\stackrel{\_}{E,\tau ⊢;<:\mathrm{void};}$ $\frac{E,\tau ⊢\stackrel{\_}{s}<:\stackrel{\_}{{\tau }^{\prime }}{s}^{\prime }}{E,\tau ⊢\left\{\stackrel{\_}{s}\right\}<:\stackrel{\_}{{\tau }^{\prime }}\left\{s^{\prime }\right\}}$

[0347] Promotable expressions are executed for their side-effects, and their type is ignored:

[0348] $\frac{E⊢\mathrm{pe}<:{\tau }^{\prime }{\mathrm{pe}}^{\prime }}{E,\tau ⊢\mathrm{pe}<:\mathrm{void}{\mathrm{pe}}^{\prime }}$

[0349] The derived types of the two branches of conditional statements are combined, and the condition must have type bool. The while statement is completely analogous:

[0350] $\frac{\begin{array}{c}E⊢e<:\mathrm{bool}{e}^{\prime }E,\tau ⊢s_1<:\stackrel{\_}{{\tau }^{\prime }}\mathrm{void}{s}_1^{\prime }E,\\ \tau ⊢s_2<:\stackrel{\_}{{\tau }^{″}}\mathrm{void}{s}_2^{\prime }\end{array}}{E,\tau ⊢\mathrm{if}\left(e\right)s_1\mathrm{else}{s}_2<:\stackrel{\_}{{\tau }^{\prime }},\stackrel{\_}{{\tau }^{″}}\mathrm{if}\left(e^{\prime }\right)s_1^{\prime }\mathrm{else}{s}_2^{\prime }}$ $\frac{E⊢e<:\mathrm{bool}{e}^{\prime }E,\tau ⊢s<:\stackrel{\_}{{\tau }^{\prime }}{s}^{\prime }}{E,\tau ⊢\mathrm{while}\left(e\right)s<:\stackrel{\_}{{\tau }^{\prime }}\mathrm{while}\left(e^{\prime }\right)s^{\prime }}$

[0351] The required result type of statements is used in the return and yield statements. The empty return statement can only occur in a void returning context.

[0352] E, void ├ return; <: void return;

[0353] If necessary, the derived return type τ′ of a normal return statement is coerced to the required return type τ.

[0354] $\frac{E⊢e<:{\tau }^{\prime }{e}^{\prime }{\tau }^{\prime }<:\tau f}{E,\tau ⊢\mathrm{return}e;<:{\tau }^{\prime }\mathrm{return}f\left(e^{\prime }\right)}$

[0355] The return-type of a yield break statement is the null type.

[0356] E, sequence<τ> ├ yield break; <: null yield break;

[0357] The required type of a yield return statement is a stream type, and if necessary, the derived return type is upcasted to the required return type. A way of inspecting a stream element is by consuming it in a foreach loop. Otherwise stream elements can never be inspected. The implementation has to distinguish only between stream elements that produce streams and ones that are simple values. Formalization herein uses the type tagging scheme that has been introduced for either values.

[0358] $\frac{E⊢e<:{\tau }^{\prime }{e}^{\prime }{\tau }^{\prime }\ne \mathrm{sequence}\langle {\tau }^{″}\rangle {\tau }^{\prime }<:\tau f}{\begin{array}{c}E,\mathrm{sequence}\langle {\tau }^{\prime }\rangle ⊢\mathrm{yield}\mathrm{return}e;<:\mathrm{sequence}\langle {\tau }^{\prime }\rangle \\ \mathrm{yield}\mathrm{return}\mathrm{new}\mathrm{sequence}\langle {\tau }^{\prime }\rangle \left(\tau ,f\left(e^{\prime }\right)\right);\end{array}}$ $\frac{\begin{array}{c}E⊢e<:\mathrm{sequence}\langle {\tau }^{\prime }\rangle e^{\prime }\mathrm{sequence}\langle {\tau }^{\prime }\rangle \\ <:\mathrm{sequence}\langle \tau \rangle f\end{array}}{\begin{array}{c}E,\mathrm{sequence}\langle \tau \rangle ⊢\mathrm{yield}\mathrm{return}e;<:\mathrm{sequence}\langle {\tau }^{\prime }\rangle \\ \mathrm{yield}\mathrm{return}\mathrm{new}\mathrm{sequence}\langle {\tau }^{\prime }\rangle \left(\mathrm{sequence}\langle {\tau }^{\prime }\rangle ,f\left(e^{\prime }\right)\right);\end{array}}$

[0359] The last rule uses the equivalence sequence<τ′>≅sequence<sequence<τ′>> for simplification of the inferred return type. This rule also shows that covariance on streams is only applicable when the coercion on the element type is the identity. Thus, sometimes, a nested stream is explicitly copied to “open it for conversion”. For example, the following method fails to type-check because the type of the type of ns is not convertible to the required type of the method f:

sequence<int> ns= . . . ;

sequence<object> f( ) {yield return ns;}

[0360] The type correct way is to copy the stream ns, such that each element can be implicitly boxed from int to object.

sequence<object> f( ) {yield return ns. {return it;};}

[0361] Note the conciseness of the apply-to-all expression to achieve this. Depending on whether the element type of the collection in a foreach statement is a supertype or a subtype of the declared type of the iteration variable, coercion is first applied to a fresh iteration variable y (i.e., y∉dom (E)):

[0362] $\frac{\begin{array}{c}E⊢e<:\mathrm{sequence}\langle {\tau }^{\prime }\rangle e^{\prime }{\tau }^{\prime }<:{\tau }^{″}f\\ E\left[x\mapsto {\tau }^{″}\right],\tau ⊢s<:\stackrel{\_}{{\tau }^{\mathrm{\prime \prime \prime }}}{s}^{\prime }\end{array}}{\begin{array}{c}E,\tau ⊢\mathrm{foreach}\left({\tau }^{″}x\mathrm{in}e\right)s<:\stackrel{\_}{{\tau }^{\mathrm{\prime \prime \prime }}}\\ \mathrm{foreach}\left({\tau }^{\prime }y\mathrm{in}{e}^{\prime }\right)\left\{{\tau }^{″}x=f\left(y\right);s^{\prime }\right\}\end{array}}$

[0363] $\frac{\begin{array}{c}E⊢e<:\mathrm{sequence}\langle {\tau }^{\prime }\rangle e^{\prime }\left({\tau }^{″}\right){\tau }^{\prime }\\ fE\left[x\mapsto {\tau }^{″}\right],\tau ⊢s<:\stackrel{\_}{{\tau }^{\mathrm{\prime \prime \prime }}}{s}^{\prime }\end{array}}{\begin{array}{c}E,\tau ⊢\mathrm{foreach}\left({\tau }^{″}x\mathrm{in}e\right)s<:\stackrel{\_}{{\tau }^{\mathrm{\prime \prime \prime }}}\\ \mathrm{foreach}\left({\tau }^{\prime }y\mathrm{in}{e}^{\prime }\right)\left\{{\tau }^{″}x=f\left(y\right);s^{\prime }\right\}\end{array}}$

[0364] Typing statement lists. Local variable declarations in statement lists are similar to a local variable assignment, but they also extend the environment:

[0365] $\frac{E⊢e<:{\tau }^{\prime }{e}^{\prime }{\tau }^{\prime }<:{\tau }^{″}\mathrm{fE}\left[x\mapsto {\tau }^{″}\right],\tau ⊢s<:\stackrel{\_}{{\tau }^{\mathrm{\prime \prime \prime }}}\stackrel{\_}{s^{\prime }}}{E,\tau ⊢{\tau }^{″}x=e;\stackrel{\_}{s}<:\stackrel{\_}{{\tau }^{\mathrm{\prime \prime \prime }}}{\tau }^{″}x=f\left(e^{\prime }\right);\stackrel{\_}{s^{\prime }}}$

[0366] In all other cases, the derived types of the statement lists are combined

[0367] $\frac{E,\tau ⊢s<:\stackrel{\_}{{\tau }^{\prime }}{s}^{\prime }E,\tau ⊢\mathrm{ss}<:\stackrel{\_}{{\tau }^{″}}{\mathrm{ss}}^{\prime }}{E,\tau ⊢s\mathrm{ss}<:\stackrel{\_}{{\tau }^{\prime }},\stackrel{\_}{{\tau }^{″}}{s}^{\prime }{\mathrm{ss}}^{\prime }}$

[0368] Typing programs. The rules for typing programs and class declarations are straightforward, and just recursively check/translate all class declarations in a program:

[0369] $\frac{\frac{c{c}^{\prime }\stackrel{\_}{\mathrm{cd}}\stackrel{\_}{{\mathrm{cd}}^{\prime }}}{\stackrel{\_}{c\mathrm{cd}}\stackrel{\_}{c^{\prime }{\mathrm{cd}}^{\prime }}}c⊢\stackrel{\_}{\mathrm{md}}\stackrel{\_}{{\mathrm{md}}^{\prime }}}{\mathrm{class}c:c^{\prime }\left\{\tau \stackrel{\_}{\mathrm{md}}\right\}\mathrm{class}c:c^{\prime }\left\{\tau \stackrel{\_}{{\mathrm{md}}^{\prime }}\right\}}$

[0370] Consider typing method declarations. Normal methods are checked by extending the environment with the types of the formal parameters and the this pointer.

[0371] $\frac{\left[\mathrm{this}\mapsto c,\stackrel{\_}{x}\mapsto \stackrel{\_}{\tau }\right],{\tau }^{\prime }⊢\stackrel{\_}{s}<:\stackrel{\_}{{\tau }^{″}}\stackrel{\_}{s^{\prime }}⫬\mathrm{yields}\left(\stackrel{\_}{s}\right)}{c⊢{\tau }^{\prime }m\left(\stackrel{\_}{\tau x}\right)\left\{\stackrel{\_}{s}\right\}<:{\tau }^{\prime }m\left(\stackrel{\_}{\tau x}\right)\left\{\stackrel{\_}{s^{\prime }};\right\}}$

[0372] Generator methods, i.e., methods that yield, are translated into ordinary methods that immediately return a promotable block expression that constructs a closure to lazily generate the stream defined by this method.

[0373] $\frac{\left[\mathrm{this}\mapsto c,\stackrel{\_}{x}\mapsto \stackrel{\_}{\tau }\right],\mathrm{sequence}\langle {\tau }^{\prime }\rangle ⊢\stackrel{\_}{s}<:\stackrel{\_}{{\tau }^{″}}\stackrel{\_}{s^{\prime }}\mathrm{yields}\left(\stackrel{\_}{s}\right)}{\begin{array}{c}c⊢{\tau }^{\prime }m\left(\stackrel{\_}{\tau x}\right)\left\{\stackrel{\_}{s}\right\}\mathrm{sequence}\langle {\tau }^{\prime }\rangle m\left(\stackrel{\_}{\tau x}\right)\\ \left\{\mathrm{return}\mathrm{new}\mathrm{sequence}\langle {\tau }^{\prime }\rangle \left(\stackrel{\_}{s^{\prime }}\right);\right\}\end{array}}$