rtype: predicate literals lead to undecidable problem in static analysis
predicates may be used in an interface
interface Integer (number) => number === parseInt(number, 10);
They introduce dependent types:
a dependent type is a type whose definition depends on a value […] Dependent types add complexity to a type system. Deciding the equality of dependent types in a program may require computations. If arbitrary values are allowed in dependent types, then deciding type equality may involve deciding whether two arbitrary programs produce the same result; hence type checking may become undecidable.
Furthermore, Integer is rather a type than a characteristic of a value. What is the type of the result c in
var c = a + b; // a: Integer, b: Integer
Catchy question! You get an error. + is not defined for Integer and we do not know that Integer is a Number. We need to add the type Number to the parameter of the predicate to provide this information:
interface Integer (number: Number) => number === parseInt(number, 10);
What is the type of c now? Since + is not defined for Integer but for Number, c is of type Number. If we like to pass c to a function that takes an Integer we have to do a manually type check before. Otherwise, we cann’t do static type analysis in a safe way.
About this issue
- Original URL
- State: open
- Created 8 years ago
- Comments: 17 (8 by maintainers)
@ericelliott late answer to your question
Yes, indeed!