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:
3 in the input box above. A button shall appear
letting you download
Prime3.scala. Run it via
The file should compile and run flawlessly outputting
ForAllCons(NotDivRec(NotDivBasic(ListIsPositive(),LTTrivial()),AddPlus1(AddZero())),ForAllNil()). Look into
you should see a value
prime3: Prime[_3] defined. The
main method simply outputs this value.
4 in the input box. Download and run
The file should compile but execution should failed with the exception
scala.NotImplementedError: an implementation is missing. Look into
prime4: Prime[_4] is defined by
Prime4.scala carefully, starting from the beginning, and try to write a valid
val prime4: Prime[_4]. Remember to follow very scrupulously the rules
stated in the first comment of
val prime4: Prime[_4], NOT A
def prime4: Prime[_4], NOT A
lazy val prime4: Prime[_4]!
Try 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:
and so on:
type _0 = String type _1 = List[_0] // List[String] type _2 = List[_1] // List[List[String]] type _3 = List[_2] // List[List[List[String]]] type _4 = List[_3] // List[List[List[List[String]]]] type _5 = List[_4] // List[List[List[List[List[String]]]]]
The next step is to define the type
Prime[N] such that:
There exists a valid of type
Prime[N]if and only if
Nis (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).
n is prime if and only if for all natural number m such that 2 ≤ m < n, then m does not divide n.
ForAll[X, N] encodes this exact property. There exists a value of type
ForAll[X,N] if and only if both:
X ≤ N
X ≤ M < N,
Mdo not divide
Actually the type
Prime[N] is an alias for
ForAll[_2, N]. We need to encode two more properties:
Jtwo natural numbers, the property that
Iis less than or equal to
I ≤ J). It is encoded as the type
Jtwo natural numbers, the property that
Idoes not divide
J. It is encoded as the type
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.