Hacker News Reader

Comment by HerrMonnezza | Hacker News Reader

  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

View on HN

That is funny, Ada/SPARK is not mentioned at all! How strange.

https://en.wikibooks.org/wiki/Ada_Programming/Contract_Based...

http://www.ada-auth.org/standards/12rat/html/Rat12-2-3.html

https://docs.adacore.com/spark2014-docs/html/ug/en/source/ho...

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.

And then if you don't test that Ada code, you blow up your Ariane 5.

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. :)

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.

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

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.

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

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.

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

Reply on news.ycombinator.com