Hacker News Reader

Comment by twblalock | Hacker News Reader

What would happen if you did not compare them before calling the function, and just passed them in such that x >= y?

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

You can't because the function takes three arguments: an x and y of type integer, and a "z" of type "proof that x < y".

This is the "types as propositions, proofs as instances" Curry-Howard correspondence lightbulb: The type "x < y" is a proposition, and if you can find any z at all of that type, then z is a proof of the proposition. So by passing in such a z that has been verified to have that type, you've certified that x < y.

> What would happen if you did not compare them before calling the function, and just passed them in such that x >= y?

It would be a type error. All the compiler would know is that "x" and "y" are strings/integers so it would tell you they were the wrong type. If you do a branch on checking they are the correct type, then in that part of the branch the compiler will know they are the correct type and allow "add" to be called.

Think about a Java program that takes a string input, converts the string input to an integer type and then passes this to a function that accepts integers only. If you just tried to pass the string to the function directly the compiler wouldn't allow it. Same thing but the type system is more expressive.

Assuming they were integers before, what type would they become after they were compared?

Its not that they change type. Its that the comparison function returns either a proof that one is greater then the other, or that they are equal. When you are in the right branch, you can pass that proof (type) along with the value into other functions.

here's a full code example:

    import Data.String

    -- takes two integers, and a proof that x < y, and yields an integer
    add : 
      (x : Integer) -> 
      (y : Integer) -> 
      (prf : x < y = True) ->     -- require a proof that that x < y
      Integer
    add x y prf = x + y

    main : IO ()
    main = do
      sx <- getLine -- read string from input
      sy <- getLine -- read string from input
      let Just x = parseInteger sx -- assuming int parse is ok, else error
      let Just y = parseInteger sy -- assuming int parse is ok, else error
      case decEq (x < y) True of   -- decEq constructs a proof if x < y is True
        Yes prf => print (add x y prf)
        No => putStrLn "no prf, x is not less than y"

lets say I mess up the sign of the comparison on the case line and write decEq (x > y) instead... then I'd get a type error

    When checking argument prf to function Main.add:
    Type mismatch between
                x > y = True (Type of prf)
        and
                x < y = True (Expected type)

there's no way to construct the prf value artificially, or sneak in different parameters that are unrelated to the prf value.

it's either a compile error or it's valid.

that is pretty awesome

An existential type - "some unknown types x (a subtype of integer) and y (a subtype of integer) for which LT x y" (or else the other branch). Languages designed for these techniques generally make it easier to write those types than it is in say Java (and in some languages it would be impossible to write that type at all) and infer them so you're not constantly writing them, though there's usually a way to express them directly/explicitly if you need to.

Maybe an analogy to a more mainstream language helps. I like using Kotlin these days:

http://kotlinlang.org/

which has nullable types. Imagine this code:

    fun useMessage(msg: Message) { .... }

    val s: Message? = someSocket.readNextMessage()   // Returns null if the socket has been closed.
    useMessage(s)

In Kotlin this would be a type error, the type of 's' is Message? and the question mark means it's possibly null. It won't compile. You can fix it by doing this:

    if (s != null) useMessage(s)

The act of testing 's' restricts its type inside the if block: we've proven it's not null, therefore the compiler will now accept this proof as evidence that the code is safe.

Idris isn't quite the same because it's a lot more general and the proofs are explicit instead of being implicit in the control flow: Idris types don't change when you test them, you get given a proof 'object' instead. But the basic idea is the same; your program does something that proves something about the type of a runtime value and that data can be used to improve program correctness.

Reply on news.ycombinator.com