3
$\begingroup$

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 :) .

$\endgroup$
  • $\begingroup$ Am I allowed to say "don't use object-oriented programming"? $\endgroup$ – Andrej Bauer Nov 29 '13 at 20:55
5
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ Are you sure that Scala has exactly the feature the question asks for and Kim Bruce's paper describes? The paper uses MyType as a bound type variable, and final_class is essentially that, even though the binder is implicit. I'm not sure, but I don't think Scala can do this. $\endgroup$ – Martin Berger Nov 29 '13 at 16:39
  • 1
    $\begingroup$ I'm pretty sure, but since I don't program in Scala, I'm not completely sure. In Overview of the Scala Programming Language, Odersky shows how Scala supports family polymorphism, which I think generalizes self types. $\endgroup$ – Neel Krishnaswami Nov 29 '13 at 21:10
  • $\begingroup$ Yes, you are right. The self.type expression corresponds to MyType in Bruce's TOOPL. Funnily enough, I do give that paper to our masters students every year, but this particular section had never registered. Thanks. $\endgroup$ – Martin Berger Nov 29 '13 at 21:36
  • $\begingroup$ @NeelKrishnaswami, you may or may not have noticed that OCaml also has this feature. class type abelian = object ('s) method inverse : 's method add : 's -> 's end $\endgroup$ – gasche Nov 30 '13 at 20:14
4
$\begingroup$

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.

$\endgroup$
2
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ That's something similar to Java Generics or C++ Templates, no? The problem I see is that this solution doesn't enforce that T extends or implements A. In any case, I suppose it's possible :) . Thanks. $\endgroup$ – castarco Nov 29 '13 at 12:00
  • $\begingroup$ Ok, i was wrong in one point. Event taking into account that i can enforce many restrictions on T... this solution has one problem yet: we cannot enforce the type T to be equal to AImpl in the trait definition... the contract can be broken. $\endgroup$ – castarco Nov 29 '13 at 12:06
  • $\begingroup$ You can change the trait definition to trait A [ T <: AImpl ] { ... }. That forces the type parameter to be (a subclass of) AImpl. $\endgroup$ – Martin Berger Nov 29 '13 at 12:48
  • $\begingroup$ But this solution makes the trait no reusable in other classes that are not subclasses of AImpl. The point i'm claiming is that there is no elegant solution in any popular OO language, and this lack of an elegant solution has no obvious reasons: in terms of performance is better to do the check in compile time than in run time. $\endgroup$ – castarco Nov 29 '13 at 13:02
  • $\begingroup$ One other reason could be that it makes type-inference harder. $\endgroup$ – Martin Berger Nov 29 '13 at 16:43

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.