Dynamic value type inference?

UPD: Ben Lovy (@deciduously) has linked to dependent types, which seems to be what I'm clumsy describing here. See his comment under the post for more details! Thank you, Ben!

Here, I'm asking for guidance and advice on further reading regarding a subject I'm going to describe next:

Consider this example in typescript:

if (false) {
  log('Unreachable code');
}

The log part will never be executed, no matter what. And a modern type system has ways to detect that dead code and will probably raise an error at the build time.

Now let's see this snippet:

const answer = 42;

if (answer - 42 > 0) {
  log('Unreachable code');
}

The log part is still unreachable, yet we won't see any error or warning.

The compiler will eat that, since the validation is static, and the minus operation done on 42 and 42 is statically defined to return a type Number.

And not 0, that it truly does.

I'll skip > comparison fn for brevity.

One more case

Imagine we have a function head, that accepts an array of items, and return the first element:

const head = arr => arr[0]

So the type of the function is detected as:

head :: any[] -> any

While in reality, it's more like:

head :: Array of length 0 as a =>
        a -> undefined

head :: Array of 1+ length as a
      , First element of a as b
     => a -> b

So the type validation would forbid me accidentally doing:

const a = head([true, 1, 'hi']);

return a / 8; // <-- Error, dividing a Boolean

To the point

Are there type systems with "dynamic type analysis" / "dynamic subset inference" that would handle such cases and properly report the type of answer - 42 to be 0?

Since I work in webdev, I'm primarily looking for implementations in this field. Yet, as well I would be glad to read more general information/achievements in other fields.

How I imagine that

For such systems to exist, I guess, they should run all the code that doesn't create side-effects and build a graph of sets of possible values subtypes.

Well, a function that divides one integer by another, has an infinity of possible values, so the calculation should be lazy somehow. Also, the system should handle loops/recursions that never stabilize.

As to side-effect-full functions where we can't infer subtypes, developers could manually define their types (as we already do now with foreign code):

Say, for an HTTP request function

function getACoinNominal(url) {
  return http(url).then(
    // ...
  );
}

we could declare:

getACoinNominal
  :: Subset of String that starts with `/`, `//` or `https://` as URL
   , Subset of number of [1, 2, 5, 10, 25, 50] value as Nominal
  => URL -> Promise<Nominal>

So that we can use getACoinNominal function only with strings that start with / // or https://, and it will return us a Promise with 1, 2, 5, 10, 25, or 50. Nothing other.

And in the cases when the exact value subset can't be calculated properly, or it takes more than a reasonable time to do so, we can always fall-back to the basic type inference.

Conclusion

I think such active analysis in the build phase will be useful not only for dead code detection but even more so for:

• smarter errors reporting
• better type guidance
• code reduce by letting us handle exact cases we should cover

As you may have found already, I don't know type systems theory (nor much of other theories, to be honest) . So, I'm asking to share some of your wisdom on:

• if such systems exist (I suspect they exist for a long time, at least in runtime engines)
• what can I read to learn more on the subject
• if it cannot exist
• share your thoughts if we need such a system

Thanks!

Appendix with use case speculations

if (code >= 400) {
  return;
}
// ... some lines of code / function calls here...
if (value == 502) { // <- Error: [ 502 ] is not a subset of [ -Infinity..400 ]
// ...

// name :: \w* => name -> void
function capitalize(name){
// ... fn logic
}
// ... some lines of code / function calls here...
const value = ' Henry ';
capitalize(value); // <- Error: [' Henry '] is not a subset of ['\w*']

Original tweet: