9 ms·

Because static typing primarily focuses on showing that your types align. This is completely tangential to knowing that the code is doing what you intended. In

Because static typing primarily focuses on showing that your types align. This is completely tangential to knowing that the code is doing what you intended. In fact, it's often at odds with understanding the intent of the code because you're limited to a set of statements that can be verified by the type checker. This can make it harder for the human reader to understand what the code is meant to be doing. For example, it takes nearly 300 lines of code to encode insertion sort using types in Idris https://github.com/davidfstr/idris-insertion-sort/blob/master/InsertionSort.idr https://github.com/davidfstr/idris-insertion-sort/blob/maste... A human reader has to be able to read that and understand that the types are encoding the intent correctly. I don't know about you, but I have a much easier time knowing whether the dynamically typed version in Python is correct or not: def insertionSort(lst): for index in range(1, len(lst)): currentvalue = lst[index] position = index while position > 0 and lst[position - 1] > currentvalue: lst[position] = lst[position - 1] position = position - 1 lst[position] = currentvalue Complex type definitions effectively become their own meta-programs that the compiler uses to verify your program, but now you've just pushed the problem back a step since somebody still has to read and understand the meta-program to know that it's verifying the correct thing.

mercer 8y ago
Is Elixir/Erlangs Dyalizer/Dyalixir similar to Clojure's spec? I'd very much like to read more on this topic, but because my knowledge of type systems pretty much started with, and is limited to TypeScript, I don't know what to ask specifically. Have you written anything about this, or could you point me to any articles that discuss this difference? Basically, I've become convinced that TypeScript, at least for anything nontrivial, is worth using over just JavaScript. There's nothing like it in the Elixir world, but I've been meaning to check out Dialyzer because I do sometimes miss what TypeScript offers.
- yogthos 8y ago
  Dyalizer is more of a linter from my understanding. Instead of aiming for formal correctness it looks for cases that are obviously incorrect instead. Meanwhile, the goal of Spec is to provide the ability to specify runtime contracts for what the code is meant to be doing. I think that both approaches compliment each other in practice. I don't know any articles comparing the two though.
coldtea 8y ago
>Because static typing primarily focuses on showing that your types align. This is completely tangential to knowing that the code is doing what you intended. That's not true. It entirely depends on the power of your type system. Types do not just encode "alignment" matching -- they can be used to encode all kinds of intent.
- coldtea 8y ago
  To give but one example, a type that is bounded by a range (e.g. 1..12 like e.g. Ada allows) doesn't just encode alignment matching (that your "month" variable doesn't get passed where a regular int or a "temperature" is expected) but also that it's not 16. That of course is just the tip of the iceberg... In Rust the type system enforces intend regarding the lifetime of a variable as well.
  - yogthos 8y ago
    You can encode interesting things using the type system, but I don't find it's nearly as practical as the alternatives such as runtime contracts. For example, consider a sort function. The types can tell me that I passed in a collection of a particular type and I got a collection of the same type back. However, what I really want to know is that the collection contains the same elements, and that they’re in order. This is difficult to express using most type systems out there, while trivial to do using a contract system such as Spec.
    - coldtea 8y ago
      >For example, consider a sort function. The types can tell me that I passed in a collection of a particular type and I got a collection of the same type back. However, what I really want to know is that the collection contains the same elements, and that they’re in order. That's a test though -- and a contract is basically an assertion for such a test. Types allow you to express and check things before the code is run.
      - yogthos 8y ago
olzd 8y ago
I hope you realize the Idris code actually prove that the list will be correctly sorted, unlike your python code.
- kazinator 8y ago
  I am skeptical; prove that it proves such a thing. Might it not actually be easier to prove that the Python code sorts than that the Idris code proves sorting?
  - antpls 8y ago
    The idea is that, if you can describe the problem (here, sorting) with a few lines, you don't have to prove that the Idris code is correct, because the machine do it for you. You can throw that sort function without even looking at the code in any critical space mission you want and, if the premises are true, then it will always correctly sort. You can imagine 3 kinds of code : - a code that describes the problem (that is both human readable and machine readable) - a code implementing the solution (here, your Python script) - a code proving the implementation correctly answers the problem (which would be math if you had to prove your Python code on a whiteboard) The idea is more about reusing and sharing trusted code, re-running the proof on your own system to make sure it's legit, and move on. You don't need to look at the proof to use the sort function, you would only look at the code that describes the problem and make sure it's the right one for your problem at hand.
    - yogthos 8y ago
      >The idea is that, if you can describe the problem (here, sorting) with a few lines, you don't have to prove that the Idris code is correct, because the machine do it for you The machine can't show that your specification is correct, only that it's self consistent. What you're doing is writing a proof that the compiler will use to verify your code. However, if you make a mistake in your proof, then the compiler will happily verify the wrong thing. The argument is that it's much harder to spot a mistake in a 300 line Idris proof than it is in a 5 line Python implementation.

mercer 8y ago

Is Elixir/Erlangs Dyalizer/Dyalixir similar to Clojure's spec? I'd very much like to read more on this topic, but because my knowledge of type systems pretty much started with, and is limited to TypeScript, I don't know what to ask specifically. Have you written anything about this, or could you point me to any articles that discuss this difference? Basically, I've become convinced that TypeScript, at least for anything nontrivial, is worth using over just JavaScript. There's nothing like it in the Elixir world, but I've been meaning to check out Dialyzer because I do sometimes miss what TypeScript offers.

yogthos 8y ago
Dyalizer is more of a linter from my understanding. Instead of aiming for formal correctness it looks for cases that are obviously incorrect instead. Meanwhile, the goal of Spec is to provide the ability to specify runtime contracts for what the code is meant to be doing. I think that both approaches compliment each other in practice. I don't know any articles comparing the two though.

coldtea 8y ago

>Because static typing primarily focuses on showing that your types align. This is completely tangential to knowing that the code is doing what you intended. That's not true. It entirely depends on the power of your type system. Types do not just encode "alignment" matching -- they can be used to encode all kinds of intent.

coldtea 8y ago
To give but one example, a type that is bounded by a range (e.g. 1..12 like e.g. Ada allows) doesn't just encode alignment matching (that your "month" variable doesn't get passed where a regular int or a "temperature" is expected) but also that it's not 16. That of course is just the tip of the iceberg... In Rust the type system enforces intend regarding the lifetime of a variable as well.
- yogthos 8y ago
  You can encode interesting things using the type system, but I don't find it's nearly as practical as the alternatives such as runtime contracts. For example, consider a sort function. The types can tell me that I passed in a collection of a particular type and I got a collection of the same type back. However, what I really want to know is that the collection contains the same elements, and that they’re in order. This is difficult to express using most type systems out there, while trivial to do using a contract system such as Spec.
  - coldtea 8y ago
    >For example, consider a sort function. The types can tell me that I passed in a collection of a particular type and I got a collection of the same type back. However, what I really want to know is that the collection contains the same elements, and that they’re in order. That's a test though -- and a contract is basically an assertion for such a test. Types allow you to express and check things before the code is run.
    - yogthos 8y ago

olzd 8y ago

I hope you realize the Idris code actually prove that the list will be correctly sorted, unlike your python code.

kazinator 8y ago
I am skeptical; prove that it proves such a thing. Might it not actually be easier to prove that the Python code sorts than that the Idris code proves sorting?
- antpls 8y ago
  The idea is that, if you can describe the problem (here, sorting) with a few lines, you don't have to prove that the Idris code is correct, because the machine do it for you. You can throw that sort function without even looking at the code in any critical space mission you want and, if the premises are true, then it will always correctly sort. You can imagine 3 kinds of code : - a code that describes the problem (that is both human readable and machine readable) - a code implementing the solution (here, your Python script) - a code proving the implementation correctly answers the problem (which would be math if you had to prove your Python code on a whiteboard) The idea is more about reusing and sharing trusted code, re-running the proof on your own system to make sure it's legit, and move on. You don't need to look at the proof to use the sort function, you would only look at the code that describes the problem and make sure it's the right one for your problem at hand.
  - yogthos 8y ago
    >The idea is that, if you can describe the problem (here, sorting) with a few lines, you don't have to prove that the Idris code is correct, because the machine do it for you The machine can't show that your specification is correct, only that it's self consistent. What you're doing is writing a proof that the compiler will use to verify your code. However, if you make a mistake in your proof, then the compiler will happily verify the wrong thing. The argument is that it's much harder to spot a mistake in a 300 line Idris proof than it is in a 5 line Python implementation.