20
$\begingroup$

I am starting a personal bibliographic research on type-checking algorithms and want some tips. What are the most commonly used type-checking algorithms, strategies and general techniques?

I am particularly interested in complex type-checking algorithms that were implemented in widely known strongly static typed languages such as, for example, C++, Java 5+, Scala or others. I.E, type-checking algorithms that are not very simple due to the very simple typing of the underlying language (like Java 1.4 and below).

I am not per se interested in a specific language X, Y or Z. I am interested in type-checking algorithms regardless of the language that they target. If you provide a answer like "language L that you never heard about which is strongly typed and the typing is complex has a type-checking algorithm that does A, B and C by checking X and Y using the algorithm Z", or "the strategy X and Y used for Scala and a variant Z of A used for C# are cool because of the R, S and T features that works in that way", then the answers are nice.

$\endgroup$
14
  • 3
    $\begingroup$ Maybe you should edit this question to ask about type checking for one specific language. Open-ended, list-style questions are generally discouraged on SE (though this particular site doesn't have a policy regarding that yet). Also: <type-system-elitist>Java's type system isn't complex</type-system-elitist>. $\endgroup$
    – sepp2k
    Mar 9, 2012 at 8:41
  • 3
    $\begingroup$ Perhaps the question could be rephrased to be more specific, but I don't think it should be closed. $\endgroup$ Mar 9, 2012 at 9:38
  • 1
    $\begingroup$ @sepp2k: I know that it is a bit broad, but ended this way because I don't want to limit the usefulness of the answers. BTW, I did not understand what you want to say with "<type-system-elitist>Java's type system isn't complex</type-system-elitist>". Java's 1.4 and below type system in fact were simple, but whit generics in Java 5, it became a lot more complex. $\endgroup$ Mar 9, 2012 at 12:09
  • 2
    $\begingroup$ Asking for one particular language would make the question more unsuited for this site, imho. The question should maybe ask for general techniques. $\endgroup$
    – Raphael
    Mar 9, 2012 at 16:33
  • 1
    $\begingroup$ @Victor A basic tool are Attribute Grammars. You will maybe not be able to do every wicked thing you can imagine with them, but they are a good starting point. $\endgroup$
    – Raphael
    Mar 12, 2012 at 19:34

2 Answers 2

14
$\begingroup$

Most research does not actually publish the type checking algorithms for full blown programming languages. You will find some formalisations of a large part of the type systems for full programming languages, such as the work done by Drossopoulou and Eisenbach for Java or Nipkov et al's work on C++. More often, though, you will only find the type systems for some core part of the language (Featherweight Java is one example) or for the core concepts of a language such as the local type inference approach of scala.

In conferences such as POPL and ICFP you will find many type checking algorithms for specific kinds of type systems, and novel approaches such as bidirectional and tridirectional type checking.

More generally, you probably need to know about the Damas-Milner algorithm, local type inference, bidirectional and tridirectional type checking, and expand from there, by following references in the papers and by using google scholar to find which papers cite these and build on the approaches described. Also, as suggested above, conferences such as POPL, ICPF, ESOP and even ECOOP and OOPSLA will have papers relevant to your quest.

$\endgroup$
2
  • $\begingroup$ Afaik, Scala's type system has been developed in research projects and is thusly published. The compiler is open-sourced, too. Have not looked into either, though. $\endgroup$
    – Raphael
    Mar 9, 2012 at 16:37
  • $\begingroup$ No need for me to infer; I know that there are published papers on Scala's type system. This claim is readily checked by searching. Also, I count the compiler's source code as sufficient publication on the algorithm (provided it is included in the sources; I assume so but did not check). My initial statement was ambiguous, true, but your reaction seems unwarranted. $\endgroup$
    – Raphael
    Mar 10, 2012 at 11:20
2
$\begingroup$

A basic tool are Attribute Grammars. You will maybe not be able to do every wicked thing you can imagine with them, but they are a good starting point.

Essentially, you can walk over a program's abstract syntax tree top-down and/or bottom-up and pass information around. So, for instance, you could pass global scope type information (e.g. classes and their members) downwards and determine the type of expressions recursively, i.e. bottom-up, passing the resulting types upwards.

Find some explanation and examples in the slides here (Chapter 5).

$\endgroup$
2
  • $\begingroup$ Does somebody have a better reference? I guess I need to buy the Dragonbook or Wilhelm/Maurer one of these days... $\endgroup$
    – Raphael
    Mar 12, 2012 at 23:11
  • 1
    $\begingroup$ The tool JastAdd is an excellent, modern compiler compiler system based on reference attribute grammars. We've used it in a number of projects. $\endgroup$ Mar 13, 2012 at 7:44

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.