Today we will explore the Curry–Howard correspondence. Our mission is writing, in Scala’s type system, the property on natural number of being prime. Wikipedia defines it by:
A natural number (1, 2, 3, 4, 5, 6, etc.) is called a prime number (or a prime) if it is greater than 1 and cannot be written as a product of two natural numbers that are both smaller than it.
An equivalent way to put it is:
A natural number is prime if it is greater than 1 and cannot be divided by any natural number greater than 1 but smaller than it.
These definitions are equivalent as, by definition, any natural number n is divisible by k if and only if it can be written n = k × p for some natural number p.
Writing a program whose execution checks whether a number is prime is easy. But we are not interested in executing programs, only compiling them! We want the compiler to verify that a number is indeed prime. At that point, you may wonder how it is even possible to use the compiler to “prove” something about numbers. That’s exactly the point of the Curry–Howard correspondence
You can write any positive integer in the input bow below:
Please write 3 in the input box above. A button shall appear
letting you download Prime3.scala. Run it via
scala Prime3.scala
The file should compile and run flawlessly outputting ForAllRec(NotDivRec(NotDivBase(SIsPositive(),LTBase()),AddPlus1(AddZero())),ForAllBase()). Look into Prime3.scala,
you should see a value prime3: Prime[_3] defined. The main method simply outputs this value.
Now, write 4 in the input box. Download and run Prime4.scala via
scala Prime4.scala
The file should compile but execution should failed with the exception scala.NotImplementedError: an implementation is missing. Look into Prime4.scala,
the value prime4: Prime[_4] is defined by ???.
Read Prime4.scala carefully, starting from the beginning, and try to write a valid
definition for val prime4: Prime[_4]. Remember to follow very scrupulously the rules
stated in the first comment of Prime4.scala.
val prime4: Prime[_4],
NOT A def prime4: Prime[_4],
NOT A lazy val prime4: Prime[_4]!prime4Try to find valid values of type Prime[_N] when is not a prime number.
To encode properties over natural number, we need to start by encoding natural numbers.
To do so, we associate to any natural number a type. Natural numbers can be constructed
by starting from the first one, 0, and creating new ones by adding 1 successively.
For example, 1 = 0 + 1, 2 = 0 + 1 + 1, 3 = 0 + 1 + 1 + 1, etc.
Our encoding will mimic this construction, starting from a base type encoding 0 and
an operation "+ 1".
The number 0 is encoded as the type _0 defined as the final abstract class _0
and the operation "+ 1" as the type function final abstract class S[N <: Nat] which
for every type N encoding a natural number n gives the type S[N] encoding the
natural number n + 1. The type Nat can simply be defined as the alias
type Nat = _0 | S[?] because a natural number is either 0 or obtained by some + 1 operations.
type Nat = _0 | S[?]
final abstract class _0
final abstract class S[N <: Nat]
type _1 = S[_0]
type _2 = S[_1] // S[S[_0]]
type _3 = S[_2] // S[S[S[_0]]]
type _4 = S[_3] // S[S[S[S[_0]]]]
type _5 = S[_4] // S[S[S[S[S[_0]]]]]
...
The next step is to define the type Prime[N] such that:
There exists a valid value of type
Prime[N]if and only ifNis (the type associated to) a prime number.
Let n be a natural number and N its associated type (for example n=3 and N = _3).
Then:
n is prime if and only if for all natural number m such that 2 ≤ m < n, then m does not divide n.
The type ForAll[X, N] encodes this exact property. There exists a value of type ForAll[X,N] if and only if both:
X ≤ NM such that X ≤ M < N, M do not divide NActually the type Prime[N] is an alias for ForAll[_2, N]. We need to encode two more properties:
I and J two natural numbers, the property that I is less than or equal to J (I ≤ J).
It is encoded as the type LessThan[I, J].I and J two natural numbers, the property that I does not divide J.
It is encoded as the type NotDiv[I, J].Read the file PrimeN.scala carefully, each step is described and explained in much details.
Why asking you to build a value that not exists? Because the main point is not knowing whether there
exists a value of type Prime[_4] but understanding why such a value (following all the rules!) cannot exists!
It is widely known and accepted in programming culture that every type has values. After all, types exists only
to qualify values, right? And instantiating a type T is as simple as calling new! There is one huge problem
with this claim: it is completely wrong!. The idea that a types can have no value, often called empty type
or uninhabited type, is the cornerstone of a lot of techniques including logic, maths, programming with rich types,
formal systems like Coq, etc.
This example is indeed both complicated and complex. It is neither a regular usage of GADTs nor something meant for production! It’s perfectly ok being confused about it or not understanding what is going on. As I said, it is an complicated and complex example!! But when you manage to understand it, consider you master the subject.