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?