9
$\begingroup$

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?

$\endgroup$
  • $\begingroup$ What you are describing has hints of bidirectional type inference, unless I'm mistaken. Describing what you are trying to do may clarify, however. $\endgroup$ – Dominic Mulligan Nov 28 '11 at 9:57
  • $\begingroup$ Are you asking because you seek a way to specialize polymorphic functions? $\endgroup$ – nponeccop Nov 28 '11 at 9:59
  • $\begingroup$ I'm mostly just trying to learn more about type systems really, and yes, I was thinking mostly about how to handle polymorphic functions (and method calls in OO languages, the same thing). I'm trying to identify the right terms for this so I can read up on it. $\endgroup$ – Derek Thurn Nov 28 '11 at 15:55
11
$\begingroup$

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

$\endgroup$
  • $\begingroup$ The Pierce and Turner paper was very enlightening, thanks. Are you aware of a minimal implementation of the algorithm they describe in code? I think that would be very interesting to look at as well, if it exists. $\endgroup$ – Derek Thurn Nov 28 '11 at 19:23
  • $\begingroup$ I don't know of any minimal implementations. There's one in Typed Racket, and one in Scala, but both implement substantially more complicated algorithms. $\endgroup$ – Sam Tobin-Hochstadt Nov 28 '11 at 20:49
0
$\begingroup$

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.

$\endgroup$
  • 1
    $\begingroup$ "OO virtual method calls are completely different thing called ad-hoc polymorphism" Ad-hoc polymorphism is another name for overloading. You seem to confuse it with subtype polymorphism. $\endgroup$ – Radu GRIGore Nov 28 '11 at 16:54
  • $\begingroup$ But subclasses are not necessarily subtypes, aren't they? E.g. for subtypes LSP is supposed to hold. $\endgroup$ – nponeccop Nov 28 '11 at 17:11
  • 1
    $\begingroup$ True, but beside the point. "Subtype polymorphism" is the standard term. See en.wikipedia.org/wiki/Subtype_polymorphism for details. $\endgroup$ – Radu GRIGore Nov 28 '11 at 18:27

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.