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)

Most upvoted comments

@ericelliott late answer to your question

I’m pretty sure the same dependent type problem exists with regular expression literals, right

Yes, indeed!