3 ms·

Off the top of my head, this sounds like dependent typing: https://en.wikipedia.org/wiki/Dependent_type https://en.wikipedia.org/wiki/Dependent_type . Simply pu

Off the top of my head, this sounds like dependent typing: https://en.wikipedia.org/wiki/Dependent_type https://en.wikipedia.org/wiki/Dependent_type . Simply put, it allows you to define types that are generic on specific values, rather than other types. So with normal typing you have generics like List<T>, but with dependent typing you can do Int<1, 10> like you described. Similarly, you can define types like the type of odd integers, or the type of lists with at least 3 elements, etc. They are very cool, but as you can imagine complicated to implement. In general dependent types can make type checking a program undecidable. You might also be interested in the numeric subtypes you can declare in some Pascal languages, like Ada. See http://www.isa.uniovi.es/docencia/TiempoReal/Recursos/textbook/aps5-6.htm http://www.isa.uniovi.es/docencia/TiempoReal/Recursos/textbo... for some examples. In Ada you can define subtypes, like the set of integers from 1 to 10. You can also define subtypes on floats, characters, and enums. You can also define the overflow rules for your type to a certain degree. It isn't quite as powerful as dependent types, I don't think you can really make it as generic, but still an interesting feature. One very interesting property of Ada is the ability to make arrays which are indexed by a non-integer type. So you can make a enum for the days of the week, then declare an array of strings indexed by the days of the week type. Then you can do things like "array[Saturday]" to access values. Effectively this lets you make an array of 7 values with strongly-typed indexing.

zozbot234 5y ago
> Simply put, it allows you to define types that are generic on specific values, rather than other types Dependent types are far more general than that. They allow a type to be parameterized on a "value" where the "value" isn't merely a program constant, but rather an arbitrary expression that's type correct at that point in the program. This is what allows them to express refinement types: the refinement type bundles a value with a description of a function that takes any given value to a correct-by-construction assertion that the value satisfies some interesting property. So if you wanted to prove that a value x in your program is in the range [m, n], you "simply" have to show how you could compute (x - m) and (n - x) at that point in your program, where the - operator can only return non-negative numbers by construction. The flip side is that m and n can be arbitrary run-time values, and there's no run-time check at all; these are essentially 'phantom' values and any computation involved in these proofs is elided: checking that a proof is correct is a special case of type checking. This is also why such languages cannot be Turing-complete, since that would allow a non-terminating function to be a valid "proof" of any property.

zozbot234 5y ago

> Simply put, it allows you to define types that are generic on specific values, rather than other types Dependent types are far more general than that. They allow a type to be parameterized on a "value" where the "value" isn't merely a program constant, but rather an arbitrary expression that's type correct at that point in the program. This is what allows them to express refinement types: the refinement type bundles a value with a description of a function that takes any given value to a correct-by-construction assertion that the value satisfies some interesting property. So if you wanted to prove that a value x in your program is in the range [m, n], you "simply" have to show how you could compute (x - m) and (n - x) at that point in your program, where the - operator can only return non-negative numbers by construction. The flip side is that m and n can be arbitrary run-time values, and there's no run-time check at all; these are essentially 'phantom' values and any computation involved in these proofs is elided: checking that a proof is correct is a special case of type checking. This is also why such languages cannot be Turing-complete, since that would allow a non-terminating function to be a valid "proof" of any property.