2
$\begingroup$

The type theory that I have seen is all developed over lambda calculus, which is an inherently functional language.

Nevertheless, in practice imperative languages have type systems. Are there differences in the type theory for imperative vs functional languages?

Improve this question
$\endgroup$
1
  • 1
    $\begingroup$ Why is the lambda calculus "inherently functional"? You can easily add mutable state to a lambda calculus (which is basically what SML and O'Caml do), and you have a higher-order imperative programming language. It's not hard to encode the lambda calculus into most object oriented programming languages (even ones without lambdas themselves, e.g. earlier Java) essentially via the Strategy Pattern. $\endgroup$ – Derek Elkins left SE Jul 4 '19 at 20:51
4
$\begingroup$

Sure there are type systems for all sorts of programming languages, including the imperative ones. It's probably best to look at something simple first that exposes the gist of the matter. A classic is John Reynold's The essence of algol, which was quite influential historically, and develops many important ideas.

Improve this answer
$\endgroup$
2
$\begingroup$

You might want to look at chapters 13 and 19 of Types and Programing Languages that handle types for constructs with side-effects, and a more general imperative language (Java) respectively.

As Andrej says, the type system community is aware of imperative languages (indeed, I know of very few completely pure systems!), and theory has developed accordingly.

Improve this answer
$\endgroup$

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.