predicate literals lead to undecidable problem in static analysis

[maiermic]

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.

[maiermic]

Are predicates intended for static type analysis?

[ericelliott]

We need to make a distinction here:

The special Predicate type is NOT a dependent type, and can be used for static analysis.

Predicate literals are NOT intended for static analysis. Instead, they're intended to enhance runtime type checking capabilities in combination with tools like rfx.

We should separate predicate literals and warn that they introduce dependent types and should have a very restricted use. Open to PR suggestions.

[maiermic]

Wow, reading the readme I did not recognize/understand that predicate literals are different to Predicate types. I really must have been confused 😕 I see clearly now, thanks 😃

[ericelliott]

Definitely open to PR suggestions to address these issues. Thanks for all your recent help, @maiermic. I really appreciate it.

[ericelliott]

I'm pretty sure the same dependent type problem exists with regular expression literals, right @maiermic?

[ericelliott]

Also, the special Any type has essentially the same problem (you can't do a proper static analysis on anything that uses Any, can you?). For all of these problems, some types can be inferred based on use-cases and runtime analysis.

We are knowingly limiting static analysis capabilities in order to enhance runtime capabilities and analysis. That said, people who want analyzable static types are free to use a static-safe subset. That may be the best approach in the documentation: Clarify the types to avoid if you want to use the static-safe subset? =)

[Mouvedia]

We should re-organize the README so that the static-unsafe types are clearly distinguished.
Maybe by tagging them with some kind of label?
For example, by appending ^{static-unsafe} in the TOC.

[maiermic]

you can't do a proper static analysis on anything that uses Any, can you?

Why not? Any is a static type. Types that use predicate literals are not.

[ericelliott]

Any is essentially the same as untyped. Literally any type is acceptable, including null or undefined values, which is effectively like turning type checking off for that variable.

[maiermic]

type checking on Any is not off. The type checker knows that a value of type Any might be null or undefined:

// a: Any
a.method(); // Error: Can not access property `method` on `a` of type `Any`, since `a` might be `null`.

[ericelliott]

type checking on Any is not off. The type checker knows that a value of type Any might be null or undefined

True, you could do that. But a type checker could make exactly the same assumption about an untyped variable. Further, your example should not necessarily cause an error, because that would break a lot of existing code.

It would also force boilerplate into every function that uses any parameter of type Any to do some type checking inside the function to guard against undefined, which is not always necessary or desirable.

Hence, Any is essentially the same as untyped, except that it gives you the option of deciding whether or not you want to type check it, and if so, how.

[maiermic]

That's why I'd like to make Any? the super type of all types instead of Any (null safety):

null is not a member of Any, but of Any?.

Although my thinking seems radical, I just like to hint at some concerns regarding static type analysis. In my opinion it leads to problems if the super type Any is similar to the type dynamic in C# or Dart, which would be the case if my example doesn't cause an error.

[ericelliott]

null is not a member of Any, but of Any?.

This is not currently the case. null is a member of Any. You're suggesting that it shouldn't be?

[maiermic]

Yes, as well as null should not be a member of Object, which isn't the case either currently.

[ericelliott]

null should not be a member of Object, or it would be hard to protect against it in the case where an actual object is expected.

[maiermic]

👍

[maiermic]

@ericelliott late answer to your question

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

Yes, indeed!