4 ms·

In other words, static typing is pointless. It has, maybe, some documentary value, but it does not substitute documentation on other invariants. For examp

In other words, static typing is pointless. It has, maybe, some documentary value, but it does not substitute documentation on other invariants. For example, your invariant might be something like I’m expecting here a monotonically increasing array of numbers with a mean value of such and such and a standard deviation of such and such. The best any static type checking will let you do is “array[float]”. The rest of your invariant must be expressed in words as a documentation of that function. I wonder if "design by contract" [1] tooling would help here? It seems to me one could express the stated invariants of the array as pre- or post-conditions on any function processing that array. [1]: https://wiki.c2.com/?DesignByContract https://wiki.c2.com/?DesignByContract

deleted 6y ago
[deleted]
johnisgood 6y ago
That is funny, Ada/SPARK is not mentioned at all! How strange. https://en.wikibooks.org/wiki/Ada_Programming/Contract_Based_Programming https://en.wikibooks.org/wiki/Ada_Programming/Contract_Based... http://www.ada-auth.org/standards/12rat/html/Rat12-2-3.html http://www.ada-auth.org/standards/12rat/html/Rat12-2-3.html https://docs.adacore.com/spark2014-docs/html/ug/en/source/how_to_write_subprogram_contracts.html#writing-contracts-for-functional-correctness https://docs.adacore.com/spark2014-docs/html/ug/en/source/ho... https://blog.adacore.com/contracts-of-functions-in-spark-2014 https://blog.adacore.com/contracts-of-functions-in-spark-201... Plus, I do not believe that static typing is pointless. Even if it were ONLY for documentation, that would already make it pretty useful, in my opinion, like Erlang's type specifications, although there is a static analysis tool called dialyzer that identifies software discrepancies such as type errors and such. In any case, from AdaCore's website: > In statically typed languages, a type is mainly (but not only) a compile time construct. It is a construct to enforce invariants about the behavior of a program. Invariants are unchangeable properties that hold for all variables of a given type. Enforcing them ensures, for example, that variables of a data type never have invalid values. > A type is used to reason about the objects a program manipulates (an object is a variable or a constant). The aim is to classify objects by what you can accomplish with them (i.e., the operations that are permitted), and this way you can reason about the correctness of the objects' values. Just for the curious: > A nice feature of Ada is that you can define your own integer types, based on the requirements of your program (i.e., the range of values that makes sense). In fact, the definitional mechanism that Ada provides forms the semantic basis for the predefined integer types. There is no "magical" built-in type in that regard, which is unlike most languages, and arguably very elegant.
- pfdietz 6y ago
  And then if you don't test that Ada code, you blow up your Ariane 5.
  - johnisgood 6y ago
    https://www.researchgate.net/publication/220475937_Design_by_Contract_The_Lessons_of_Ariane https://www.researchgate.net/publication/220475937_Design_by... For the record: that was ages ago, the language has improved a lot since then. Ada 2012 includes features for contracts, for example. Read the "Preface" of "Programming in Ada 2012" for details. :)
    - pfdietz 6y ago
      The Ariane 5 failure was due to the faster trajectory of that launcher causing an integer overflow that the Ariane 4 (which the software was cribbed from) did not experience. I'm not clear how you encode that in a contract. The sad thing about this is that if that code had been in (say) C the launch would have been fine, since no integer overflow would have been trapped, shutting down the guidance computer.
chromatin 6y ago
Great point.in addition to the excellent sibling comment on Ada, I would add that I have personally benefited (in the field of scientific computing) from contract programming facilities available in D https://dlang.org/spec/contracts.html https://dlang.org/spec/contracts.html
haskellandchill 6y ago
You can express those invariants using dependent types. Look at something like Lean.
clankyclanker 6y ago
Thank you for mentioning that and reminding me about two of my favorite projects, Eiffel and PyContract. (Is part of why DbC is so useful is because it's an extremely concise way to write assertions?) I'd love static typing systems if they allowed for DbC-style type declarations. There are times when the thing I need to use isn't a generic int, or even a short int, but an integer three or more. That's also type information, just not type information based on the shape of the data in memory. I've never seen a type system that can make those determinations at compile time, even when working with literal numbers in source code.
- ywei3410 6y ago
  Dependent type-systems like Agda can do that. Unfortunately they are also a pain to write. Fun-fact, you can use church-encoding to transform from your generic int to a "shape" based encoding for the slowest operations ever in quite a few languages (Python included).
- henrikeh 6y ago
  Ada has that. Bounded types and subtyping. For example, the type system is aware of the ranges of allowed values and can statically enforce this. Runtime checking is used by default but can be disabled.

deleted 6y ago

[deleted]

johnisgood 6y ago

That is funny, Ada/SPARK is not mentioned at all! How strange. https://en.wikibooks.org/wiki/Ada_Programming/Contract_Based_Programming https://en.wikibooks.org/wiki/Ada_Programming/Contract_Based... http://www.ada-auth.org/standards/12rat/html/Rat12-2-3.html http://www.ada-auth.org/standards/12rat/html/Rat12-2-3.html https://docs.adacore.com/spark2014-docs/html/ug/en/source/how_to_write_subprogram_contracts.html#writing-contracts-for-functional-correctness https://docs.adacore.com/spark2014-docs/html/ug/en/source/ho... https://blog.adacore.com/contracts-of-functions-in-spark-2014 https://blog.adacore.com/contracts-of-functions-in-spark-201... Plus, I do not believe that static typing is pointless. Even if it were ONLY for documentation, that would already make it pretty useful, in my opinion, like Erlang's type specifications, although there is a static analysis tool called dialyzer that identifies software discrepancies such as type errors and such. In any case, from AdaCore's website: > In statically typed languages, a type is mainly (but not only) a compile time construct. It is a construct to enforce invariants about the behavior of a program. Invariants are unchangeable properties that hold for all variables of a given type. Enforcing them ensures, for example, that variables of a data type never have invalid values. > A type is used to reason about the objects a program manipulates (an object is a variable or a constant). The aim is to classify objects by what you can accomplish with them (i.e., the operations that are permitted), and this way you can reason about the correctness of the objects' values. Just for the curious: > A nice feature of Ada is that you can define your own integer types, based on the requirements of your program (i.e., the range of values that makes sense). In fact, the definitional mechanism that Ada provides forms the semantic basis for the predefined integer types. There is no "magical" built-in type in that regard, which is unlike most languages, and arguably very elegant.

pfdietz 6y ago
And then if you don't test that Ada code, you blow up your Ariane 5.
- johnisgood 6y ago
  https://www.researchgate.net/publication/220475937_Design_by_Contract_The_Lessons_of_Ariane https://www.researchgate.net/publication/220475937_Design_by... For the record: that was ages ago, the language has improved a lot since then. Ada 2012 includes features for contracts, for example. Read the "Preface" of "Programming in Ada 2012" for details. :)
  - pfdietz 6y ago
    The Ariane 5 failure was due to the faster trajectory of that launcher causing an integer overflow that the Ariane 4 (which the software was cribbed from) did not experience. I'm not clear how you encode that in a contract. The sad thing about this is that if that code had been in (say) C the launch would have been fine, since no integer overflow would have been trapped, shutting down the guidance computer.

chromatin 6y ago

Great point.in addition to the excellent sibling comment on Ada, I would add that I have personally benefited (in the field of scientific computing) from contract programming facilities available in D https://dlang.org/spec/contracts.html https://dlang.org/spec/contracts.html

haskellandchill 6y ago

You can express those invariants using dependent types. Look at something like Lean.

clankyclanker 6y ago

Thank you for mentioning that and reminding me about two of my favorite projects, Eiffel and PyContract. (Is part of why DbC is so useful is because it's an extremely concise way to write assertions?) I'd love static typing systems if they allowed for DbC-style type declarations. There are times when the thing I need to use isn't a generic int, or even a short int, but an integer three or more. That's also type information, just not type information based on the shape of the data in memory. I've never seen a type system that can make those determinations at compile time, even when working with literal numbers in source code.

ywei3410 6y ago
Dependent type-systems like Agda can do that. Unfortunately they are also a pain to write. Fun-fact, you can use church-encoding to transform from your generic int to a "shape" based encoding for the slowest operations ever in quite a few languages (Python included).
henrikeh 6y ago
Ada has that. Bounded types and subtyping. For example, the type system is aware of the ranges of allowed values and can statically enforce this. Runtime checking is used by default but can be disabled.