5 ms·

The Idris example seems to need further explanation: > In Idris, we can say "the add function takes two integers and returns an integer, but its first argument

The Idris example seems to need further explanation: > In Idris, we can say "the add function takes two integers and returns an integer, but its first argument must be smaller than its second argument": > add : (x : Nat) -> (y : Nat) -> {auto smaller : LT x y} -> Nat > add x y = x + y That's all well and good, if you know the values of x and y at compile time. Consider a program that reads x and y from STDIN. The user could provide an x that is equal to or larger than y (or could provide only one value, or values that are not numbers). I see no way to deal with that except to throw a runtime error. Is that what would happen?

platz 10y ago
not in idris, because it would force you to do that check manually and pass in the evidence as proof. it has a bunch of tools to help you do this.. namely lifting values into types with 'dependent pairs'. idris doesnt automagically calculate everything for you, but makes sure at compile time, that you provide evidence at run time for the things you have asserted in the types. it makes more sense after going through some of the tutorials and books.
NhanH 10y ago
I do NOT know anything about Idris, but I'd imagine you have to do a check along the line of `if (x<y) then` before being able to call `add`, within that block-scope, the compiler should be able to infer that x<y. Typescript has something similar, where if you do `if (foo)`, the compiler will know that foo can't be null or undefined.
_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.
seanwilson 10y ago
> That's all well and good, if you know the values of x and y at compile time. Consider a program that reads x and y from STDIN. The user could provide an x that is equal to or larger than y (or could provide only one value, or values that are not numbers). I see no way to deal with that except to throw a runtime error. Is that what would happen? Before you could call "add", you would have to add a branch/condition to verify "x" and "y" met the pre-conditions. The compiler would then know from the context of where you called "add" that the pre-conditions were always met. As you couldn't guarantee the pre-conditions were always met, you would have a code branch that decides what to do when the pre-conditions aren't satisfied. The important difference to other languages though is that the compiler enforces that you're never allowed to call "add" unless you know the inputs satisfy the pre-conditions.
continuational 10y ago
x = readFromStdin y = readFromStdin if(x < y) { // in this scope, you have proven x < y } else { // in this scope, you have proven x >= y }
doomrobo 10y ago
x and y do not have to be known at compile time. If I let y be a random Nat, and x be y - 1 (or 0 if y == 0), then I can statically prove that LE x y.
lanna 10y ago
To draw an analogy with more mainstream type systems, say you have a function like add(x: Int, y: Int): Int (takes two integers and returns an integer). Now, somewhere else in your code, you have something like: x = readline() y = readline() add(x, y) That won't compile because readline returns string and add expects integers. Somewhere between readline and add you'll have to convert the strings to integers, and that piece of code (not the add function) is the one that has to be concerned with things like the user entering "abc" where a number is expected. As far as the add function itself is concerned, it will always be invoked with two integers; the burden of proof is on the caller.
exDM69 10y ago
> Consider a program that reads x and y from STDIN. A program like this should fail to compile! You can't feed two arbitrary numbers from stdin to the "add" function above. In order to make it compile, you'd need to add some logic that uses min/max to swap the values so x is less than y.

platz 10y ago

not in idris, because it would force you to do that check manually and pass in the evidence as proof. it has a bunch of tools to help you do this.. namely lifting values into types with 'dependent pairs'. idris doesnt automagically calculate everything for you, but makes sure at compile time, that you provide evidence at run time for the things you have asserted in the types. it makes more sense after going through some of the tutorials and books.

NhanH 10y ago

I do NOT know anything about Idris, but I'd imagine you have to do a check along the line of `if (x<y) then` before being able to call `add`, within that block-scope, the compiler should be able to infer that x<y. Typescript has something similar, where if you do `if (foo)`, the compiler will know that foo can't be null or undefined.

_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.

seanwilson 10y ago

> That's all well and good, if you know the values of x and y at compile time. Consider a program that reads x and y from STDIN. The user could provide an x that is equal to or larger than y (or could provide only one value, or values that are not numbers). I see no way to deal with that except to throw a runtime error. Is that what would happen? Before you could call "add", you would have to add a branch/condition to verify "x" and "y" met the pre-conditions. The compiler would then know from the context of where you called "add" that the pre-conditions were always met. As you couldn't guarantee the pre-conditions were always met, you would have a code branch that decides what to do when the pre-conditions aren't satisfied. The important difference to other languages though is that the compiler enforces that you're never allowed to call "add" unless you know the inputs satisfy the pre-conditions.

continuational 10y ago

x = readFromStdin y = readFromStdin if(x < y) { // in this scope, you have proven x < y } else { // in this scope, you have proven x >= y }

doomrobo 10y ago

x and y do not have to be known at compile time. If I let y be a random Nat, and x be y - 1 (or 0 if y == 0), then I can statically prove that LE x y.

lanna 10y ago

To draw an analogy with more mainstream type systems, say you have a function like add(x: Int, y: Int): Int (takes two integers and returns an integer). Now, somewhere else in your code, you have something like: x = readline() y = readline() add(x, y) That won't compile because readline returns string and add expects integers. Somewhere between readline and add you'll have to convert the strings to integers, and that piece of code (not the add function) is the one that has to be concerned with things like the user entering "abc" where a number is expected. As far as the add function itself is concerned, it will always be invoked with two integers; the burden of proof is on the caller.

exDM69 10y ago

> Consider a program that reads x and y from STDIN. A program like this should fail to compile! You can't feed two arbitrary numbers from stdin to the "add" function above. In order to make it compile, you'd need to add some logic that uses min/max to swap the values so x is less than y.