On Using Prolog for Type Checking and Type Inference
Type checking can be seen as a restricted form of type inference: you compare the inferred type with the declared type to see if they are the same. Type inference is essentially the unification of a set of constraints on types (based on the type rules) to arrive at a most general type. Failure to do so (e.g. conflicting constraints) means that an expression is not typable in your type system.
Manfred von Thun recently made the observation that Prolog is well suited for type inference. I don’t know whether or not this is a novel observation but it is definitely interesting. I definitely like the idea of using a separate language, and independant phase for type analysis in my compiler. For those interested in Prolog, I have to grudgingly admit that the Wikipedia entry on Prolog is surprisingly thorough and quite useful.