Take the 2-minute tour ×
Computer Science Stack Exchange is a question and answer site for students, researchers and practitioners of computer science. It's 100% free, no registration required.

I've noticed that some languages include a logic engine as part of their type system (e.g. Shen, Typed Clojure).

Other languages have a much more direct type checking algorithm (e.g. Haskell / Hindley-Milner).

What specific features of a type system make it necessary to include a logic engine?

share|improve this question
add comment

1 Answer

I'm not sure where you would draw the line between "direct type checker" and "logic engine". In a deep sense every type checker for a modern type system is a theorem prover (or proof-checker; more on this in a moment). The theorem to be proven is "the program is well-typed", or "this function has type X".

Modern type systems and their checking/inference algorithms tend to be specified in terms of logic; typically intuitionistic typed logic (a.k.a. Martin-Löf theory). If you have a look at, say, the paper for the standard Hindley-Milner type inference algorithm [1], you'll see that it's specified abstractly in terms of logic. Let-polymorphism also relies on the Robinson unification algorithm, famously used in Prolog.

I'm going to go out on a limb here and suggest that the degree to which a type inference algorithm resembles a "logic engine" (however you define it) depends on how "decidable" the rules are, and how much "inference" you need to do (as opposed to merely "checking"). The type system of the simply-typed lambda calculus is intuitionistic logic (and I do mean it really is the same thing; this is the famous Curry-Howard correspondence), so you'd think that any type checker for that system is a "logic engine" in any reasonable sense. But because you only need to "check" rather than "infer", it's a proof checker rather than a theorem prover.

The standard introductory reference on this topic is TaPL [2]. If you're at all interested in this topic, it's well worth a read; any well-stocked university library should have a copy.


  1. Principal type-schemes for functional programs by Damas and Milner (1982).
  2. Types and Programming Languages by Benjamin C. Pierce.
share|improve this answer
add comment

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

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