Baptiste Véron

Arnaud Hubert

Joël Abadie

Nicolas Andreff

Geometric analysis of the singularities of a magnetic manipulation system with several mobile coils

It has been demonstrated that magnetic fields are relevant for manipulating an untethered magnet, either using fixed coils or mobile permanent magnets. This paper shows however, that any magnetic manipulation method is prone to singular configurations and that the simple numerical analysis of the rank of the "manipulation matrix" is not enough to detect them. Alternatively, we propose a geometrical analysis to interpret and detect the singularities as well as to decide on the acceptability of a reference trajectory. Then, we present results obtained by simulating a planar manipulation system including a multiple mobile coils and a Helmholtz like set-up.

I. INTRODUCTION

This work is in the context of the gastrointestinal endoscopy. Since the development of the M2A capsule endoscopy system [START_REF] Yu | M2a (tm) capsule endoscopy: A breakthrough diagnostic tool for small intestine imaging[END_REF], several studies have been led to improve the concept of capsular device navigating through the gastrointestinal tracts, especially about the two challenges of the localization and the controlled manipulation of the capsule. This paper focuses on this second challenge: replacing passive locomotion (peristaltis) of the capsule, by an active control of the motion.

One way to control the capsule motion is to add legs to the capsule [START_REF] Alonso | Control electronics integration toward endoscopic capsule robot performing legged locomotion and illumination[END_REF], but this yields strong energy concerns.

An alternative to embedded actuation is to actuate the capsule externally using magnetic fields. This presents the advantage of being non toxic to the human body [START_REF] Schenck | Human exposure to 4.0 tesla magnetic fields in a whole-body scanner[END_REF] and it permits to remotely control the device without any potentially traumatic gripping in the intestinal wall (due to the legs). Two approaches can be found in the literature for this type of magnetic manipulation.

The first method employs stationary electromagnets and then control their currents to adjust the magnetic field (as in opthalmology) [START_REF] Yessin | Modeling and control of untethered biomicrorobots in a fluidic environment using electromagnetic fields[END_REF], [START_REF] Kummer | Octomag: An electromagnetic system for 5-dof wireless micromanipulation[END_REF]. In a Helmholtz configuration, the workspace lies between the two coils where a uniform magnetic field is present [START_REF] Wang | Study on magnetic localization and actuation of active capsule endoscope[END_REF]. This is used in MRI systems to displace a magnetic micro-object within the blood vessels [START_REF] Felfoul | Real-time positioning and tracking technique for endovascular untethered microrobots propelled by mri gradients[END_REF], [START_REF] Martel | Automatic navigation of an untethered device in the artery of a living animal using a conventional clinical magnetic resonance imaging system[END_REF].

The second method makes use of permanent magnets to create the appropriate magnetic field and they are moved around the patient using a robotic system to displace the manipulated object [START_REF] Tognarelli | Magnetic propulsion and ultrasound tracking of endovascular devices[END_REF], [START_REF] Ciuti | Robotic magnetic steering and locomotion of capsule endoscope for diagnostic and surgical endolumial procedures[END_REF]. On some of these systems, the "driving permanent magnet" is constantly rotating [START_REF] Mahoney | Control of untethered magnetically actuated tools with localization uncertainty using a rotating permanent magnet[END_REF], [START_REF] Lien | Magnetic control system targeted for capsule endoscopic operations in the stomachdesign, fabrication, and in vitro and ex vivo evaluations[END_REF].

Existing work (Table I) shows that the two approaches are complementary.

The stationary electromagnets approach has full dexterity. However the electrical consumption (associated to heat

The authors are with the FEMTO-ST Institute -UMR CNRS 6174 -AS2M department (Automatic control and Micro-Mechatronic Systems) -24 rue Alain Savary, 25000 Besancon (FRANCE). I: Some pros and cons of magnetic manipulation techniques (from [START_REF] Véron | Advocacy for multi mobile coil magnetic manipulation in active digestive endoscopy[END_REF]) concerns) becomes high as the capsule evades from the sources. Conversely, the mobile magnets approach does not need electrical energy to generate the field, but the use of a constant field is intrinsically unstable (since the capsule is always attracted by the magnet, which can not be "turned off") and offers only partial dexterity (because the continuity of motion is much more restrictive, with respect to time, than the continuity of the magnetic flux).

Our concept, depicted in Fig. 1, consists of several coils actuated by a robotic system so that they can move around the patient and stay close to the capsule. Hence, it keeps full dexterity by making use of coils while reducing energy consumption by a nearer manipulation. Moreover, the robotic system, yet to be properly designed, can be made lighter and less bulky than the existing prototypes, in order to be intrinsically safe to the patient. Recently, we proposed in [START_REF] Véron | Advocacy for multi mobile coil magnetic manipulation in active digestive endoscopy[END_REF], [START_REF] Véron | Magnetic manipulation with several mobile coils towards gastrointestinal capsular endoscopy[END_REF] an hybrid approach by using multiple mobile coils in order to control the motion of a magnetic capsule by both servoing the currents and moving the magnetic sources. Modification of the magnetic field then becomes possible mechanically and electrically. A redundant system is therefore created which increases manipulability and dexterity. To verify this ability we study the control of such system.

However, the complexity of this system is prone to singularities [START_REF] Véron | Magnetic manipulation with several mobile coils towards gastrointestinal capsular endoscopy[END_REF]. This paper contributes to show that the usual condition number is not enough for a reliable detection of such singularities and to propose, as an additional criterion, the use of the angles between the columns of the "manipulation matrix" which models the current-to-force conversion. These angles are used to determine the acceptability of a reference trajectory, which is shown by simulating a multi mobile coils system and a Helmholtz like set-up.

This paper is organized as follows. Section II presents the theoretical background for magnetic manipulation and singularity analysis, while Section III focuses on the study of a particular case. Then Section IV presents the application of this theory by simulating two planar manipulation systems. Conclusion and perspectives are given in Section V.

II. A HYBRID APPROACH TO MAGNETIC MANIPULATION

A. Basic electromagnetics seen from a robotics viewpoint

The motion of the capsule is driven by the efforts applied on it. These efforts are due to the magnetic field created by each coil (the magnetic force F m,i and torque C m,i ), the weight of the capsule (m g), and friction force F f and torque C f . All these efforts and accelerations are expressed in F 0 , a fixed reference frame which can be attached to the patient, to the perception system, or to the patient's bed. F ob j is the local frame linked to the moving object. The notation i X used in the rest of the paper points out in which reference frame F i the vector X is expressed. If nothing is specified, the vector is expressed in F 0 .

The magnetic efforts applied on a permanent magnet located at the point P with a magnetization vector M (which encompasses the magnet strength and its orientation in space) in an external magnetic field B i (P) created by a coil i, are given by [START_REF] Jackson | Classical electrodynamics[END_REF]:

F m,i = V • ∇ (M • B i (P)) (1) C m,i = V • M ∧ B i (P) (2)
where V is the volume of the permanent magnet, ∇ is the gradient operator and ∧ is the cross-product.

As electromagnets are used, the magnetic field created by the ith coil also depends on the current I i flowing through this coil. Then B i (P) = B i (P, I i ). Moreover, computing the magnetic field due to a coil i is usually easier in the frame F i attached to this coil, but this formula can also be easily expressed in the reference frame F 0 using the homogeneous matrix 0 [T ] i multiplication, composed of the orientation and position of F i with respect to F 0 :

B i (P, I i ) = 0 [T ] i i B i ( i P, I i ) (3)
In vacuum, air, or any linear magnetic medium, the superposition principle is used to compute the overall magnetic field created by the n coils. As shown in [START_REF] Kummer | Octomag: An electromagnetic system for 5-dof wireless micromanipulation[END_REF], in such a case, forces and torques can be computed as a linear combination of the currents in the coils, grouped in the vector I. For a system with n coils, the direct electro-magnetic model is then given by:

[A(P, M)] I = F m C m (4)
By construction, the electro-magnetic manipulation matrix, or simply the "manipulation matrix", [A] depends on: the position of the capsule P, the orientation of the capsule (which can be deduce from M), and the position of each coil 0 [T ] i .

Moreover, [A] depends non-linearly on P and I which does not guarantee that even for simple set-ups (e.g. Helmholtzlike configuration), it will never be singular.

Finally, the three possibilities to control the efforts applied to the capsule appear in this matrix modelling. The first control method is to change the coils position which will modify the matrix [A], the second method is to change the currents in the coils, and the third one is the hybrid one we proposed.

Notice also that [A] can be decomposed as:

[A] = A F A C (5)
[A F ] and [A C ] are two 3 × n matrices, and the product of these matrices by the vector of currents I gives respectively the magnetic force F m and the magnetic torque C m .

B. Study of the singularities

The matrix [A] is a 6×n matrix, with n the number of coils, i.e. the number of independant currents. The ith column of this matrix represents the wrench on the capsule (force and torque) per current unit created by the ith coil, according to (1) and (2). Thus, [A] has the same structure as a robot kinematic Jacobian matrix. The analysis of its singularities is thus needed.

Numerically, singularities are detected by computing the rank of the matrix (usually, by detecting the fall of the ratio of successive singular values). This is actually related to the condition number of the matrix:

Cond([A]) = σ 1 σ N with σ 1 σ 2 • • • σ N > 0, the singular values of [A]
obtained by singular value decomposition (SVD). The condition number is frequently used as a so-called manipulability index [START_REF] Merlet | Jacobian, manipulability, condition number and accuracy of parallel robots[END_REF] to measure the performance of a mechanism. However, in addition to the specificities of the special euclidean group SE(3), this index suffers from the fact that one needs an empirical choice of the threshold value to decide the closeness of the rank deficiency. Unfortunately, this threshold on the ratios of two successive singular values does not have a physical interpretation.

On the opposite, for such kinematic matrices, whose dimensions are 6 × n, one can express the singularities from geometry. A geometrical analysis relies on the fact that if [A] is non-singular, a subset of columns which spans the whole space (ie. of dimension 6) exists.

In practice, the relative orientation of each column to each other has a great importance. Indeed, if all these columns are almost collinear, without [A] being singular, the necessary energy to move in a "transverse" direction (see Fig. 2) is much higher than in an ideal case (a subset of the columns forming an orthogonal base). are parallel (i.e. α i, j = 0), but a non-singular case with small angles (let us say 5 or 10 deg) between the columns of [A F ] may also cause significant problems in practice. At right angles, the manipulability is good, because the energy transfer is decoupled. At small angles, it is poor, as more energy is needed to move the capsule in the "transverse" direction (Fig. 2) than in the "common" direction. This is particularly prevalent in magnetic manipulation, because at small angles, one would need higher currents in the coils than at angles almost equal to π/2 rad. Since "higher currents" means a risk of current saturation as well as heating in the coils, this situation should be avoided. As a consequence, the analysis of the evolution of the angles α i, j (between the ith and the jth column vectors of the matrix [A F ]) can be used to check if the trajectory is acceptable, i.e. the trajectory does not encounter a singularity of [A].

III. STUDY OF A PARTICULAR CASE

A. Description Fig. 3: System studied.

The proposed criteria is investigated in the horizontal planar configuration. Thus, the study is carried on a system (presented in [START_REF] Véron | Magnetic manipulation with several mobile coils towards gastrointestinal capsular endoscopy[END_REF]) with n = 3 coils, and the capsule can move in the plane made by the coils axis as shown on Fig. 3.

The architecture shown is similar to a 3-UPS parallel kinematic manipulator. The coils can turn around a vertical axis (O i , Z) in order to keep the mobile on their axis of revolution. This architecture was chosen to be able to use the well-known magnetic dipole approximation [START_REF] Wang | Study on magnetic localization and actuation of active capsule endoscope[END_REF] often used in literature to compute the magnetic field i B i ( i P, I i ). This approximation is only valid when the distance between P and the coil axis is small.

i B i ( i P, I i ) =      B r = µ 0 2 π (I i • π a 2 ) cos θ r 3 B θ = µ 0 4 π (I i • π a 2 ) sin θ r 3 B ϕ = 0      (6)

B. Modeling

As the system is studied in the horizontal plane, P, M and B i (i = 1, 2, 3) are coplanar. Thus, the generic form of the matrix [A] becomes:

[A] =         F 1x F 2x F 3x F 1y F 2y F 3y 0 0 0 0 0 0 0 0 0 C 1z C 2z C 3z         (7)
which can be reduced, as previously mentioned, by suppressing the rows of 0.

The geometrical analysis is then reduced to the study of the angles α i, j between 2D column vectors of [A F ] (the upper two rows of [A]).

IV. SIMULATION RESULTS

A. Simulation set-up

A simulation in C++ using the ViSP library [START_REF] Marchand | Visp for visual servoing: a generic software platform with a wide class of robot control skills[END_REF] has been developed. The trajectory control, based on the structure shown in Fig. 4, is computed. With this control strategy, the orientation control and the current control are independent. The trajectory tracking block is a PD plus feed-forward controller that provides the desired acceleration (a * , ω * ) for the capsule from the difference between its measured (P, M) and reference position (P * , M * ). To determine the current I needed to ensure (a * , ω * ), the dynamic model of the capsule is used:

[A(P, M)] I = m • a 0 [I G ] ob j • ω - F f C f (8)
where m is the mass of the capsule, 0 [I G ] ob j its inertia, F f and C f the friction efforts, and a and ω the acceleration. This model is inverted by singular value decomposition to calculate the current I applied into the coils. It is implemented in the block called Inverse Dynamic Model in Fig. 4.

B. Results

First, the simulation is ran without any friction (F f = C f = 0) or measurement noise. The simulated system includes three coils with 930 turns placed at 2π/3 rad on a circle of 75 mm radius, and a capsule which mass is 10 g. On Fig. 5 the desired trajectory P * , a 40 mm long straight line, and the realized trajectory are displayed. They match very accuratly, with a maximal error of 2.19 • 10 -5 mm in position and 1.69 • 10 -7 rad in orientation. This correspond to the numerical round-off errors.

Moreover, the currents flowing through the coils to realize this trajectory are shown on Fig. 7 and do not exceed 0.35 A. Consequently, we can conclude that the trajectory is physically admissible.

Now, let us observe the angles between the columns of [A F

] along this trajectory. Fig. 8 shows that, as expected, during the whole trajectory, there is always at least one of the angles which is close to π/2 rad. This means that the algorithm is always able to construct a base for the forces in the horizontal plane, and thereby to find a linear combination that gives the desired effort. Moreover, the simulation did not encounter any loss of rank of the matrix [A], which is also normal for a properly planned trajectory. However the two angles come close to π, meaning that two columns align. However, executing the simulation for different trajectories led us to find that some of them induce a loss of control. This is illustrated on Fig. 9a and9b, where the desired trajectory is the same trajectory as the first one, but this time with the capsule orientation perpendicular to the direction of the trajectory. Notice that the control is lost on the orientation. Furthermore, the currents applied to the coils become very high where the control is lost (Fig. 10) which means that this trajectory is not admissible.

The trajectory was realized with several values of ε, the detection threshold of the rank. Note that in the first case (ε = 10 -3 Fig. 11a) the loss of rank of the manipulation matrix [A] happens before any loss of control, and in the second case (ε = 10 -6 Fig. 11b) the loss of rank is not detected until the control is lost. This highlights that the rank is not a sufficient criteria. On the contrary, Fig. 12a shows a sudden decrease of the angles between the direction of the forces from each coil. At t = 33.36 s, the starting time of the control loss, the three angles are equal to 0 (Fig. 12b).

In such a case, the three coils can only create a force along the same direction, which actually is orthogonal to the desired trajectory. This fully explains why the current dramatically increase (see Fig. 10 and Fig. 13), yielding unstabilities. To avoid these unstabilities one can define a margin on the angles related to the maximum current admissible by the system (see Fig. 13).

C. Discussion

Conventional devices for magnetic manipulation found in the literature (as [START_REF] Ivan | First experiments on magpier: a planar wireless magnetic and piezoelectric microrobot[END_REF]) are most of the time composed of four fixed coils, which are placed in a configuration similar to the Helmholtz one (face to face in pairs). A simulation of such a system was done and the analysis of the angles α i, j between the columns of the matrix [A F ] (whose dimension is 2 × 4 in this case) was conducted on this system. We see that trajectories with singularities on these angles are unusual for this kind of system. Most of the time, the singularities encountered are due to a loss of rank, and the perturbation ensuing such a singularity may not induce a strong loss of control. Yet, having found this non-admissible trajectory confirms the need of a proper singularity analysis in magnetic manipulation, whatever the configuration. A non-admissible trajectory is displayed Fig. 14. Similarly to the previous simulation, a sudden decrease happens on the angles α i, j (Fig. 15b) at the moment of the control loss (t = 25.96 s). This highlights the relevance of this analysis, and attests that it can be applied to different kind of systems (with mobile or fixed coils).

V. CONCLUSIONS AND PERSPECTIVES

This paper studies the manipulability for manipulation systems based on multiple mobile coils. A geometrical analysis allows to check if planned paths are acceptable or not.

This geometrical analysis comes in addition to a more classic numerical criterion (the condition number of the matrix), which is a necessary but insufficient condition. The geometrical criterion easily defines a margin on the angles to ensure the controllability of the system. These results have also been confirmed for magnetic manipulation systems with Helmholtz-like fixed coils.

This study on the angles α i, j is a first interesting approach. However, it is not enough; one must also ensure that the norm of each column is not too low. Indeed, as a column represents the wrench per current unit, a low norm would imply high currents in the coils. A more complete study is being led in order to determine a manipulability criterion adapted to multi mobile coils systems.

Finally, this study reveals that magnetic actuated devices are subject to constraints that may be non-holonomic constraints. One perspective of this work is then the trajectory planning for magnetic manipulation systems.

Fig. 1 :

 1 Fig. 1: Robot-assisted magnetic manipulation with several mobile coils.

Fig. 2 :

 2 Fig. 2: "Transverse" direction.

Fig. 4 :

 4 Fig. 4: Control strategy inspired by Parallel Kinematic Machine (PKM) with linear actuators.

Fig. 5 :Fig. 6 :

 56 Fig.5: Position followed by the capsule (plain). The desired trajectory (dashed) is a straight line, the * is the starting point, and the magnetization is in the same direction as the trajectory.

Fig. 7 :

 7 Fig. 7: Currents inside the coils during the trajectory Fig. 5.

Fig. 8 :

 8 Fig. 8: Angles between the direction of the force created by each coil during the trajectory Fig. 5.

Fig. 9 :

 9 Fig. 9: (a) Position followed by the capsule (plain). The desired trajectory (dashed) is a straight line, the * is the starting point, and the magnetization is perpendicular to the trajectory. (b) Tracking error during the trajectory.

Fig. 10 :

 10 Fig. 10: Currents inside the coils during the trajectory Fig. 9a.

6 Fig. 11 :

 611 Fig. 11: Rank of the matrix [A] during the trajectory Fig. 9a.

Fig. 12 :Fig. 13 :

 1213 Fig. 12: (a) Angles between the direction of the force created by each coil during the trajectory Fig. 9a. (b) Zoom in.

Fig. 14 :

 14 Fig. 14: Simulation output for a 4 fixed coils system.

Fig. 15 :

 15 Fig. 15: (a) Angles between the columns of the matrix [A F ] during the trajectory Fig. 14. (b) Zoom in.

TABLE

ACKNOWLEDGMENT

The authors would like to thank Pierre Renaud, Xavier Weber and Lucas Perdrix for the design of the robotic system seen in Fig. 1. This work was partly supported by the French ANR Labex ACTION ("ANR-11-LABX-01-01").


Vincent Cremet

François Garillot

Sergueï Lenglet

Martin Odersky

A Core Calculus for Scala Type Checking

We present a minimal core calculus that captures interesting constructs of the Scala programming language: nested classes, abstract types, mixin composition, and path dependent types. We show that the problems of type assignment and subtyping in this calculus are decidable.

Introduction

The programming language Scala proposes a new model for component systems [START_REF] Odersky | Scalable component abstractions[END_REF]. Components in this model are classes, which can be combined using nesting and mixin composition. Classes can contain abstract types which may be instantiated in subclasses. The Scala component model thus provides a single framework for the construction of objects and modules. Modules are identified with objects, functors with classes, and signatures with traits.

The advantage of this approach is that a single fairly small set of language constructs is sufficient for core programming as well as the definition of components and their composition. Furthermore, the identification of modules and objects provides new ways to formulate standard programming tasks such as the expression problem [START_REF] Garrigue | Code reuse through polymorphic variants[END_REF][START_REF] Torgersen | The expression problem revisited: Four new solutions using generics[END_REF][START_REF] Odersky | Independently extensible solutions to the expression problem[END_REF] and family polymorphism [START_REF] Ernst | Family polymorphism[END_REF][START_REF] Odersky | Scalable component abstractions[END_REF].

Scala's approach to component modeling is based on three programming language constructs: modular mixin composition, abstract type members, and explicit self-types. All three have been studied in the νObj calculus [START_REF] Odersky | A nominal theory of objects with dependent types[END_REF]. A key concept of the νObj calculus, path-dependent types, is also present in Scala. However, some other constructions of νObj do not correspond to Scala language constructs. In particular, νObj has first-class classes which can be passed around as values, but Scala has not.

First-class classes were essential in establishing an encoding of F <: in νObj, which led to a proof of undecidability of νObj by reduction to the same property in F <: [START_REF] Pierce | Bounded quantification is undecidable[END_REF]. However, since Scala lacks first-class classes, the undecidability result for the calculus does not imply that type checking for the programming language is undecidable.

In this paper, we study the problem of decidability of Scala type checking. We construct (algorithmic) Featherweight Scala, abbreviated FS alg , a minimal core calculus of classes that captures an essential set of features of Scala's type system. Classes can have types, values, methods and other classes as members. Types, methods, and values can be abstract. The calculus is designed to be syntactically a subset of Scala (with the deviation of explicit self-names, explained below). Its typing rules correspond closely to the ones implemented in the Scala compiler.

An important aim in developping Featherweight Scala was to show that Scala's core type-checking rules are decidable. One particular problem in this respect are cyclic definitions that relate members of different classes. Featherweight Scala allows cyclic references between members of different mixin classes. Because cycles cannot be ruled out by construction, they have to be detected by the type checker. The typing rules achieve this by keeping track of the sets of definitions that have already been visited in a typing proof. This gives the calculus an algorithmic flavor, hence the name FS alg .

All presented deduction rules are syntax-directed and thus lead directly to procedures for subtyping and type assignment. The central result of this paper is that these procedures are algorithms, i.e. that they terminate in each case.

Related Work: Scala's component constructions provide a middle ground between the worlds of object-oriented programming and functional module systems [START_REF] Harper | A type-theoretic approach to higher-order modules with sharing[END_REF][START_REF] Leroy | A syntactic theory of type generativity and sharing[END_REF]. Many of the concepts in both worlds are unified. Mixin composition in Scala borrows from mixinmodules [START_REF] Ancona | A primitive calculus for module systems[END_REF][START_REF] Ancona | A calculus of module systems[END_REF][START_REF] Hirschowitz | Mixin modules in a call-by-value setting[END_REF], as well as from the more linear object-oriented mixin composition [START_REF] Bracha | Modularity meets inheritance[END_REF][START_REF] Bracha | The Programming Language Jigsaw: Mixins, Modularity and Multiple Inheritance[END_REF]. Components in Scala can be mutually recursive, a property which is also addressed by work on recursive modules [START_REF] Crary | What is a recursive module?[END_REF][START_REF] Nakata | Recursive object-oriented modules[END_REF]. Abstract types in Scala are also present in SML style signatures [START_REF] Leroy | A syntactic theory of type generativity and sharing[END_REF][START_REF] Harper | A type-theoretic approach to higher-order modules with sharing[END_REF], and correspond almost exactly to virtual classes in Beta [START_REF] Madsen | Object-Oriented Programming in the BETA Programming Language[END_REF].

Later work on virtual classes [START_REF] Ernst | gBeta: A language with virtual attributes, block structure and propagating, dynamic inheritance[END_REF][START_REF] Ernst | A virtual class calculus[END_REF] is more general in that classes, and not just types, can be abstract. However, references to abstract types in [START_REF] Ernst | A virtual class calculus[END_REF] can only refer to members of an enclosing "self", not to members of an arbitrary path. Several other variations on virtual types [START_REF] Torgersen | Virtual types are statically safe[END_REF][START_REF] Igarashi | Foundations for virtual types[END_REF][START_REF] Nystrom | Scalable extensibility via nested inheritance[END_REF] and some alternative proposals [START_REF] Bruce | A statical safe alternative to virtual types[END_REF][START_REF] Rémy | On the (un)reality of virtual types[END_REF][START_REF] Bruce | Some challenging typing issues in object-oriented languages[END_REF][START_REF] Jolly | Simple dependent types: Concord[END_REF] have also been researched. Typed class-based calculi for describing Scala's static analysis are described in [START_REF] Altherr | Inner Classes and Virtual Types[END_REF] and [START_REF] Altherr | A Typed Intermediate Language and Algorithms for Compiling Scala by Successive Rewritings[END_REF] but the authors do not address the problem of their decidability.

The focus in the paper is on a minimal calculus that captures the essential features of an existing programming language. In this motivation it follows the work on Featherweight Java [START_REF] Igarishi | Featherweight Java: A minimal core calculus for Java and GJ[END_REF]. Both calculi model a simple, purely functional core language of objects with fields and methods in a nominal class-based type system. They also take some similar shortcuts in the interest of conciseness. For instance, both assume call-by-name evaluation in order not to have to deal with the thorny initialization issues of their underlying languages. However, the set of more advanced language constructs that are modeled are different in each case. Featherweight Java models type casts, and has extensions that model generics as well as inner classes [START_REF] Igarashi | On inner classes[END_REF]. Featherweight Scala models inner classes, member type abstraction, as well as path-dependent types. It can also model most of the generic constructs in FGJ [START_REF] Igarishi | Featherweight Java: A minimal core calculus for Java and GJ[END_REF] via encodings.

The rest of this paper is structured as follows. Section 2 explains Scala's model of abstract types and path dependent types from a programmer's perspective. Section 3 introduces the Featherweight Scala calculus FS alg . Section 4 shows that subtyping and type-assignment are decidable in this calculus. Section 5 relates the obtained results to the situation in the Scala language. Section 6 concludes.

Programming in Featherweight Scala

Featherweight Scala is a fairly small subset of Scala, but it is expressive enough for one to write meaningful programs in it. In the following, we show how some common classes and programming idioms can be encoded in the calculus.

Peano Numbers. We start with an encoding of Peano numbers, shown in Figure 1. This encoding presents a trait Nat with five member methods. Methods isZero and pred are abstract, that is, they lack an implementation in trait Nat. By contrast, methods succ, add and subtract are concrete. A trait in Scala is an abstract class which may be combined with other traits using mixin composition.

References from one member of a Nat object to another always go via the "self" reference of the class. The name of the self-reference is given after the opening brace of the class body. In the example above it is this0. The name can be freely chosen, but in the examples in this paper we always use thisN, where N is the nesting level of the enclosing class. As a shorthand notation we sometimes omit the definition of a self-name which is never used in the class body that follows.

Class Nat also contains a nested class Succ which defines the successor value of the current object this0. This class is an extension of Nat, which gives concrete definitions for the two abstract members of Nat: isZero returns always false and the predecessor method pred always returns the self-reference of the outer Nat class.

The successor method succ simply creates a new instance of the Succ class and returns it. Note that Featherweight Scala allows instance creation expressions such as new Succ {} only as right-hand sides of value definitions; that's why we were forced to define in the body of succ an intermediate value result. Regular Scala does not have this restriction, and also provides many other shorthands that would make the example more pleasant to write and read.

The final two methods, add and subtract, define addition and subtraction in terms of the previous three methods. Their implementation uses standard syntax for field selection, method calls, and recursion.

Figure 1 also gives a definition of the zero value for Peano numbers. This value is defined as a direct specialization of class Nat, which also defines the natural implementations of Nat's abstract methods isZero and pred. The right-hand side of zero's definition combines a definition of a new anonymous class and a creation of an instance of this class in a single syntactic construct. Alternatively, one could also proceed in two steps, by defining a subclass Zero of Nat, and then creating an instance value val zero = new Zero {}.

The preceding example used exclusively the constructs of the Featherweight Scala calculus, with two exceptions: First, we assumed a type Boolean with values true and false and a if-then-else construct. Second, we assumed an error function which aborts a program with a given error message.

In the example we have also taken some liberty in presenting top-level definitions for Nat and zero. By contrast, a Featherweight Scala program is simply an expression, which typically contains embedded definitions for classes and values. To get a complete program which computes 2+2 one could combine the program fragments in Figure 1 The element type of a given list is represented by the type member Elem of class List. The member is defined as an abstract type in class List. Hence, when a List object is created, a concrete implementation of this type has to be provided. For instance, the definition val nilOfNat = new Nil { type Elem = Nat } defines a value nilOfNat as an empty list with element type Nat. The type alias type Elem = Nat is used to "fill in" the abstract type member Elem that Nil inherits from List.

The List class also contains a type alias which defines ListOfElem as a type name for lists whose element type is the same as the element type of the list in question. This alias does not implement an abstract type member in a parent class; it is there only for convenience.

The List class also defines a test method isEmpty, as well as methods which return the head and tail of a list. Method head returns values of type Elem whereas tail returns values of type ListOfElem. All three methods are abstract in class List.

The subclass Nil of List represents empty lists. It defines method isEmpty to return true. Selecting the head or tail of an empty list always results in an error.

The subclass Cons of List represents nonempty lists. The head and tail of a nonempty list are kept in the fields hd and tl of class Cons. Scala uses val for a definition of a local value or a field of a class, whereas def is used for a method definition. Classes in Featherweight Scala do not have constructors; however, one can use member-redefinition to initialize the values of an object. For instance, the following code defines two lists of element type Nat which contain the values (2) and (1, 2), respectively.

val list2 = new Cons { this0 | type Elem = Nat val hd : Nat = zero.succ().succ() val tl : this0.ListOfElem = nilOfNat } val list12 = new Cons { this0 | type Elem = Nat val hd : Nat = zero.succ() val tl : this0.ListOfElem = list2 }
The List example showed how genericity can be encoded using abstract types. In fact, there is a general encoding that lets one encode all forms of parameterized types in Scala into types with abstract members. Details are found in [START_REF] Altherr | A Typed Intermediate Language and Algorithms for Compiling Scala by Successive Rewritings[END_REF]. Class Function gives an interface for functions with arbitrary domain and range types. The interface specifies two abstract types Dom and Range as well as an method abstract method apply that takes arguments of type Dom and that yields results of type Range.

A first-class functional value is then a concrete implementation of class Function, which gives types for Dom and Range as well as an implementation for method apply. As an example, Figure 4 presents a map function which applies a given argument function to all elements of a given list and returns a list consisting of all the results of these applications. In regular Scala, this function would be defined as follows:

def map[A, B](f : A ⇒ B, xs : List[A]): List[B] = if (xs.isEmpty) Nil else f(x.head) :: map(f, xs.tail)
Since map is conceptually a polymorphic method, its encoding in Featherweight Scala makes use of a wrapper class Mapper which defines two abstract types A and B, representing the element types of the argument and result lists, respectively. The map method in Mapper takes as arguments a function f from type A to type B, and a list xs of element type A. It returns a list of element type B. An application of map would be written as follows:

val list23 = new Mapper { type A = Nat; type B = Nat }.map(inc, list12)
This instantiates the Mapper class with type Nat as the element type of the argument and result list, and invokes the map method of the instantiation with inc and list12 as arguments. The expression would return the encoding of the list (2, 3).

The example shows that monomorphic functions such as inc can be first-class values. However, the construction cannot be generalized to polymorphic functions. The reason is that polymorphic functions like map have to be encoded using wrapper classes. Such wrapper classes are first-class values neither in Featherweight nor in regular Scala. By contrast, the νObj calculus has classes as first class values, and therefore can encode polymorphic functional values.

The Algorithmic Featherweight Scala Calculus

The FS alg calculus aims at describing some central aspects of the Scala type system in a simple and formal way. The features whose study has been privileged in this work are: method overriding, mixins, inner classes, virtual types, singleton types and types with member refinements. The calculus does not model objects with state and has no concept of type parameters in classes or methods. Genericity can be encoded using types with member refinements.

Syntax

The abstract syntax of FS alg is given in Figure 5. Amongst the names occurring in a program, we distinguish the variables that are used as binders for objects and can be α-conversed, the value labels that designate the members defining a field or a method, and the type labels that designate the members defining a class or a virtual type.

A member can be a value field, a method, a type field or a class. A value field is immutable and refers to an object. The types of value fields, method parameters and method results must be given explicitly. Value fields and methods can be either concrete or abstract. A declaration is called abstract if the right-hand side is absent. For instance, a declaration like val n a : T = t defines a concrete field a with value t, whereas the field declaration val n a : T is abstract. In order to factorize abstract and concrete declarations we use the notation val n a : T (= t)

? . Type fields are also either concrete or abstract, a concrete type field being sometimes called a type alias. A class member trait n A extends T ϕ | M declares a class A with parents T and members M , the variable ϕ denotes the current instance of the class. Class members cannot be abstract.

Every occurrence of a declaration in a program is tagged with a unique integer n. This integer has no computational meaning, it is simply used for detecting cycles during the static analysis.

The terms of the calculus are standard. A variable x can represent the current instance of a class, a method parameter, or the name of an object which has been created locally. Field selections and method calls have the same syntax as in Java. The construct val x = new T ; t allows the user to define a new instance of the type T , with a name x whose scope is limited to the term t.

A FS alg program is simply a term, which is usually of the form

val z = new ϕ | M ; t .
It consists of a list of member declarations M that together make up a universe object z and a main term t to be evaluated in the context of z. The variable ϕ is an alias of z; it represents the self reference of the universe object which contains all top-level declarations. We distinguish a subcategory of terms that can be used inside types, and that we call paths. A path is either a variable or the selection of a field on a term that is itself a path. The introduction of paths is motivated by their property of always evaluating to the same object value and of being strongly normalizable. Both properties are needed if we want type soundness to hold. However, this goes beyond the scope of the present paper.

Σ ⊢ T ≺x M Σ ; val x = new T ; t → Σ, x : M ; t (red-new) Σ ; t → Σ ′ ; t ′ Σ ; e[t] → Σ ′ ; e[t ′ ] (red-context) Lookup ∀ i, Σ ⊢ Ti ≺ϕ Ni Σ ⊢ `T ´˘ϕ | M ¯≺ϕ `Ui Ni ´⊎ M (lookup-sig) traitnA extends `T ´˘ϕ | M ¯∈ Σ(y) Σ ⊢ `T ´˘ϕ | M ¯≺ϕ N Σ ⊢ y.A ≺ϕ N (lookup-class) type n A = T ∈ Σ(y) Σ ⊢ T ≺ϕ M Σ ⊢ y.A ≺ϕ M (lookup-
Our calculus has a rich syntax of types. A type selection p.A is either a class type if A is a class label, a virtual type if A is an abstract type label, or an alias type of A is a concrete type label. A class type p.A has as values all instances of class A whose enclosing instance associated with A is the object denoted by p. Virtual and alias types p.A have a rather different meaning: they represent the type held by the type field A in the object p. A singleton type p.type represents the type of which p is the unique element. Finally, a type signature T ϕ | M combines the concepts of intersection types and member refinements: it represents the intersection of types T with additional constraints on members expressed by declarations M .

Operational semantics

Figure 5 contains the inference rules that define a small-step operational semantics for our calculus. It is composed of a reduction relation and a lookup relation. Both relations use the concept of evaluation environment Σ, which is a list of bindings x : M that associates an object name x with its set of members. The reduction relation Σ ; t → Σ ′ ; t ′ reduces t to t ′ in the environment Σ. The reduction of a term can imply the creation of new objects that are added to the environment, leading to a new environment Σ ′ . The lookup relation Σ ⊢ T ≺ ϕ M collects all declarations M in a type T . Together with the concept of evaluation context for terms and types, the rule red-context lets us reduce inside a term. The evaluation of a program val z = new ϕ | M ; t consists in repeatedly reducing the term t in the environment context z : [z/ϕ]M until reaching a term that is a value, i.e. a variable y. Such a semantics is needed if we want to state and prove a theorem of type safety. Note that in this semantics the value attached to a field member is re-evaluated each time the field is selected, which corresponds to a call-by-name semantics.

Type system

The type system of FS alg is described by an algorithmic system of inference rules. In such a system, any judgment is matched by the conclusion of at most one rule, which means that the application of rules is completely deterministic. Typing FS alg requires the definition of several auxiliary judgments about types in addition to the classical judgment that assigns a type T to a term t: membership (S, Γ ⊢ T ∋ M ), subtyping (S, Γ ⊢ T <: U ), expansion (S, Γ ⊢ T ≺ ϕ M ) and type well-formedness (S, Γ ⊢ T wf). Most of the judgments are parameterized by a typing context S, Γ , where S is a set of indices representing locked declarations, and Γ is a set of bindings x : T between variables and types such that all variables x are pairwise distinct.

Type assignment. The first two boxes of Figure 6 present the judgments that assign types to terms. The judgment S, Γ ⊢ t : T always assigns the most precise type to a term, in particular a path p always receives the type p.type according to this judgment, provided it can be assigned a bound T (rule path). A field selection t.a is typable if it is possible to type t and to establish, using the membership judgment, that the type S of t contains a field declaration val n a : T (= u)

? ; in this case type T is assigned to the selection t.a (rule select). Note that this rule is only applicable if t is not a path. In case t is a path p, we fall back to rule path. Rule method allows to type method calls s.a t : the type of s must contain a declaration for the method a, and each argument must have a type which is compatible with the one required by the method declaration, i.e. which is a subtype of the expected type. If these conditions are fulfilled, the type announced by the method declaration is given to the term s.a t . Finally, rule new allows the typing of a local object creation val x = new T ; t. Such a term gets the type of t if several conditions are satisfied. The members declared inside type T must be concrete: the expansion judgment S, Γ ⊢ T ≺ ϕ M returns all the member declarations M of a type T such that x represents the self reference. The type T must be well-formed. The term t must be typable in the environment Γ extended with the binding x : T . Finally, because the scope of x is limited to t, the variable x must not appear in the type S of t.

The judgment S, Γ ⊢ path p : T is a typing judgment specialized for paths. Contrary to the previous judgment, it does not always return the singleton type p.type for a path p. Rather, it returns the less precise but more informative type associated with it, called its bound. If p is a variable x, its bound is the type associated with x in the environment (rule path-var), if p is a selection p ′ .a, its bound is the declared type T of a as seen from p ′ (rule path-select).

Membership and expansion.

In FJ [START_REF] Igarishi | Featherweight Java: A minimal core calculus for Java and GJ[END_REF], there is a lookup relation that computes the most precise signature of a method visible from a given class. In FS alg the member judgment S, Γ ⊢ T ∋ M presented at the bottom of Figure 6 generalizes this relation to the computation of any kind of declaration (not just methods) visible from any kind of type (not just class types). In FJ the lookup relation is quite simple, it returns the signature of the method as it appears in the program; in FGJ, since classes can have type parameters and since a member signature can refer to some type parameters of its enclosing class, the lookup relation requires also the computation of type values for such type parameters. In FS alg , things are more complicated: because types depend on paths, the signature of a member can depend on the self reference x of its enclosing class, or more generally on the self reference of any enclosing class, direct or indirect. Thus, the result of the lookup must replace x with the actual value of the enclosing instance. To illustrate this, suppose we have a method declaration def n a () : x.A in a class C where x is the self reference. If the starting type T of the membership judgment is a singleton type p.type, then it is possible to replace x with p and obtain p.A. But if the starting type T is a class type q.C, then the lookup fails because there is no available instance of C with which to replace x. However, if the signature of a does not depend on x (for instance if the return type of a is an external type root.Int), then the lookup succeeds, even from q.C (because in root.Int there is no self reference to be replaced). Rules ∋singleton and ∋-other respectively implement the situation where the starting type T is a singleton type and where it is not. In the first case, the path p is first expanded into q with the path alias expansion judgment. Then, we take the type T of q which, by construction, is not a singleton type. Using the type expansion judgment we collect all declarations M of T and we substitute p for the self reference ϕ in the declaration we are interested in. In case the starting type T is not a singleton type, we can immediately collect its declarations, but we have to check that the declaration we are looking for does not contain the self reference ϕ.

The type expansion judgment S, Γ ⊢ T ≺ ϕ M (third box of Figure 6) collects all declarations M of a type T where ϕ is used to represent the self reference inside declarations M . The expansion of a class type p.A is the expansion of the type signature T ϕ | M composed of its parents T and its direct members M (rule ≺-class). The index n of the class is added to the set S of locks in order to avoid falling into an infinite expansion (for instance if a class extends itself). Rule ≺-type is completely analogous. It expands a type alias while performing the same actions on locks in order to prevent infinite alias expansion. Finally, rule ≺-signature expands a type signature: it starts by expanding all parents T and then merges all collected declarations N with the direct members M of the type signature. The concatenation with rewriting of common members ⊎ of several sets of declarations is defined by M ⊎ N = M | dom(M )\ dom(N ) , N , where the domain dom(M ) of a sequence of declarations is the set of labels it defines and the restriction M | L of declarations M to a set of labels L consists of all of those declarations in M that define labels in L.

Type and path alias expansion. We introduce here two auxiliary judgments, type alias expansion and path alias expansion that will be used when defining the subtyping judgment. The idea of the type alias expansion judgment S, Γ ⊢ T ≃ U is very simple: we take a type T and if T is a type alias p.A for another type T ′ , we recursively expand T ′ until we reach a type that is no longer a type alias. This simple behavior is formalized by the five rules in the first box of Figure 8.

There exists also a relation of aliasing between paths. For instance, with a field declaration val n a : p.type in a class where x is the self reference, the path x.a has type p.type. Because p.type is a singleton type and x.a belongs to this type, this really means that x.a and p represent the same object, or equivalently that x.a is an alias for p. In this reasoning, we have performed a one-step alias expansion going from x.a to p. The judgment defined at the bottom of Figure 7 implements the complete alias expansion of a path by repeating the operation we have performed in this example. Once again, we prevent falling into a loop by adding an index to the set S of locks (rule ≃-Step). This index is the one of the last field selected in the considered path p. It is computed by the function ψ(p). This function takes as implicit arguments the environments S and Γ and is defined as follows.

ψ(p.a) = n if S, Γ ⊢ p.type ∋ val n a : T (= t) ? ψ(x) = x
The expansion terminates when we reach a path that cannot be given a singleton type (rule ≃-Refl).

Subtyping. The subtyping judgment S, Γ ⊢ T <: U (central box of Figure 8) is used to compare two types T and U . In theory, such a relation must be defined by considering all possible kinds of types for T and all possible kinds of types for U . But in practice it is possible to factorize and eliminate a great number of cases. First we expand both types into types T ′ and U ′ (rule <:-unalias). This simple operation allows to quickly eliminate all cases where T ′ or U ′ is an abstract type p.A, because if a type is still abstract after alias expansion nothing can be said about it. As a consequence, in the auxiliary judgment S, Γ ⊢ * T <: U we assume that T and U are not abstract types. If U is a singleton type q.type, then only another singleton type p.type can be a subtype of it (rule <:-singleton-right), and in this case paths p and q must be equivalent, i.e. they must be aliases for the same path p ′ . If the left-hand side is a singleton type p.type and the right-hand side U is not, then we just take the bound T of p and recursively compare it with U (rule <:-singleton-left). If both types are a selection of the same type label A (rule <:-singleton-left), then their prefixes must be equivalent. Suppose now that the right-hand side is a class type. We just have to consider the cases where the left-hand side is a class type or a type signature. If the left hand-side is a class type p.A then we recursively check that there exists one parent of the class that is a subtype of p ′ .A ′ (rule <:-class). If the left-hand side is a type signature T ϕ | M the procedure is analogous. Finally, we are left with the case where the right-hand side is a type signature T ϕ | M . There are then two things to check: first that the type T is a subtype of all parents T in the type signature, which expresses the fact that a type signature represents the intersection of its parents. And secondly, that type T satisfies the constraints expressed by the declarations M . This is the case if T expands to a set of declarations N , with a greater domain than M , and if the declarations that are common to N and M are more precise in N , which is expressed by the subtyping test between members S, Γ ⊢ N ≪ M .

The subtyping between members is standard (bottom of Figure 8): it is covariant for the types of field declarations and for the result types of methods, contravariant for the method parameter types, and invariant for type and class declarations. The invariance for type aliases is crucial since an alias conceptually represents an equality between types. The member subtyping relation is lifted to sequences of members using the following definitions:

N ≪ N ′ ⇔ ∀(N, N ′ ) ∈ N × N ′ , dom(N ) = dom(N ′ ) ⇒ N <: N ′
Well-formedness. There are two well-formedness judgments: one for types S, Γ ⊢ T wf (top of Figure 7), and one for members S, Γ ⊢ M wf ϕ (top of Figure 7)

For a singleton type p.type to be well-formed, the path p must be typable (rule wfsingleton). In order to avoid a cyclic dependence between a path and its type, we also check the well-formedness of the bound T of p. Because we do not want to fall into a loop, we extend the set of locked indices with ψ(p). For a class type p.A to be well-formed (rule wf-class), it is sufficient to check that a class named A is accessible from p, which is expressed by a membership judgment starting from the type p.type. For an abstract type p.A, a declaration of the type A must also be visible from p. In addition, if the type is an alias for a type T we also check that T is well-formed. This is needed since we do not want type aliases to let us define recursive types. Such a test serves for detecting illegal cycles, as for the rule wf-singleton. Finally, the well-formedness of a type signature is checked by first putting a binding with the type signature in the environment (rule wf-type).

The well-formedness of fields and methods is standard. For a field declaration the type T ′ of the optional value t must conform to the declared bound T (rule wf-x-field). For a method, the types of parameters S and the method type T must be well-formed in the current environment, which means that the judgment excludes the possibility for the type of a parameter to depend on another parameter. The body t of the method must be typable in an environment extended with the parameters, and its type T ′ must conform to the return type (rule wf-x-method). Note that we require parameter types not to contain singleton types. This restriction has almost no impact on expressiveness and it has the advantage of simplifying the termination proof of path alias expansion. The well-formedness of a type declaration is equivalent to the well-formedness of the type T it is an alias for (rule wf-x-type). Eventual cycles in this definition are detected indirectly by the well-formedness of T . For typing a class declaration (rule wf-x-class) we check the well-formedness of its associated type signature T ϕ | M composed of its parents and direct members, in an environment extended with a binding for the class self reference ϕ. It might be surprising that here we do not check for the absence of cycles in the class hierarchy, but such cycles are actually detected by the well-formedness of the type signature: if a class inherits, directly or indirectly, of itself, there cannot exist an expansion of the parents T . A type signature T ϕ | M (rule wf-x-signature) is well-formed w.r.t. a self reference ϕ if the T can be expanded, which forbids singleton types and abstract types in the parents of a signature, and if all new members of the type, directly present in M , are compatible. The compatibility of a list of groups of members is defined in such a way that a member declaration is always more precise than another declaration defined in a previous group in this list, which is expressed by the formula ∀ (i, j), S, Γ ⊢ (N i+j , M ) ≪ N i . Proof. It is easy to see that a variable only has a single type assignment in the context at any time, so all that remains to prove is that field declarations of the form val n a : T (= t) ? for a given a are unique in a given p.type. We do it by induction on the Expansion judgment and pathselect, using the semantics of ⊎, a method that we are going to detail in the following. Proof. The rules are syntax-directed (the form of the input determines the rule that must be used, and all the parameters of any recursive calls), except for ≺-class, ≺-type and ≃-step.

Decidability of the Algorithmic Type System

≺-class and ≺-type seem to create an ambiguity, but they are in fact algorithmically equivalent, since they only differ on the member that will be sought in the expansion of the type of the path that is in the conclusion.

The path in the premises of ≃-step is uniquely defined by the Path Typing judgment using Lemma 4.1. Proof. We start by inlining the membership rule ∋-singleton in the recursive calls of the three other judgments, leading to the following rules:

The other rules are left unchanged, and the system with those updated rules is trivially equivalent to the previous one. We prove the termination of the Expansion, Path Typing and Path Alias Expansion judgments by mutual induction, reasoning by case on the last rule of the derivation. The result is then easily extended to the Membership judgmement by inspection.

Cases ≃-refl and pathvar are easy. For the others, we consider that several rules in those judgments make all their recursive calls on a strictly larger set of locked symbols, and can therefore appear at most a finite number of times in any derivation. We can then concentrate on the remaining case, ≺-signature. Let us define the size of a type by the lexicographical pair (N, L) where N is the number of its members and L its textual size. Then this size is finite and positive, and ≺-signature only makes recursive calls on strictly smaller types. Those recursive calls conclude when reduced to a type signature with no inherited types, in which case the conclusion is true by vacuity.

Corollary 1. The Type Alias Expansion judgment terminates on all inputs.

Proof. Easy induction, considering that the rule ≃-type can only be applied a finite number of times. Proof. We proceed by mutual induction on those two judgments, and then by case on the last step of the derivation. Using Corollary 1, we can concentrate on the subtyping of unaliased terms (⊢ * ) using rule <:-unalias.

Case 1 (Algorithmic Subtyping). Cases <:-singleton-right and <:-paths are easy using Lemma 4.3. Moreover, it is easy to show using the Path Alias Expansion judgment, that the type T in the premises of <:-singleton-left is not a singleton type. This rule therefore allows us to unfold a subtyping problem referring to a singleton type to a subtyping problem between non-singleton types in a single step. Since our subtyping rules do not contain singleton types in their premises, the only singleton types we can encounter in a subtyping derivation are those explicitly mentioned in the program, and their number is finite. We can therefore consider that we work modulo this unfolding.

Using the definition of the size of a type given in the proof of Lemma 4.3, we can show that all the recursive calls to the Algorithmic Subtyping judgment are made on a strictly smaller type, noticing in the case of <:-class that a given trait can not extend itself.

The remaining case is <:-sig-right, where the call to the Member Subtyping judgment could potentially create a cycle. Let us proceed by contradiction: if there is such a cycle, it means that we have found a type signature T x | M such that one of its member declarations contains a declared type that is is either T x | M or some S y | N such that ∃ i, S i = T x | M . Then the textual length of this type is larger than the textual length of the type signature that contains it, which is absurd.

Case 2 (Member Subtyping). Easy with the previous case. Proof. We proceed by mutual induction on those judgments, then by case on the last rule of the derivation.

Case 3 (Member Well-Formedness). Considering wf-x-signature, we notice that, in a similar way to the problem we encountered with rule <:-sig-right in Case 1 of Lemma 4.4, we are in presence of a judgement that makes several potentially cyclic recursive calls to the Well-Formedness judgment. However, since the judgment is syntaxdirected, we notice that such a cycle would require us to find a type signature T x | M directly containing a member whose declared type lexically contains T x | M itself, which would give this type signature an infinite textual length.

The remaining interesting cases are wf-x-field and wf-x-method. in both cases, making a derivation involving those rules cyclic requires defining a type signature that directly contains a field or method whose value contains an instantiation of this very type signature:

M ∋ val n a :

T = val x = new T x | M ; t
This would again give an infinite textual length to the term T x | M .

Case 4 (Well-Formedness). We start by noticing that wf-singleton and wf-type can only occur a finite number of times, since they make their recursive calls on a strictly larger set of recursive types. We then conclude using the previous case and the termination lemma for the Membership judgment (Lemma 4.3).

Case 5 (Type Assignement). We conclude remarking that we make recursive calls to the Type Assignement judgment on structurally smaller terms, and using the previous termination lemmas.

Type Checking and Type Inference in Scala

The previous section showed that type-checking in FS alg is decidable. Does the same hold for full Scala? It is at present too hard to give a definite answer since full Scala is too complicated to admit a formalization of its type system which is complete yet still manageable enough to admit a proof of decidability. But one can conjecture. To do this, we need to compare full Scala with Featherweight Scala. Most of the additional syntactic constructs in full Scala do not cause particular problems for type-checking. However, unlike Featherweight Scala, full Scala has local type inference [START_REF] Pierce | Local type inference[END_REF][START_REF] Odersky | Colored local type inference[END_REF].

Local type inference needs to construct least upper bounds and greatest lower bounds (wrt the subtype ordering) of sets of types. The decidability of these lub and glb operations in FS alg is currently an open question. To see the problem, consider the following three class definitions. One can apply the same step to the result type of fromT to obtain a still greater lower bound. Repeating this step infinitely often one obtains the following limit of an ascending chain of lower bounds: so that there is hope that this implementation does in fact represent an algorithm for type checking Scala programs. Type-inference, on the other hand, needs to compute lub's and glb's of types and is believed to be undecidable. The Scala compiler avoids potential non-termination at the price of incompleteness by imposing an upper limit on the size of the types computed by a lub or glb. Note that we have classified here the typing of an if-then-else expression as a typeinference problem, not a type checking problem. The justification of this classification is that it is possible (and, at rare occasions, necessary) to provide a type for the expression with an explicit annotation.

Conclusion

We have presented a calculus for type-checking core Scala programs. Featherweight Scala describes the central constructs for programming components in Scala: nested classes, modular mixin composition, abstract types, type aliases, and path-dependent types. Unlike previous work on foundations of Scala [START_REF] Odersky | A nominal theory of objects with dependent types[END_REF], this calculus is decidable and admits a straight-forward type-checking algorithm.

Featherweight Scala programs are essentially a syntactic subset of regular Scala programs. The subset is kept minimal, so that one can concentrate on a small set of typing issues. In future work it would be interesting to extend the calculus to a larger fragment of Scala. Among the most interesting extensions are a call-by-value semantics, polymorphic methods, and mutable state.

The correctness of the calculus also remains to be verified. The operational semantics of FS alg is defined by a small-step reduction semantics. We intend to show in future work that it satisfies the subject-reduction and type-soundness properties. Judging from our experience with previous calculi [START_REF] Odersky | A nominal theory of objects with dependent types[END_REF][START_REF] Cremet | Foundations for Scala: Semantics and Proof of Virtual Types[END_REF] this looks plausible, but a formal proof still needs to be completed.

traitFig. 1 .

 1 Fig. 1. Definition of Peano numbers

Fig. 2 .

 2 Fig. 2. Definition of the List class hierarchy

traitFig. 3 .

 3 Fig. 3. Definition of first-class functions

Figure 3 Fig. 4 .

 34 Fig. 4. Encoding of the higher-order map function

  valna : T (= t) ? Field decl defna `y : S ´: T (= t) ? Method decl type n A (= T ) ? Type decl traitnA extends `T ´˘ϕ | M ¯Class decl s, t, u ::= Term x Variable t.a Field selection s.a `t´M ethod call val x = new T ; t Object creation Singleton type `T ´˘ϕ | M ¯Type signature Reduction valna : T = t ∈ Σ(x) Σ ; x.a → Σ ; t (red-value) defna `z : S ´: T = t ∈ Σ(x) Σ ; x.a(y) → Σ ; [y/z]t (red-method)

5 .Fig. 6 .Fig. 7 .

 567 Fig. 6. The FS alg Calculus : Type Assignment, Expansion & Membership

Lemma 4 . 1

 41 If a term t can be assigned a type T by the Path Typing judgment, then it is unique.

Lemma 4 . 2

 42 The calculus defines a deterministic algorithm.

Lemma 4 . 3

 43 The Path Typing, Expansion, Membership, and Path Alias Expansion judgments terminate on all inputs.

Lemma 4 . 4

 44 The Algorithmic Subtyping and Member Subtyping judgments terminate on all inputs.

Lemma 4 . 5

 45 The Type Assignement, Well-Formedness and Member Well-Formedness judgments terminate on all inputs.

  trait A { this0 | type T def fromT(x : T): A } trait B { this0 | type T def fromT(x : T): B } trait C extends A with B { this0 | def fromT(x : T): C } Now assume that we want to find the greatest lower bound of A and B. Clearly, C is a lower bound of A and B, but it is not the greatest one. A greater lower bound is represented by the following refinement type: with B { this0 | fromT(x : T): C }

  Scala does not have a clause { thisN | ... } which names the self-reference thisN of the enclosing class. Instead, one always uses the reserved word this. Self-references of an outer class C can be denoted by prefixing this with the name of the outer class, e.g., C.this.

	trait List extends Any { this0 |
	type Elem
	type ListOfElem = List { this1 | type Elem = this0.Elem }
	def isEmpty(): Boolean
	def head(): this0.Elem
	def tail(): this0.ListOfElem
	}
	trait Nil extends List { this0 |
	def isEmpty(): Boolean = true
	def head(): this0.Elem = error("Nil.head")
	def tail(): this0.ListOfElem = error("Nil.tail")
	}
	trait Cons extends List { this0 |
	val hd : this0.Elem
	val tl : this0.ListOfElem
	def isEmpty(): Boolean = false
	def head(): this0.Elem = hd
	def tail(): this0.ListOfElem = tl
	}
	as
	follows:
	val universe = new { global |
	class Nat { ... }
	}
	val zero = new universe.Nat { ... };
	val two = zero.succ().succ();
	two.add(two)
	In this program, references from one top-level definition in universe to another would go
	via the top-level self-reference global.
	The syntax used in the examples in this section is also regular Scala, with one ex-
	ception: Lists. As a second example, Figure 2 presents a class hierarchy for lists in Featherweight
	Scala. There are three classes: A base class List and two subclasses Cons and Nil that
	define non-empty and empty lists, respectively.
	Lists can have arbitrary element types. In the standard Scala library, this is expressed
	by a parameterized type, but the featherweight version does not have type parameters.
	Instead, we use abstract types to express the genericity of the list abstraction.

(path-var) S, Γ ⊢ p.type ∋ valna : T (= t) ? S, Γ ⊢ path p.a : T (path-select)Type Assignment S, Γ ⊢ path p : T S, Γ ⊢ p : p.type (path) S, Γ ⊢ t : S t is not a path S, Γ ⊢ S ∋ valna : T (= u) ? S, Γ ⊢ t.a : T (select) S, Γ ⊢ s : S S, Γ ⊢ t : T ′ S, Γ ⊢ T ′ <: T S, Γ ⊢ S ∋ defna `x : T ´: U (= u) ? S, Γ ⊢ s.a `t´: U (method) S, Γ, x : T ⊢ t : S x ∈ fn(S) S, Γ ⊢ T ≺ϕ Mc S, Γ ⊢ T wf S, Γ ⊢ val x = new T ; t : S (new) Expansion S, Γ ⊢ p.type ∋ traitnA extends `T ´˘ϕ | M {n} ∪ S, Γ ⊢ `T ´˘ϕ | M ¯≺ϕ N n ∈ S S, Γ ⊢ p.A ≺ϕ N (≺-class) S, Γ ⊢ p.type ∋ type n A = T {n} ∪ S, Γ ⊢ T ≺ϕ M n ∈ S S, Γ ⊢ p.A ≺ϕ M (≺-type) ∀ i, S, Γ ⊢ Ti ≺ϕ Ni S, Γ ⊢ `T ´˘ϕ | M ¯≺ϕ `Ui Ni ´⊎ M (≺-signature) Membership S, Γ ⊢ p ≃ q S, Γ ⊢ path q : T ψ(p) ∪ S, Γ ⊢ T ≺ϕ M ψ(p) ⊆ S S, Γ ⊢ p.type ∋ [p/ϕ]Mi (∋-singleton)T is not a singleton type S, Γ ⊢ T ≺ϕ M ϕ / ∈ fn(Mi) S, Γ ⊢ T ∋ Mi (∋-other)

S, Γ ⊢ p.type ∋ type n A (= T ) ? " {n} ∪ S, Γ ⊢ T wf n ∈ S " ?S, Γ ⊢ p.A wf (wf-type)MemberWell-Formedness (S, Γ ⊢ T wf) ? S, Γ ⊢ type n A (= T ) ? wfx (wf-x-type) S, Γ ⊢ T wf (S, Γ ⊢ t : T ′ S, Γ ⊢ T ′ <: T ) ? S, Γ ⊢ valna : T (= t) ? wfx (wf-x-field) S, Γ, ϕ : x.A ⊢ `T ´˘ϕ | M ¯wfϕ S, Γ ⊢ traitnA extends `T ´˘ϕ | M ¯wfx (wf-x-class)S, Γ ⊢ S, T wf S does not contain singleton types `S, Γ, x : S ⊢ t : T ′ S, Γ ⊢ T ′ <: T´?S, Γ ⊢ defna `x : S ´:T (= t) ? wfx (wf-x-method) ∀i, S, Γ ⊢ Ti ≺ϕ Ni S, Γ ⊢ M wfϕ S, Γ ⊢ T wf ∀ (i, j), S, Γ ⊢ (Ni+j, M ) ≪ Ni S, Γ ⊢ `T ´˘ϕ | M ¯wfϕ (wf-x-signature) Path Alias Expansion S, Γ ⊢ path p : q.type ψ(p) ∪ S, Γ ⊢ q ≃ q ′ ψ(p) ⊆ S S, Γ ⊢ p ≃ q ′ (≃-Step)S, Γ ⊢ path p : T T is not a singleton type S, Γ ⊢ p ≃ p (≃-Refl)

Type Alias ExpansionS, Γ ⊢ p.type ∋ type n A = T {n} ∪ S, Γ ⊢ T ≃ U n ∈ S S, Γ ⊢ p.A ≃ U (≃-type) S, Γ ⊢ p.type ∋ type n A S, Γ ⊢ p.A ≃ p.A (≃-abstype) S, Γ ⊢ p.type ∋ traitnA extends `T ´˘ϕ | M S, Γ ⊢ p.A ≃ p.A (≃-class) S, Γ ⊢ `T ´˘ϕ | M ¯≃ `T ´˘ϕ | M (≃-signature) S, Γ ⊢ p.type ≃ p.type (≃-singleton) Algorithmic Subtyping S, Γ ⊢ T ≃ T ′ S, Γ ⊢ U ≃ U ′ S, Γ ⊢ * T ′ <: U ′ S, Γ ⊢ T <: U (<:-unalias) S, Γ ⊢ p ≃ p ′ S, Γ ⊢ q ≃ p ′ S, Γ ⊢ * p.type <: q.type (<:-singleton-right)U is not a singleton type S, Γ ⊢ p ≃ q S, Γ ⊢ path q : T S, Γ ⊢ T <: U S, Γ ⊢ * p.type <: U (<:-singleton-left)S, Γ ⊢ p ≃ p ′ S, Γ ⊢ q ≃ p ′S, Γ ⊢ * p.A <: q.A (<:-paths)A = A ′ {n} ∪ S, Γ ⊢ Ti <: p ′ .A ′ n / ∈ S S, Γ ⊢ p.type ∋ traitnA extends `T ´˘ϕ | M S, Γ ⊢ * p.A <: p ′ .A ′ (<:-class) S, Γ ⊢ Ti <: p.A S, Γ ⊢ * `T ´˘ϕ | M ¯<: p.A (<:-sig-left)T is not a singleton type ∀i, S, Γ ⊢ T <: Ti S, Γ ⊢ T ≺ϕ N dom(M ) ⊆ dom(N ) S, Γ ⊢ N ≪ M S, Γ ⊢ * T <: `T ´˘ϕ | M (<:-sig-right) Member Subtyping S, Γ ⊢ T <: T ′ S, Γ ⊢ valna : T (= t) ? <: valma : T ′ (= t ′ ) ? (<:-member-field) S, Γ ⊢ type n A = T <: type n A (= T ) ? (<:-member-type) S, Γ ⊢ traitnA extends `T ´˘ϕ | M ¯<: traitnA extends `T ´˘ϕ | M ¯(<:-member-class) S, Γ ⊢ S ′ <: S S, Γ ⊢ T <: T ′ S, Γ ⊢ defna `x : S ´: T (= t) ? <: defma `x : S ′ ´: T ′ (= t ′ ) ? (<:-member-method) Fig. 8. The FS alg Calculus : Subtyping

S, Γ ⊢ p ≃ q S, Γ ⊢ path q : T ψ(p) ∪ S, Γ ⊢ T ≺ϕ M , [ϕ/p](valna : T ′ (= t) ? ), M ′ ψ(p) ⊆ S S, Γ ⊢ path p.a : T ′ (path-select) S, Γ ⊢ p ≃ q S, Γ ⊢ path q : T ψ(p) ∪ S, Γ ⊢ T ≺ϕ M , [ϕ/p](traitnA extends `S´˘x | N ¯, M ′ ) ψ(p) ⊆ S {n} ∪ S, Γ ⊢ `S´˘x | N ¯≺x N ′ n / ∈ S S, Γ ⊢ p.A ≺x N ′ (≺-class) S, Γ ⊢ p ≃ q S, Γ ⊢ path q : T ψ(p) ∪ S, Γ ⊢ T ≺ϕ M , [ϕ/p](type n A = S), M ′ ψ(p) ⊆ S {n} ∪ S, Γ ⊢ S ≺x N ′ n / ∈ S S, Γ ⊢ p.A ≺x N ′ (≺-type)

Acknowledgement. We thank Rachele Fuzzati for proofreading the formal description of the calculus.

This limit does not exist as a finite type in FS alg , but the natural algorithm for computing lower bounds is likely to try to construct it, and this would result in non-termination. A similar infinite approximation can be constructed for the lub operation by using the contravariance of method parameters. An example is the lub of the two refinements

The problem of infinite approximations of lub's and glb's also occurs when type-checking Java 1.5 programs with generics and wildcards [START_REF] Torgersen | Adding wildcards to the Java programming language[END_REF]. The decidability of the latter is currently open [START_REF] Zdancewic | Type inference for Java 5: Wildcards, F-bounds, and undecidability[END_REF].

The Scala compiler addresses this problem by imposing a maximum size on the types computed by its lub and glb operations. It is currently set at 10 levels of parameterizations or refinements. If a type computed by lub or glb exceeds this limit the system will reply with an error such as the one below: Scala compiler thus turns the potential problem of undecidability of type inference into a completeness problem: local type inference might now fail to give a solution even if a best type would exist. However, in practice such complicated types arise very rarely. Moreover, it is always possible to guide the type inference process by adding more type annotations, so that infinite approximations are avoided.

In the failed example above, the problem would have been avoided by giving an explicit annotation of the desired type of the problematic conditional. For instance, the following compiles without error.

To summarize, the results on type-checking Featherweight Scala give some degree of confidence that type-checking regular Scala is also decidable. Furthermore, the formalization of locks in FS alg corresponds closely to the present implementation in the Scala compiler,