Subtype + type inference + parametric polymorphism = argh
I’ve generally been a big fan of Fortress’ multiple dynamic dispatch. Although it complicates overloading, it provides a lot of room for specialization through polymorphism that is unseen in just about every other OO language. This summer, when Justin and I were coming up with the semantics for overloading generic and non-generic functions, we punted on the issues that arise from static type inference; i.e., if I elide the static parameters in a function call and statically a non-generic overloading is chosen, then do I infer those static type parameters at runtime given that a generic overloading is chosen then?
Today David, Jan, and Guy tried to figure out what exactly to do about this and their answer seems to involve runtime constraint solving on function calls. Static constraint solving is harder since all the types represent all their subtypes also — at runtime your types are the actual tags or object types, so you don’t need to consider subtyping under them. But still, performing unification on function calls at runtime seems absolutely terrible! What if such an overloaded, static-type-inferred function call occurs in a loop and hit a bajillion times? Hopefully we can do a lot of work at link time since the whole type hierarchy would be known. (Right?)
As if that weren’t enough of a pickle, I just realized a further problem: surprise, surprise, it’s about coercions! Users define coercions within the declaration of the target type, and all coercions should be added statically; i.e., if an expression needs to be coerced at all, then statically it will be wrapped inside a coercion to some target type. This sounded like it might conflict with the dynamic dispatch and runtime unification for type inference, so I tinkered around with some examples. Consider the following:
(* Declared overloadings of `f`. *) f(x: Object, y: Object): Object f[\T <: Num[\T\]\](x: T, y: T): T (* Call site *) n: Object = (* some ZZ32 *) f(n, 1)
Statically, the first overloading is picked and the `1` is not coerced (`n` has type Object, which is not a subtype of Num[\T\] for any T, and `1` has type IntLiteral, which is trivially less than Object). But at runtime we’re either stuck with the first overloading (yuck) or we dynamically choose to coerce `1` to type ZZ32 (yuck, but less so). If the former, we are choosing a much less specific overloading than we could be. If the latter, we are violating the principle that all coercions are decided statically!