Research on call-site based type inference?

Question

I'm trying to learn more about whole-program type checking and type inferencing systems that use information from function call sites to compute type information (in addition to the standard approach of using the function body). For example, such an algorithm might use a function call like foo(1) to infer that the function in foo takes integer arguments. Obviously this would complicate inference a lot and make the check non-modular.

Anyway, I haven't had much luck finding any research on this approach, probably because I don't know the correct terminology to describe what I'm talking about. Any pointers?

Answer 1

Almost all systems with type inference use call-site information to do this. Examples include Standard ML, OCaml, F#, and Haskell. Many other languages use call-site information to infer type parameter instantiation, such as Java, C#, Scala, and Typed Racket. This often goes by the name "Local Type Inference".

I would just describe what you're looking for as "Type Inference", and you should probably start by looking up what's commonly known as the "Hindley-Milner" system. The Wikipedia page gives a reasonable introduction, and pointers to the original papers.

The place to start for Local Type Inference is Pierce and Turner's original paper, best read in the TOPLAS 2000 version (ACM, PDF).

Answer 2

You can take a look at type systems for intersection types which can give you something like a :: Int -> Int | Bool -> Bool, so you know that two specializations to Int and Bool are enough, or to use a usual type inference to infer most general types followed by a control flow analysis to collect actual type arguments. In fact there are hybrid approaches (CFA expressed as a type system and vice versa).

Research works on inferring least general types instead of most general types may exist, but I'm unaware of them.

As for techniques to implement polymorphism, two solutions exist: 1) specialization (think of C++ templates) 2) uniform representation assumption (think of C-style collections with void*).

For 2 you don't need the type from call-site during typechecking, and can support separate compilation more easily.

Note that we are talking about parametric polymorphism here, and OO virtual method calls are completely different thing called subtype polymorphism. Note that C++ templates support both something like parametric polymorphism and duck typing, which is yet another form of polymorphism.