Global type inference for an OO trait-based language [early idea]

In trying to bring my YinYang work to a textual programming language, I'm beginning to design a new type system based on mixin-like traits (as in YinYang, no classes) but with global type inference (also, to support the inference described in the before-mentioned paper). As we know, global type inference through Hindley Milner in OO languages is problematic given support for subtyping. So a language like Scala is limited to local type inference.

I'm developing my system based adding the concept of an "at most" constraint as the opposite of the typical "at least" constraint. Rather than have type variables that are bound, their "at most" constraint starts as an open type that is gradually narrowed via unification. Consider some Scala/C# like code:

trait Dictionary[K,E] { 
  def set(key : K, elem : E) = {...}
  def get(key : K) : E = {...}
}
def foo(s : string) = {...}

def bar(dict) = {
  dict.set(key = 42, elem = "hello");
  foo(s = dict.get(0));
}

The bar method lists dict as an argument without specifying a type, so a type parameter is implicitly created for it (we could have written def bar[T](dict : T)). The second-last statement (calling "set") propagates a constraint on dict that (a) dict is at least a Dictionary (as in YinYang, methods are selected directly rather than by name), K is at most int while E is at most string. The last statement (calling "foo") propagates a constraint on dict that E is at least string (so E is string since its at least and at most a string). So for any def "p" with argument "a" that is called on expression "e" (so "p(a = e)") we have:

typeof(e) <: typeof(a)
typeof(a) :> typeof(e) 

Where <: is "at least," which are combined by union, and :> is "at most," which are combined by intersection. A type error occurs on a type parameter if "at least" is not a subset of "at most." An actual type is just a set of traits where extension means subset (so if C : B and B : A, then typeof(C) is (A, B, C)). Type variables are never closed until they go out of scope (in which case, we can just take "at least" to be its type), and so we have to limit the type system in some way so we can type check in a modular way, which I haven't really explored yet.

YinYang-style inference comes into play when we start treating traits like type variables that can be constrained. Also, exclusive extension relationships (which prevents an int from being mixed in with a Button, for example) continue to temper the flexibility of compositions so the system isn't completely open-ended.

So I'm trying to figure out why I think this is workable to support global type inference when Scala cannot support it with similar mechanisms. Any ideas? Perhaps its because I'm not relying on name binding (names are resolved to symbols by the IDE)?

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

What do you mean by "(no

What do you mean by "(no classes)"?

It seems this is made a little easier for yourself by defining foo(s: string) rather than just foo(s). Do you propose a truly global inferencing algorithm, in the sense that you are going to review all of f()'s callers to see what f()'s argument types are? How will you handle recursion? Library boundaries?

BTW, I think this is incredibly interesting. I'm working on a language that would use this (over my current local-only type inference) in a heartbeat if you/we figure out if any remaining limitations are acceptable.

Scala-style traits are

Scala-style traits are simply classes that support mixin-style inheritance sans constructors. In the language I'm designing, there are only traits that have constructors and a few other features (exclusive inheritance) that allow them to supersede the need for classes in a language.

Inference will be restricted to the module level, so you can't change the type of a library method simply by implementing it. However, any constraints computed in compiling a module remain visible to clients of that module (for visible symbols of course!). Recursion is easy enough to detect in a set-based way (hey, the set I got for this type includes myself...to top or bottom!). I hacked this scheme up in Scala (because I was bothered with lazy type completion) at one point a long time ago, and it seemed to work.

I'm just wondering if I'm reinventing the wheel (or worse yet, an unworkable square wheel, even dependent types...scary), it seems like an obvious solution.

clarification

Trying to clarify.

When Scala unifies types, its trying to compute an equivalence, "T = A" whereas I think only a range is necessary in my case, "A <= T <= B," which I think should be much easier to compute. The lack of name binding means we don't depend on type information to resolve names to symbols, so equivalence isn't really necessary (on the flip side, we can definitely use what type information we have to guide name resolution in the IDE). And since I have no qualms about upgrading types as needed (refining the at-least type on demand), I think I'm dealing with a different set of language design constraints.

So performance would be limited by the size of sets being unioned and intersected, which in term depends on (a) the number of letters (e.g., type parameters, traits) in our type systems, and (b) the "depth" of the type (since type parameters are members and can have members...). As for (a), this can get tricky since type parameters are duplicated on instantiation (make an object, call a method), and we can't just blow them away very easily. As for (b), in a functional language you can have very deep typeful structures, but in an imperative language less so. Limiting accuracy of deeper structures could some how help.

Combinatorics and decidability

What you describe seems no different from the usual approach to subtyping inference (see e.g. the works of Palsberg and others). The reason that, in practice, it doesn't work well as a global mechanism is that (1) constraints quickly explode combinatorially, and (2) there is no succinct way to present inferred "types" to the user.

In Scala, you also have very expressive forms of (first-class) polymorphism, which make everything undecidable immediately, even without subtyping.

Ah, I've been looking at

Ah, I've been looking at some of Jens' papers but didn't see an immediate similarity. I should probably look for some sort of trade off, as in arguments have to be typed so that all type variables are explicit and the constraints converge more quickly while still conveying benefits to library users (the dictionary example would still work, but the dict argument would need some sort of type).

The problem with Scala, as I understand it, is that they are tracking exact type parameter bindings and therefore unification is very hard. I think that by tracking upper and lower bounds separately, there is a lot more leeway (unification is just intersection most-bounds and union for least-bounds, no magic number limits needed to compute LUBs and MLBs!), or maybe I'm deluding myself.

At most

dict.set(key = 42, elem = "hello");

K is at most int while E is at most string

It does not seem clear to me why these should be an upper bound.

We know that dict.K is at

We know that dict.K is at most int and dict.E is at most string (actually referred to as a lower type bound???). When I grab some key or element from dict later, that upper bound is very useful in further type checking as well as code completion (i.e. we can show completions between the at-least and at-most type bounds).

Why do we know that?

What I intuitively understand from `key = 42, elem = "hello"` is that a key can be constructed from an integer, and an elem can be constructed from text. This is compatible, for example, with `key` type being a rational or float, of which 42 is one example. It does not make sense to me that you treat these as upper bounds. Rather, "can be constructed from" is a lower bound - a trait or typeclass.

What am I missing? Are there no overloaded operators, literals, or expressions in your language?

We're talking about

We're talking about constraints on type signatures, not constraints on values.

To say E is "at most" string does not mean that a variable of type E cannot hold subclasses of string. It means that the type declaration for E must be at most string. It cannot be more than string otherwise a string could not be assigned.

e.g. in C++:

class base
class string : public base
class myString : public string

template<class E> struct foo { E * member; } var;

var.member = new string("hello") implies that var.E is at most string, because if var.E were myString the assignment would be invalid. However, E could be less than string (it could be base).

Right!Actually, my example

Right!

Actually, my example is bad because I'm using types that aren't typically refined, a better example would be:

dict[1] = aDog;
dict[2.3] = aCat;

K is at most a number (the intersection of int and float) while E is at most a mammal (the intersection of dog and cat). These types are useful for guiding code completion, where we don't see the program as a close entity. At-least type constraints are driven by need; e.g.,

foreach (var e in dict.Elements) e.doAnimalStuff();

In this code, e has doAnimalStuff in its code completion menu, and after the code is written, E would be at least an animal, which is completely compatible with it at least being a mammal.

It get's a bit more interesting if we do:

object a : Thing;
dict[1] = a;
foreach (var e in dict.Elements) e.doAnimalStuff();

So typically there would be an error on "a" if its type was closed, but with the "maze of twisty classes" work, "a" is automatically upgraded to an animal because it needs to be. We could do this implicitly or through a fix mechanisms, but the point is that it is driven by inference.

Ah, so when the programmer

Ah, so when the programmer specifies a type, he's in fact specifying a minimum type, but the rest of the program text can constrain that further. Yes, that makes sense, since in a statically untyped language every variable tacitly has a specified type of <root type> and type inference in those languages per se is attempting to tighten that up.

Applying this to a whole program sound scary, but within the context of a well-defined module with an interface that is firmly typed (i.e. those are the actual types, not minimum types), and which only calls out to other well-defined modules, it seems like this should let you abandon specifying type information everywhere within the module (since any time an object "arrives", it's either been created explicitly and has a known type, or it's been passed in and has a known type). So you could create a library with a well-defined C++ interface, but internally it's all just typeless variable declarations.

Then, as meta-level 1, the users of a module in a specific program could expose their inference information for that interface, and that inference information could be combined to tighten up the interface according to actual usage. So, say a library is flexible with regards to some input objects (they have virtual functions defined) but in fact only one type of object is used. The interface can now be tightened up - just for this program - to make those functions non-virtual. And now they can be inlined, even, during link-time code generation. Huge performance win, but still based on nice flexible library code. And the flexible library code has a static signature so can also be linked with code which doesn't do the type inference.

I like the idea, definitely, although I doubt I have anything to contribute regarding its feasibility in the general case :)

erroneous constraints on type signatures?

the type declaration for E must be at most string. It cannot be more than string otherwise a string could not be assigned

But:

  • a string could be assigned if E was a superclass of string
  • a string could be assigned if E was any class with a unique constructor from strings

The latter point may be language-dependent - e.g. Haskell can do it for numbers (via typeclass), while C++ can do it for strings.

In your example, if E was of type `base`, it could be assigned `new string("hello")`. And it could also be assigned any subclass of string.

Yes, any value with a type

Yes, any value with a type that is a superclass of E can be assigned to E (and doing so changes the at-most type of E), in fact, anything can still be assigned to E because its at-least type is empty.

I'm not considering conversions.

Right, so your bullet points

Right, so your bullet points explain what "not more than string" means, and your last line reiterates my last sentence. So why the "but"?

The second bullet point does

The second bullet point does not describe "not more than string".

Ordering is backwards

Superclasses are usually conceived as supertypes of their subclasses.

So must be at least string.

More examples

Consider the following code:

def foo[T](t : T) = t;

val aCat : Cat = ...;
val aDog : Dog = ...;
var x = foo(aCat) // typeof(x) :> Cat
x = aDog;         // typeof(x) :> Mammal

So the typeof(x) isn't exactly Cat after the foo call, it is just at-most Cat. The second assignment to aDog then causes x's type to be at most Mammal (the intersection of cat and dog).

We didn't really need the dummy foo call to achieve this:

val aCat : Cat = ...;
val aDog : Dog = ...;
var x = aCat; // typeof(x) :> Cat
x = aDog;     // typeof(x) :> Mammal

Basically assignment, binding, and return create at-most type constraints.

My idea for global inference doesn't work so great for functional structures, consider:

abstract trait List {
  abstract def ForEach(a); 
}
trait Empty :: List {
  override def ForEach(a) = {};
}
trait Prepend(val At, val Rest) :: List {
  override def ForEach(a) = {
    a(At); // so a <: Action[ON], a.ON :> typeof(at)
    Rest.ForEach(a); // Rest <: List...
  }
}

The inference algorithm could infer that the typeof(At) is actually a type parameter of List so it can be used to type the declaration of ForEach in List:

abstract trait List[T] {
  abstract def ForEach(a : Action[ON :> T]); 
}
trait Empty :: List {
  override def ForEach(a) = {};
}
trait Prepend(val At : T, val Rest : List) :: List {
  override def ForEach(a) = {
    a(At); 
    Rest.ForEach(a);
  }
}

But if we follow through and do that on Rest, we'll add type parameters to List forever. So we either have to cut off or disallow recursive type inference, or not bother at all with creating new type parameters, rejecting the above code as incorrectly typed. Since we can't create type parameters, the type system is quite limited, but still very useful in expressing typical OO imperative constructions.

So let's look at a sane explicitly annotated definition of List:

abstract trait List[T] {
  abstract def ForEach(a : Action[/* ON :> T - inferred */]); 
}
trait Empty :: List {
  override def ForEach(a) = {};
}
trait Prepend(val At : T, val Rest : List[T : T]) :: List {
  override def ForEach(a) = {
    a(At); /* infers a.ON :> T */
    Rest.ForEach(a);
  }
}

List[T : T] is an explicit type constraint on Rest.T to be at least this.T. Now let's call ForEach on a list:

val list : List = ...;
val a : Action = x => x.doAnimalStuff(); /* infer a.ON <: Animal */
list.ForEach(a);

By our constraints we have

list.T <: a.ON <: Animal

so...we can infer by transitivity that:

list.T <: Animal

Or do we? Actually, expressions should have their own names, so the action is actually an anonymous something:

val list : List = ...;

var a : Action = ($a) x => x.doAnimalStuff(); /* infer $a.ON <: Animal, a :> $a */
list.ForEach(a); /* infer a.ON :> list.T

So we really have

a.ON :> $a.ON (given a :> $a) 
and
$a.ON <: Animal
and
list.T <: a.ON 

Ugh, so what can we say about that? The problem is the assignment to val a, since we don't have equivalence, we just say that "a" could be at most $a, and when we call ForEach, the constraint is not really propagated as we really want (a could have been reassigned to another type somewhere else). So that is still something to figure out. (Co/contra) variance always gets us in the end!

Variance!

So my parent post got sort of whack at the end: it turns out I have a big problem with co and contravariance, which shouldn’t be so surprising but here I am. Here are some observations: an “at-least” type constraint of some type parameter T is not just some bound, it constrains what values can be assigned to T: if T

trait Cell[V] { var Value : V; } 

var    c = Cell[V : Dog];  // typeof(c) :> Cell[V <: Dog]
if (b) c = Cell[V : Cat];  // typeof(c) :> Cell[V <: Cat]
                           // typeof(c) :> Cell, (Dog + Cat) :> c.V :> (Dog * Cat)
object foo;
c.Value = foo;         // foo <: c.V <: (Dog + Cat), c.V :> (Dog * Cat * foo) 
var k = c.Value;       // typeof(k) :> c.V :> foo, foo <: typeof(k)

Ok, so that’s weird, after the third statement, c.V’s at least type is the union of Dog and Cat (a mythical dog cat), while its at most type is Mammal (Dog intersected with Cat). Variance works out because “at-least” types are used to constrain assignments (so “foo” must be a cat and dog) while “at-most” types are used to constraint evals (so “k” is only guaranteed to be a mammal). Yikes! What does colon “:” mean then? In Scala, I think “:” means “<:” (we write V &lt: Dog, not V : Dog) but that doesn’t make sense in my type system, “V : Dog” is really invariant and means something like “Dog :> V <: Dog” if we want the above results. We also need the following rule to capture the invariance of type member parameters in :

if A :> B and B.T :> C then A.T :> C
if A :> B and B.T <: C then A.T <: C

I’m not sure yet if the dual rule also applies to A <: B.