Is there a language with strong typed interfaces where types resolution are "delayed"?

Question

I know that this question it not entirely theoretical, but I think that's the place where is more probable that someone knows the answer.

The question is: is there any OO strong typed language where I could "delay" the definition of the method's arguments types?

I'll write an example. Imagine I want to model abelian additive groups, and I program the following interface:

interface AbelianAdditiveGroup
{
    public method add(b final_class) : final_class;
    public method additiveInverse() : final_class;
}

Where final_class is a keyword to tell the compiler to use the implementation class, not the AbelianAdditiveGroup or any other intermediate abstract class.

That's an example of what I'm searching. I think that using fixed interfaces or classes as argument types in these methods is a bad approach in a lot of cases because this causes that we have to do multiple runtime type checks in our code.

If there is no language with this feature... is there any good reason for this?

Thanks in advance :) .

Answer 1

What you are looking for are called "self types", and have been studied theoretically for ~20 years or so.

For example, see Safe Type Checking in a Statically-Typed Object-Oriented Programming Language by Kim B. Bruce, in the 1993 POPL (Principles of Programming Languages), pp. 285-298. Off the top of my head, John Mitchell and Kathleen Fisher have also worked on this, and they may also be described in Abadi and Cardelli's book A Theory of Objects.

Scala supports them, but I don't know if other mainstream OO languages do.

Answer 2

Perhaps you are looking for modules. For example, the following code uses OCaml's module system to define a signature for monoids and two implementations:

module type Monoid = sig
  type t
  val identity : t
  val oper : t -> t -> t
end

module IntSum : Monoid = struct
  type t = int
  let identity = 0
  let oper x y = x + y
end

module IntProd : Monoid = struct
   type t = int
   let identity = 1
   let oper x y = x * y
end

Does this qualify as OO? Hmm... What does OO mean again?

To give this more of a cstheory vibe: modules are related to existential types (but not the same thing, see below). In turn, existential types are essentially (second-order) existential quantification under the propositions-as-types correspondence. See Mitchell and Plotkin's Abstract types have existential type (paywall) as well as Cardelli and Wegner's On Understanding Types, Data Abstraction, and Polymorphism. See also this HaskellWiki entry on existential types.

There are some subtleties to this point, however. See e.g. MacQueen's Using Dependent Types to Express Modular Structure.

Answer 3

In Scala you can use parametric polymorphism for this, e.g. like so:

trait A [ T ] {
   def f ( t : T ) : T
   def g ( t : T ) : T = t }

class AImpl () extends A [ AImpl ] {
   def f ( t : AImpl ) : AImpl = t }

(Traits are a generalisation of Java interfaces). This can be resolved at compile-time, although I don't know how the Scala compiler and the JVM implement this. Other languages with expressive polymorphism should enable similar constructs.

Edit following Neel's remarks: here is a Scala implementation that, I think, does exactly what you want, but without a hack like type-parameterisation.

trait A { self =>
  def f ( t : self.type ) : self.type
  def g ( t : self.type ) : self.type = t }

class AImpl () extends A {
  def f ( t : this.type ) : this.type = t }

Scala's self=> ... construct gives you access to the this pointer in classes 'up the inheritance/implementation hierarchy', and .type give you the corresponding type.