Hacker News new | past | comments | ask | show | jobs | submit login

Nothing; it would return a partially applied function that waits for a proof that `x < y` before continuing. (Trying to use that function as an integer would be a type error).

The key here is that `add` is not a function `Nat -> Nat -> Nat`, it is a function `(a : Nat) -> (b : Nat) -> LT a b -> Nat`. There are just some compiler features that allow you to avoid having to write out the full `LT a b` proof each time you want to add things!




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 < y"? What would that even look like?

Well, there's a really obvious case: we know that "x < Succ x", so we can define a value "Obv" which represents this:

    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 < Succ (Succ x)", "x < "Succ (Succ (Succ x))", and so on, but that's clearly redundant and inconvenient. Instead, we just need to spot that all of these fit the pattern "x < Succ y", where "x < y". This lets us argue by induction: if "x < y", then "x < Succ y", which we can represent using a value "Ind" like this:

    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 <= y" it would count from zero, and the same can be done for ">" 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




Guidelines | FAQ | Support | API | Security | Lists | Bookmarklet | Legal | Apply to YC | Contact

Search: