Hegel: Refinements should be invalidated by side effects

[vkurchatkin]

const a:  { a: string | number } = { a: 'foo' };

function foo() {
  a.a = 1;
}

function test(x: { a: string | number }) {
    if (typeof x.a === 'string') {
      foo(); // this invalidates the refinement
      const a: string = x.a.toUpperCase(); // runtime error
    }
}

 test(a);

[Raynos]

How do you know what is an is not a side effect ?

Calling functions and methods inside if statements is quite common.

Even x.a is a potential getter that had a side effect. This can go pretty deep.

[Raynos]

For example

class MyThing {
  async fetchTagsAndDoStuff () {
    const res = await this.dataLayer.fetchTags(this.bucketName)
    if (res.err) {
      this.logger.warn('oops could not get tags', { err: res.err })
      return { err: res.err }
    }

    const res2 = await this.dataLayer.getBucketInfo(this.bucketName)
    if (res2.err) {
      this.logger.warn('oops could not get bucket info', { err: res2.err })
      return { err: res2.err }
    }

    return { data: { tags: res.data, info: res2.data } }
  }
}

Here we have res.err a side effect logger method and then returning res.err

In this case the type of res is { err: Error } | { data: T }

[vkurchatkin]

You are right. There are a couple of thing that can be done

1. Purity tracking. Functions that are free of side effects should be marked as such. Properties that are definitely not getters.

2. Visibilty tracking. This is probably very convoluted in practice. The idea is to prove that a given statement can't possible affect a given refinement, because it doesn't see the refined binding or value.

Simple example:

import { foo } from 'foo';

export function test(x: string | number) {
    if (typeof x === 'string') {
       foo(); // foo is from outer scope, so there is no way it can affect x
    }
}

But this will become convoluted very quickly:

```js
import { foo, bar } from 'foo';

export function test(x: string | number) {
bar(() => x = 1);

if (typeof x === 'string') {
   foo(); // foo is from outer scope, but current scope has leaked through `bar`
}

}

[Raynos]

Should some of these soundness features be behind opt in / opt out flags ?

Like maybe in my code base I would be ok with assuming "no side effects in function calls" and some other code bases might really like the advanced checking of "Please invalidate on side effects"

[vkurchatkin]

I guess if soundness is the goal, then there is no middle ground