Inlined constrained type using control flow analysis

[gulshan]

Some recent features like "String Literals" or "strict null check" in Typescript can be used to shift responsibility of checking the validity of a parameter from function/API developer's side to caller's side. And with control flow analysis, one can start with an discriminated union type and based on the flow of the code, compiler will determine or exclude some specific types. So, code like this-

    function checkResponse(response: String): boolean {
        if (response === null)
            throw new Error("Response cannot be null")

        if (response === "YES")
            return true
        if (response === "NO")
            return false

        throw new Error("Not valid response")
    }

can be converted to-

    function checkResponse(response: "YES"|"NO"): boolean {
        return (response === "YES")
    }

And compiler will ensure the caller will only be able to call the function with appropriate values. This increases integrity of code. (Although, caller should also be using Typescript in these cases, as the checking does not exist in compiler generated javascript code.)

Now, I am proposing a Typescript feature with similar intention/result- shifting the responsibility of validation to upper(caller/consumer) side. What I am trying to propose is best described by an example. Using this feature code like this-

    function squareRoot(num: number): number {
        if (num < 0)
            throw new RangeError("Not valid number")
        var root: number
        // do the calculation
        return root
    }

will become something like-

    function squareRoot(num: number:[_ >= 0]): number {
        var root: number
        // do the calculation
        return root
    }

Here, a constraint is being attached :[_ >= 0] (syntax can be anything else, more fitting with Typescript) with it's parameter, and the range checking is omitted. Now, according the new feature, the compiler will show an error, if during this function call, it cannot be sure whether the parameter value satisfies the constraint or not using control flow analysis. So-

    squareRoot(0) //Ok. For constants, compiler can check validity by itself
    squareRoot(-1) //Error

    var userInput = Number(prompt())
    squareRoot(userInput) //Error, compiler not sure

    if(userInput >= 0 )
        squareRoot(userInput) //Ok

    if(userInput > 1000)
        squareRoot(userInput) //Ok

    if(userInput > -1 )
        squareRoot(userInput) //Error, compiler not sure

    if(userInput < 0)
        return
    squareRoot(userInput) //Ok

And this is not only for range checking numbers. But any (pure- without side effect) function taking an object of type T and returning boolean can be attached to type T. So, checking if some string is a valid email or satisfies a regex pattern, or whether a file is writable or more complex check for a complex type, all are possible within the scope of this proposal.

I am calling this idea Constrained Type- a type with an attached constraint. Most of goals of this proposal can be achieved now in current language, using newly derived types/inheritance. But someone has to derive a child type for each of the constraints they want to check. The constructor in the derived type can then check and prevent invalid objects being created. But it seems doing too much for too little. It is cumbersome for both API developers and callers. And doing this by inheritance hides the base or actual type of the data to the API consumer. That's why we see very few of them. This proposal will make both the base type and the constraint easily visible to the consumer, as the constraint is inlined with the base type. It does not clog the base type, as it is not a part of it. And consumer/caller can then just declare a variable of base type and check to reach constraint satisfaction- a workflow very similar to what is currently practiced.

There are some previous proposals like this- "Tag types" #4895 and "Refinement Types" #7599 (both by @Aleksey-Bykov). But what I understood from reading them (and I may be wrong), they are trying to track changes of some object to determine whether some condition holds at some point of code. This proposal has nothing to do with tracking states. It just proposes to describe attributes of data with more ease and increase integrity using compiler's ability to analyse control flows.

[zpdDG4gta8XKpMCd]

it's not about tracking the state, it's about taking advantages of invariants proven at runtime:

function isPositive(value: number): value is number & Positive { // a tag assigned after assertion passed
   return value > 0;
}
function isPositive(value: number): value is number > 0 { // narrowing to a refined type ("constrained" type), alternative syntax: [_ > 0]
   return value > 0;
}

pretty much the same thing, with the exception that Positive only makes sense to the developer who made it up, whereas the number > 0 type can be used by the type checker as in #7599

it's important to note that "refinments" only good as long as the value doesn't change, once the value changed, refinments are worth nothing, this is why:

• it's either requires much more sophisticated flow analysis being able to identify places where refinments need to be remove widening the type to original state
• or limit it to immutable types like string, number and objects with readonly immutable fields

belated definition:

• a refinment is a type + a predicate associated with it that was proven to hold true for a given value in a given context

the purpose of refinments is to take advantage of the knowledge that encoded in the predicate during static check and proven at runtime

[gulshan]

I think, I get the refinement types now. And it requires quite complex compiler ability and will be hard for non-functional languages. What do you think about this proposal? This will work with mutable variables/objects also.

[gulshan]

Now I think, these constraints only makes sense with ranges of numbers. For that, some special syntax like number<lower..upper> can be used- boundaries are inclusive and optional. So my example method will become-

function squareRoot(num: number<0..>): number {
    var root: number
    // do the calculation
    return root
}

Composite types can just use constraints with their members of type number.

[gulshan]

Related #15480