## 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:
- The subtyping between two classes is allowed in the usual OO style.
- 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.
- The subtype relation for complex types is non-variant
at the domain position of a function type
and co-variant at all other positions.
- No subtype relation may exist between two types
with different heading algebraic datatype constructors.
- 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.

A long version of the paper is here.

The slides for a talk at ECOOP96 are here.

Zhenyu Qian