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].
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?