Dynamic value type inference?
Tags: help, discuss, typescript
Published: 2020-01-02 12:49:28

**UPD:** Ben Lovy (@deciduously) has linked to [dependent types]( https://en.wikipedia.org/wiki/Dependent_type), 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:

```ts
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:

```ts
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:

```ts
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
```

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

So the type validation would forbid me accidentally doing:

```ts
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

```ts
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

```ts
if (code >= 400) {
  return;
}
// ... some lines of code / function calls here...
if (value == 502) { // <- Error: [ 502 ] is not a subset of [ -Infinity..400 ]
// ...
```
<figcaption>Type of Number is reduced to a subset of possible values (less than 400)</figcaption>

```ts
// 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*']
```
<figcaption>By declaring a function type that accepts strings of letters only we restrict values it can be called with</figcaption>

---

_Original tweet:_

{% twitter 1211624440301314053 %}