What's even more interesting is the structure of "LT a b". Let's assume that Nat has the common Peano arithmetic structure:
data Nat : Type where
Zero : Nat
Succ : Nat -> Nat
Here "Zero" represents zero and "Succ" represents "one more than". Hence "Succ (Succ (Succ Zero))" is one more than one more than one more than zero, AKA three.
Given two such values "x" and "y", how on Earth can we prove that "x Well, there's a really obvious case: we know that "x
Obv : (x : Nat) -> LT x (Succ x)
Notice that we don't write "y" explicitly, since it can be written in terms of "x".
What about those cases where "x" and "y" differ by some other amount? We could define values for "x
Ind : (x : Nat) -> (y : Nat) -> LT x y -> LT x (Succ y)
This is enough to prove that "x" is less than any number greater than "x". In fact, we don't need to give the values of "x" and "y" explicitly, as they appear in the "LT x y" types and can hence be inferred. In languages like Idris we indicate inferrable parameters using braces, hence our "LT" type looks something like this:
data LT : Nat -> Nat -> Type where
Obv : {x : Nat} -> LT x (Succ x)
Ind : {x : Nat} -> {y : Nat} -> LT x y -> LT x (Succ y)
Now, this looks familiar. Compare it to the definition of "Nat": we have two constructors, one of which ("Zero"/"Obv") can be written on its own, whilst the other ("Succ"/"Ind") is recursive, requiring an argument containing the same constructors.
Values of type Nat include:
Zero : Nat
Succ Zero : Nat
Succ (Succ Zero) : Nat
And so on, whilst values of "LT x y" include:
Obv : LT x (Succ x)
Ind Obv : LT x (Succ (Succ x))
Ind (Ind Obv) : LT x (Succ (Succ (Succ x)))
Although LT contains more static information than Nat, it actually follows exactly the same structure. What does this mean? Values of type "LT x y"
are numbers; in particular they're the
difference between "x" and "y"!
In the case of "LT", these numbers start counting from one (since one number is not less than another if their difference is zero). If we define a similar type for "x " and ">=".
These types are actually really useful. They're also closely related to linked lists, vectors, etc. although they store dynamic information as well as static.
I assume this is all old hat to those with mathematical training, but I found it interesting enough to write about at http://chriswarbo.net/blog/2014-12-04-Nat_like_types.html