Off-the-shelf semantic subtyping is slightly different from what is implemented in Luau, because it requires models to be set-theoretic, which requires that inhabitants of function types “act like functions.” There are two reasons why we drop this requirement.

Set-theoretic semantic subtyping does not support this normalization, and instead normalizes functions to disjunctive normal form (unions of intersections of functions). We do not do this for ergonomic reasons: overloaded functions are idiomatic in Luau, but DNF is not, and we do not want to present users with such non-idiomatic types.

For these two reasons (which are largely about ergonomics rather than anything technical) we drop the set-theoretic requirement, and use pragmatic semantic subtyping.

Unexpectedly, this is not always true in set-theoretic models, due to uninhabited types. In set-theoretic models, if x has type never then f(x) has type never. We do not want to burden users with the idea that function application has a special corner case, especially since that corner case can only arise in dead code.

The other difference between Luau’s type system and off-the-shelf semantic subtyping is that Luau does not support all negated types.