Why is type inference impractical for object oriented languages?

Question

I'm currently researching ideas for a new programming language where ideally I would like the language to mix some functional and procedural (object oriented) concepts.

One of the things that I'm really fascinated about with languages like Haskell is that it's statically typed, but you do not have to annotate types (magic thanks to Hindley-Milner!).

I would really like this for my language, however after reading up on the subject it seems that most agree that type inference is impractical/impossible with subtyping/object orientation, however I have not understood why this is. I do not know F#, but I understand that it uses Hindley-Milner AND is object-oriented.

I would really like an explanation for this and preferably examples on scenarios where type inference is impossible for object oriented languages.

Corfu

Reading tip: Benjamin Pierce, "Types and Programming Languages" – Saluki

You might be interested in reading this paper: research.microsoft.com/en-us/um/people/moskal/pdf/msc.pdf – Alexine

Answer 1

When using nominal typing (that is a typing system where two classes whose members have the same name and the same types are not interchangeable), there would be many possible types for a method like the following:

let f(obj) =
    obj.x + obj.y

Any class that has both a member x and a member y (of types that support the + operator) would qualify as a possible type for obj and the type inference algorithm would have no way of knowing which one is the one you want.

In F# the above code would need a type annotation. So F# has object orientation and type inference, but not at the same time (with the exception of local type inference (let myVar = expressionWhoseTypeIKNow), which always works).

Pall

I don't really get why this is a problem. Wouldn't the type checker know the type of obj before the call to f? – Corfu

@Corfu I'm talking about type-checking the definition of f, not the call-site. There may not even be a call to f or the call to f might be in a different compilation unit. – Pall

Ok, but what if I build a type checker that infer the types of objects/functions/arguments/whatever when they are used? In that case, there could be many versions of f depending on how it's called. Is that even a possible/sane thing to do? – Corfu

@Corfu It means that anyone who wants to use your functions needs access to your source code, that the source code needs to be recompiled everytime it's used and that it's impossible to type-check libraries by themselves (i.e. you'd only be able to typecheck it in the context of code that use the library). Those are a lot of drawbacks, but it is how C++ templates work, so it's not unprecedented. – Pall

@Pall the C++ community realizes full well that this model has lots of drawbacks, hence various attempts to introduce typing for templates ("concepts"). – Kino

@Pall By the way the problem is not unique to OO languages at all, see Haskell with its requirement for unique selector names. An OO language could ostensibly have a similar requirement. – Kino

Very interesting points! Maybe I can introduce optional type constraints to lesser the impact of these drawbacks? Anyways, I'm happy with the discussion so I'm accepting this as the answer :) – Corfu

@monoceres: it would actually be quite interesting to see a functional language with C++ -like templating built into it. ::mumble:: – Whydah

Answer 2

To add to seppk's response: with structural object types the problem he describes actually goes away (f could be given a polymorphic type like ∀A ≤ {x : Int, y : Int}. A → Int, or even just {x : Int, y : Int} → Int). However, type inference is still problematic.

The fundamental reason is this: in a language without subtyping, the typing rules impose equality constraints on types. These are very nice to deal with during type checking, because they can usually be simplified immediately using unification on the types. With subtyping, however, these constraints are generalised to inequality constraints. You cannot use unification any more, which has at least three unpleasant consequences:

1. The number and complexity of constraints explodes combinatorially.
2. The information you have to display to the user in case of errors is incomprehensible.
3. Certain forms of quantification can quickly become undecidable.

Thus, type inference for subtyping is not impossible (there have been many papers on the subject in the 90s), but it is not very practical.

A much simpler alternative is employed by OCaml, which uses so-called row polymorphism in place of subtyping. That is actually tractable.

Hussar

Interesting. Unfortunately I lack the theoretical understanding of typing to fully understand your points. Any thoughts on the discussion in the other answer about using C++ like templating concepts (which seems to be best described as "compile time duck typing")? – Corfu

From a type-checking perspective, templates essentially are just macros. So not very interesting and not very modular. :) – Hussar