# What is an example of constructive vs. nonconstructive type theory?

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 . Most constructive type theories, including Martin-Löf type theory, embody the Curry-Howard isomorphism  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?

• 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. Sep 29, 2020 at 5:45
• 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". Sep 29, 2020 at 12:40