teal-language / tl

The compiler for Teal, a typed dialect of Lua
MIT License
2.11k stars 109 forks source link

and operator not type-checking properly #462

Open Xandaros opened 3 years ago

Xandaros commented 3 years ago

The and operator has some weird inconsistencies with the type checking. For example, the following is valid:

local a: string = false and "x"

The and operator seems to always assume the type of the second operand, but does not require both operands have the same type. In contrast, the or operator will fail to compile on the same example, as it does require both operands have the same type.

and should probably be adjusted to match the behaviour of or.

hishamhm commented 3 years ago

This is a "lenient" behavior we're currently letting slip because x = <boolean> and <othertype> is a very common Lua idiom, which means that the resulting value will be either of type <othertype> or it will be falsy, and potentially checked with if x then later. This is generally okay because every type includes a falsy value, nil.

The only value which breaks this is, indeed, the other falsy value, false. Nobody writes false and x so that's a pathological case, and in case of boolean-returning expressions, their use in x = returns_bool() or something_of_type_T is generally to check later if x is falsy or not, so you would use if x then, which is the logical thing to do if you use that expression, then the block will only enter if the variable is of the correct type T.

If you want something to be boolean | T to have it be either T or false, you can type the variable explicitly.

Still, I'm interested to know if you got yourself a bug because of this behavior! Do you have any real code example where this behavior was problematic? Thanks for the feedback!

Xandaros commented 3 years ago

No, I did not actually run into any issues with this directly. I was working on a language server for teal (https://github.com/Xandaros/teal-lsp)

While this is indeed a common Lua idiom, this does break the type checker. In the example I gave, you end up with a string variable with the value false and you're never told about it.

Maybe this is fine - the teal project does not appear to be what I initially thought, anyway. (I expected a fully type checked dialect of Lua, straying from Lua-isms where necessary. Removing nil would have been a very welcome change, too. Instead it seems that teal just wants to provide types and stick to Lua as close as possibly otherwise)

hishamhm commented 3 years ago

Yes, in technical terms we say that the type checker is unsound. But this is by design, so in this case it is not broken. This does not mean that Teal is 100% bug free of course, so it may be broken (and in need to be fixed!) in other places, but this particular behavior, among with other unsound ones, are intentional.

This pragmatic approach is taken by other languages built on top of dynamic language ecosystems. The most notable example is TypeScript. TypeScript has evolved over time to include better taming of null, so this is something on our eventual radar as well.

Teal does not aim to stick as closely to Lua as possible (that would be the Sorbet approach for the Ruby type checker, for example), but on the other extreme a fully sound type system would result in a language that would behave very differently from Lua, in spite of any syntactic similarity. Interoperating with existing Lua libraries and codebases is a goal, so we can't really make it into a "Haskell with a Lua syntax coating". :)