4 ms·
I can kinda imagine it but can you elaborate on the part about getting rid of types?
by borplk 11y ago
I can kinda imagine it but can you elaborate on the part about getting rid of types?
- miguelrochefort 11y agoBy replacing types with arbitrary expressions, you could go beyond just having a list of integers. You could have a list of odd numbers, a list of words starting with "A", a list of ages over 18, a list of prime numbers, a list of at least 5/items, a list of all integers (infinite), etc. You can only access index N of a list whose type expression proves that it has at least 5/items. You can only access the fields of objects that are proven not to be null. You can only give as input to a function that expects an odd number a value whose type expression proves it to be an odd number. Basically, you can never have runtime exceptions.
- infinite8s 11y agoYou are talking about dependent types (https://en.wikipedia.org/wiki/Dependent_type https://en.wikipedia.org/wiki/Dependent_type) and only a few theorem-proving languages support them.