5 ms·

The missing explanation is that `smaller` is a third argument to the function. It's type is a proof that x <= y. Since it is in curly brackets with the auto key

by _ibu9 10y ago

The missing explanation is that `smaller` is a third argument to the function. It's type is a proof that x <= y. Since it is in curly brackets with the auto keyword, the compiler will fill in this proof in many cases, like when the values are statically known. In the case where the values are read from the external environment, first you would have to compare them before calling the function. The comparator would return either a proof that x <= y, or x > y. In the first case you plug that value into the `smaller` argument, in the second case it's your responsibility to signal whatever kind of application-specific error is appropriate (assuming x > y is some kind of erroneous condition).

platz 10y ago
though the comparator cannot return just a boolean, because it could be 'wrong'. this is where the dependent constructs come in to make sure the answer is correct
deleted 10y ago
[deleted]
twblalock 10y ago
What would happen if you did not compare them before calling the function, and just passed them in such that x >= y?
- seanwilson 10y ago
  > 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.
  - twblalock 10y ago
    Assuming they were integers before, what type would they become after they were compared?
    - kazagistar 10y ago
      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.
      - platz 10y ago
        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.
        jackmott 10y ago
        that is pretty awesome
    - lmm 10y ago
      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.
- icen 10y ago
  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!
  - chriswarbo 10y ago
    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 http://chriswarbo.net/blog/2014-12-04-Nat_like_types.html
- bo1024 10y ago
  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.
- mike_hearn 10y ago
  Maybe an analogy to a more mainstream language helps. I like using Kotlin these days: http://kotlinlang.org/ 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.

by _ibu9 10y ago

platz 10y ago

though the comparator cannot return just a boolean, because it could be 'wrong'. this is where the dependent constructs come in to make sure the answer is correct

deleted 10y ago

[deleted]

twblalock 10y ago

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

seanwilson 10y ago
> 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.
- twblalock 10y ago
  Assuming they were integers before, what type would they become after they were compared?
  - kazagistar 10y ago
    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.
    - platz 10y ago
      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.
      - jackmott 10y ago
        that is pretty awesome
  - lmm 10y ago
    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.
icen 10y ago
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!
- chriswarbo 10y ago
  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 http://chriswarbo.net/blog/2014-12-04-Nat_like_types.html
bo1024 10y ago
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.
mike_hearn 10y ago
Maybe an analogy to a more mainstream language helps. I like using Kotlin these days: http://kotlinlang.org/ 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.