Building Types Better, One Brick at a Time: How Constructive Type Theory Lays the Foundation for Your Program

Constructive Types, Introduction and Elimination, with Scala Examples

Constructive type theory treats types as more than labels. A type comes with concrete ways to build values and to use them, so “having” a value of a type is evidence that you can construct it and operate on it. This view yields the Curry–Howard idea, where types correspond to propositions and values correspond to proofs. A value of type A is a proof that A holds because you can exhibit an instance of A. Unlike classical logic, where non-constructive proofs may assert existence by contradiction, constructive type theory ties meaning to construction and use.

Constructiveness appears directly in the rules that introduce and eliminate each type. Introduction rules show how to make values. Elimination rules show how to take values apart or use them. From these rules we obtain computational content. Every proof tells us how to compute with the value it proves. This is why constructive type theory pairs elegantly with programming, since types describe both shape and behavior.

Constructive systems usually avoid non-constructive principles such as the Law of Excluded Middle for arbitrary propositions. The issue is not philosophical flair, it is that excluded middle does not tell you how to build a witness for either side. Constructive reasoning prefers evidence that can be executed.

Booleans exist constructively because we can introduce true and false and eliminate them with a conditional. Functions exist because we can introduce a function by writing a rule from inputs to outputs and eliminate a function by applying it to an argument.

Natural numbers illustrate this pattern well. We introduce 0 and we introduce a successor operation written s(n). We eliminate natural numbers by recursion or by pattern matching that distinguishes 0 from s(n). This pair of rules gives the type a concrete meaning. We can make numbers and we can consume them predictably.

Why Constructiveness Matters

Programming benefits from this discipline because types become executable specifications. If a program inhabits a type, you hold code that a compiler can run and a verifier can check. This improves reliability, documents intent, and supports modular reasoning. Introduction and elimination then serve as a simple contract. They say how to create values and how to use them, with no gaps.

We presents Martin-Löf Type Theory, often abbreviated as MLTT, as a constructive foundation where propositions are types and proofs are programs. We state how MLTT supports an operational equivalence between value-level programs, abbreviated as VLPs, and type-level programs, abbreviated as TLPs. We also sketch an algorithm that translates VLPs into TLP proofs.

MLTT is a constructive system in which a term inhabiting a type is a proof of the corresponding proposition. Dependent types allow a type to depend on a value, so properties can vary with inputs. Functional languages can encode such proofs, since function application corresponds to proof construction. In our work we use Scala 3. It runs on the JVM, integrates with existing bytecode libraries, and provides strong typing with higher-kind types, path-dependent types, and union and intersection types. Its implicit mechanism with given and using closely mirrors proof search, because the compiler resolves contextual evidence automatically.

In MLTT a proof must be explicitly constructed, yet proof assistants automate search by applying dependent functions and introduction or elimination rules. Scala 3 behaves similarly at compile time. A given value stands for a proof of a type. A function that requires contextual parameters stands for a theorem that needs proofs of its premises. The compiler searches the context and supplies them when available. This pattern is enough to mechanize many small constructive proofs, such as those that appear in examples of Peano arithmetic elsewhere in this article.

The basic idea is illustrated with a minimal Scala 3 snippet. The code is shown below and available from my Github repo.

import scala.util.NotGiven

trait A
trait B
trait C

given proofAB(using a: A): B = new B {}
given vacuous(using NotGiven[A]): B = new B {}
given aGiven: A = new A {}

val bOK: B = summon[B]  // resolved by proofAB, or by vacuous if A is absent
val cFail: C = summon[C] // does not compile, no proof of C in scope

Here, proofAB encodes “A implies B” by requesting A as contextual evidence to construct B. The declaration aGiven supplies that evidence. The definition vacuous uses NotGiven[A] as a stand-in for the absence of A, which you can read as “not A.” If A is missing, the compiler may still construct B by the vacuous path. Attempting to summon C fails at compile time, which is the desired outcome when no proof exists.