3 ms·

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 ex

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.