2
$\begingroup$

I am trying to get some basic terminology down related to type theory, and am currently on understanding the difference between "constructive type theories" and "nonconstructive type theories", as mentioned here:

Like first-order logic, Church’s type theory is classical in the sense that it admits nonconstructive reasoning principles such as the law of excluded middle and double negation elimination. P. Martin-Löf introduced in 1972 a constructive form of type theory now known as Martin-Löf type theory [42]. Most constructive type theories, including Martin-Löf type theory, embody the Curry-Howard isomorphism [33] that elegantly connects proving theorems in type theory to writing programs in lambda calculus. Constructive type theories also have a close connection to category theory and have been extensively used to formalize constructive mathematics and ideas from theoretical computer science [12, 39].

Wikipedia's example of constructive vs. nonconstructive proofs doesn't help elucidate the concepts. I am not entirely sure this has to do with Constructivism in Mathematics, but it seems like it.

What is meant exactly by constructive vs. nonconstructive in terms of type theory? What is an example to demonstrate the difference between constructive and nonconstructive type theories? How would I explain the difference between constructive and nonconstructive type theories to a non-mathematician, such as a software engineer?

$\endgroup$
2
  • $\begingroup$ In your quote: "nonconstructive reasoning principles such as the law of excluded middle and double negation elimination". I suggest you look up these principles first. $\endgroup$ – Zhen Lin Sep 29 '20 at 5:45
  • $\begingroup$ How you would explain those things to a software engineer may depend very much on how they encounter/interact with type theory. I don't know enough to answer this sort of question. But given the relationship between constructive mathematics and programs (e.g. the work of Martin-Löf), I imagine that for many software engineers, the answer is "nonconstructive type theory is something you won't encounter/have to worry about at all". $\endgroup$ – Mark S. Sep 29 '20 at 12:40
3
$\begingroup$

As it is mentionned in the quoted text, the different between constructive and nonconstructive type theory has to do with constructivism in Mathematics. As there are many variations of constructive mathematics, it is just impossible to give an accurate meaning of the difference between constructive, and nonconstructive.

But there is also technical meaning to constructivity in type theory. A type theory is constructive if it enjoys the canonicity property: every term of a given type computes to a canonical form, that is a combination of the sole constructors of that type.

Using nonconstructive axioms such as excluded middle, you can prove the existence of a term of a given type, but you are not able to compute that term (in a canonical form).

$\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.