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

Here 'head' will return 'undefined' for empty array and 'first element' for arrays of 1+ length
Forgive me this free-form type notation

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 ]
// ...

Type of Number is reduced to a subset of possible values (less than 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*']

By declaring a function type that accepts strings of letters only we restrict values it can be called with

---

Original tweet:

Comments

[Ben Lovy]

I'm not completely positive I've correctly parsed your question, but it sounds to me like you're describing dependent types. Is that more or less correct? I don't know of any webdev technologies that can do this, it's a pretty niche feature confined to fancy academic languages like Idris, F*, and ATS. All very cool, but not exactly what you'd use for practical work today.

[Kostia Palchyk]

Hi, Ben!

From what I understand, it looks like what I was searching for!
And it surely supplies me with reading materials for months (well, years rather) 🙂

Thank you very much! 🎄

P.S.: Will it be useful to have it in our day-to-day development? What do you think?

[Ben Lovy]

Awesome! My only experience with it is from messing around with Idris, here's the relevant section in the docs - the "holes" described in the section preceding are another really cool idea. Idris is just pretty cool in general, and worth your time even if you never deploy any code

I do think it's a useful idea, but the Wiki article notes it does complicate type checking. It can slow the process, and lead to more complicated situations, including those which may be undecidable - potentially a step backwards in terms of practical benefit if you hit that case.

In general, though, I agree with you, I think moving that check to the type level is a good idea. If I append to an array, it actually, conceptually, is part of the "type" of the return value that the length of my array is greater than the original length (by exactly one). Seems useful to be able to specify that in the definition, much like it's useful to define any types at all.

I'd be curious to see if you come up with anything cool with this feature, or work out a way to approximate it with TS!