[rezonant]

> But since we are compiling AOT and not JIT, we cannot de-opt/undo that guess if it becomes wrong - instead we would just crash. > > But we could define the type using type annotations (TS)! > > Now we have to do 0 checks of the type of a, since we already know it at compile-time. This can allow for some big speedups :)

This comes with a big caveat that if the type assertion is wrong at runtime that the AOT'ed app will crash. Also I get the sense that the author assumes type "string" always means non-null and non-undefined but this is only true if the strictNullChecks compiler option is enabled.

Nonetheless, cool to see folks experimenting in the JS engine arena, especially around AOT!

[o11c]

A useful way to think of this kind of thing is to hoist the assertions into the caller, where they can be optimized out.

There's a lot of poorly-explored room in compiler design to take generalized invariants/preconditions/postconditions into consideration (explicit ones are useful for opaque functions defined in a different TU), not just things considered "types" (the problem with types is that they have different lifetime/allocation concerns than assertions).

[ReleaseCandidat]

Refinement types and liquid types (which are a subclass of refinement types).

[o11c]

From what I've seen, those are poorly done in practice, usually in multiple ways.

Recently I've been writing code to deal with partial alignment. The desired invariants here typically involves at least 3 variables:

  align must be a power of 2. Since this involves only one variable, refinement types can handle this one just fine at least (expression: n && !(n & (n-1)) ).
  0 <= skew < align
    skew != 0 in some branches, additionally
  pointer_as_int(buf.start) % align == skew
    some APIs take 2 buffers that should both have the alignment
    often if the buffer points to a size-zero span at NULL, the condition does not need to hold however
  (skew + buf.len) % align == 0 (only relevant sometimes; sometimes this is a different alignment than other invariants)

Since these are, generally, separate function arguments with completely different origins, how do you apply refinement types here? Additionally, the buffer can have different kinds of external ownership; in particular, Rust's aggressive "I must move ownership without warning" makes it impossible to write a lot of good code. We must not abandon the good parts of C if you want people to actually use your stuff, even ignoring the incremental-conversion problem.

Now consider ABI compatibility, say if we had forgotten to add the skew != 0 condition somewhere. If old code calls the function, it needs to hit a thunk that verifies the condition. New code however should have done that in the caller and thus enter the code directly. Where is the compiler tooling to support this? Clearly, invariants (and pre- and post-conditions, which are just invariants for a finite time) need to be able to specify what version of your code they were first specified in. That's a lot of information to specify in a function type which often gets disregarded.

[canadahonk]

Agreed, I have it behind a flag because of this, in the (far) future I could enable by default if I write a type checker built-in or something. Thank you!

[thaodsfwefs]

> Disabling `strictNullChecks`

Are people this eager to be PIP'd?

[rezonant]

You don't really get the luxury of being opinionated about Typescript settings when you are implementing a runtime