Static-typing for languages with covariant parameters

Published by marco on

Updated by marco on

Example

class DRIVER
  feature
    name: STRING
    license_valid: BOOLEAN
end

class TRUCK_DRIVER
  inherit
    DRIVER
  feature
    maximum_weight_vehicle: INTEGER
end

class VEHICLE
  feature
    drive (d: DRIVER) is
      require
        d.license_valid
      deferred
      end
end

class TRUCK
  inherits
    VEHICLE
      redefine
        drive
      end
  feature
    weight: INTEGER

    drive (d: TRUCK_DRIVER) is
      require else
        d.maximum_weight_vehicle
          >= weight
      deferred
      end
end

v: VEHICLE
t: TRUCK
d: DRIVER

t := create TRUCK
d:= create DRIVER

v := t
  — legal by polymorphism
v.drive (d)
  — legal by language rules and 
  — static checking, but will 
  — generate a run-time error since 
  — the actual method called will 
  — expect a TRUCK_DRIVER instead
  — of a driver and will access a
  — property unique to that class.

The draft Type-safe covariance by a collection of Eiffel’s leading lights, including Bertrand Meyer, Emmanuel Stapf and Axa Rosenberg, addresses an issue that crops up only in advanced OO languages.

By that I mean only one known language, Eiffel.

The issue is that in a language that allows covariant parameter definition and polymorphism, it becomes possible to execute a statically valid, but dynamically invalid, routine call. See the example to the left for a simple, but perfectly valid case.

In the process of discussing a solution to this problem, the paper covers a lot of other features unique to Eiffel and provides several glaringly bad examples where other languages would benefit from having them.

For example, there is a short discussion of the utility of anchored types, wherein a parameter or feature type is ‘anchored’ to the type of another variable. It is almost necesssary in a language that allows covariant parameter redefinition since often several methods have to be updated with the new type, as is the case with TRUCK_DRIVER in the example.

“For such a ‘setter’ procedure the body of the redefinition would, as shown, simply reproduce the original, unlike routine redefinitions that also change the implementation. Such signature-only redefinitions are common and would cause ‘redefinition avalanche’ with large amounts of duplicated code. This is not acceptable in practice and is avoided by Eiffel’s anchored type mechanism.”

Similarly, an irrefutable case is made for genericity using Java core classes as an example, where the paper derides Java’s approach with “…[a] possible name for the programming language mechanism illustrated here is ‘Genericity Through Comments’.)”. The code examples clearly show programmers struggling with concepts wholly missing from their languages; the language is not capable of expressing the intent and results in hard-to-understand, heavily-casted, ugly code.

“These examples, from a fundamental Java library, seem to suggest that the mechanisms discussed in this article — covariance, descendant hiding, genericity — do address fundamental expressive needs of programming; excluding them leads to a contorted style involving casts and exceptions, and to risks of run-time failure.”

Further along, another feature unique to Eiffel, contracts, is discussed, but not in detail. Instead, it is simply noted that a program has three levels of correctness: a program may be “syntactically legal”, it may be “valid” if it “satisfies all [the] type rules” and, finally, it may be “correct” if it satisfies the defined contracts in the program. It is the issue of validity that is addressed in this paper, adding another layer of static checking. In effect, this static check will flag all cases where a bad call may be made and forces the class writer to define a ‘recast’ function to address these cases.

After an opening salvo on the pathetic state of the more popular object-oriented languages, the authors settle down to solving the static-checking problem that crops up once more freedom is allowed in a language. The discussion turns to various solutions and the relative amounts of expressiveness afforded by each. The general topic of expressiveness brings another opportunity to hammer home the somewhat belabored (in this article, not in general) point of the astounding lack of expressiveness in modern languages like Java, C++, Delphi, etc.

“How much expressiveness is sufficient remains partly a subjective judgment; for example, Java programmers appear to survive without genericity, covariance or multiple inheritance, and some of them may not realize what they are missing if they have not had access to these mechanisms in other languages. On the other hand, examination of typical Java code shows (see Viega et al. [14]) that they resort to various unnatural tricks to emulate them.”

I find it quite refreshing to read an article that poses language features that help me write better and more failsafe programs, rather than making compilability the major goal and writing off eminently useful features as “too hard to compile or type-check”.