Typed Object-Oriented Programming with Late Binding

Object-oriented programming languages are suitable for describing real-world objects, while functional programming languages for algebraic values. In this paper we propose an object-oriented functional programming language, called TOFL, which combines many desired properties of the two paradigms. In particular, TOFL unifies object classes, inheritance, (method) redefinitions and late binding as in object-oriented languages, algebraic data types, higher-order functions, type classes and type inference (without type reconstruction in this paper) as in functional languages.

More concretely, TOFL combines the Haskell-like and object-oriented type system.

  • It allows the usual OO classes and FP algebraic data types. Types are constructed by algebraic datatype constructors and OO classes (regarded as 0-ary type constructors).
  • The sybtyping relation satisfies the following restrictions:
    (a) The subtyping between two classes is allowed in the usual OO style.
    (b) A type with an algebraic datatype constructors may be a subtype of a class, but in this case the class cannot contain attributes. The style of the declaration resembles that of Haskell.
    (c) The subtype relation for complex types is non-variant at the domain position of a function type and co-variant at all other positions.
    (d) No subtype relation may exist between two types with different heading algebraic datatype constructors.
    (e) No classes may be a subtype of a type with a heading algebraic datatype constructor.
  • The type system allows a concept of self-type.

    TOFL extends the usual mechanism of sending a message to a receiver-object to that to a receiver-expression. The self type can occur anywhere and arbitrary times within a type corresponding to the receiver-expression. But outside the type, the self type can only occur at co-variant positions. Under this restriction, TOFL can support binary operations naturally without sacrificing the static type safty.

    TOFL supports dynamic binding mechanism. The underlying calculus, ie. a stratified and explicitly typed $\lmd$-calculus $\HM$ with overloaded functions, where redefinitions and late binding become late binding of overloaded functions, has been proved to be confluent.

    The paper is here.
    FTP: ftp.uni-bremen.de:/pub/Uni-Bremen/Departments/CS/Chairs/Krieg-Brueckner/qian/ecoop96.ps.gz

    A long version of the paper is here.
    FTP: ftp.uni-bremen.de:/pub/Uni-Bremen/Departments/CS/Chairs/Krieg-Brueckner/qian/lecoop96.ps.gz

    The slides for a talk at ECOOP96 are here.

    For a hard copy send a message to Zhenyu Qian.