5 ms·

The biggest feature I want out of Starlark the language (not Bazel the build system) is to allow optional type annotations. They don’t have to do anything, they

by jez 2y ago

The biggest feature I want out of Starlark the language (not Bazel the build system) is to allow optional type annotations. They don’t have to do anything, they don’t have to specified, it just needs to be syntactically valid to put type annotations somewhere. If there were syntax for type annotations that tools like Bazel ignored, it would be possible for some enterprising soul who’s forced to use Bazel at work to throw up an initial prototype of a type checker and a language server for Starlark in Bazel. The language is not that complicated that a type checker couldn’t be written by a hobbiest. My biggest frustration when using Bazel is not even Bazel—it’s the fact that when I’m looking at code like this[1], everything comes from a single, unannotated `rctx` variable that has no type annotation. So when I’m trying to read the code, it’s a matter of constantly grepping the repo, grepping the bazel docs, and grepping the bazel source code to get any new code written. Why can’t I just hover and see the docs? Why can’t I press `rctx.` and see all the attributes available? I frequently hear “why do you need types? the language is Turing complete just run it and see if it fails” but that misses the point that I have want to use types to guide what code to write in the first place. [1] https://github.com/bazel-contrib/toolchains_llvm/blob/master/toolchain/internal/configure.bzl#L59 https://github.com/bazel-contrib/toolchains_llvm/blob/master...

kccqzy 2y ago
A type system is a very good thing, but it directly contradicts one of the goals for this language, simplicity. As someone who has written type inference code for plain Hindley-Milner type systems and those with subtyping, I can tell you this is very much an open research problem. Inferred types, understandable type errors, expressive language: choose two out of three. If you sacrifice good type inference and require users to specify type annotations themselves they will not like it especially considering users' mental model of this language comes from Python; if you sacrifice understandable type errors, users will reject the whole system as soon as they encounter a type error; if you sacrifice expressiveness you are taking away features users want like subtyping. If you want something that's ignored by Bazel and only used by some other tools you already have it: docstrings. You can enforce docstrings to be of a certain format and contain type annotations. Be the solution you want to see: be that hobbyist that writes a type checker and language server.
- vlovich123 2y ago
  I don’t get this argument as it seems at odds with the existence proof of Python itself having optional typing, type inference, understandable type errors and an expressive language. What am I missing?
  - kccqzy 2y ago
    Here's an elementary litmus test that anyone slightly experienced with type systems will know. How do you type the omega combinator in Python? lambda x: x(x) What about the application of the omega combinator to itself? (lambda x: x(x))(lambda x: x(x)) How do you type the Y combinator in Python? lambda f: (lambda x: f(x(x)))(lambda x: f(x(x))) Depending on the choice of the type system you can either answer: this cannot be assigned a type in which case your type system is too weak to express many real-world programs, or it does have a type but then your type system is so sophisticated that people using this language (just for writing BUILD rules) won't be able to understand type errors in this type system. I have yet to find a middle ground. In case you claim this is impractical functional programming, bear in mind you can write the same thing using classes in object-oriented programming. --- Okay let's not even talk about these weird-looking "combinators" even though they have a rich history. Consider this function: lambda x: {'this': x, 'next': x + 1} What is its type? Again the answer depends on plenty of choices that need to be made by the type system designer. Do you force dictionaries to have a single type for values? If so, many users used to Python will reject your system for being too inflexible. If not, will you now introduce row polymorphism in your type system? Will you now introduce depth subtyping and width subtyping in your type system? (For example if a function only needs field 'x' in a dictionary but the caller passes a dictionary with both fields 'x' and 'y' should not result in an error; that's why you need subtyping.) Now let's consider the lowly plus operator. In real Python the plus operator can work on integers, floats, strings, sets, etc. Let's say your type inference algorithm uses the RHS to find that x must be an integer. But that's wrong; it could still be a float. Can you now write a type for that expression? Hint: it involves record types, intersection types, type variables and other things that would not be comprehensible.
    - 2y ago
smeenai 2y ago
starlark-rust (used by Buck2) supports this! They're immensely useful for grokking complex build code, as you said. https://github.com/facebook/starlark-rust/blob/main/docs/types.md https://github.com/facebook/starlark-rust/blob/main/docs/typ...
fire_lake 2y ago
Given that “types” are passed around like values in Bazel this may prove complicated to support.
- bqmjjx0kac 2y ago
  Given that is deterministic, it should be possible to just run the code and record the set of types that reach every parameter and variable. A bit expensive, perhaps. And it breaks down if the code is in an intermediate state. Like, "I just deleted a comma, where did my type annotations go?"
  - coder543 2y ago
    Are you saying that every function can only be called with a consistent set of types in the parameters? It’s not possible to call a function two times and supply parameters that have different fields on them? Unless that is true, the end result might not be ideal. You could certainly record the information that is there at every line of code at runtime, and you could probably calculate the union of the parameter types to find only the fields that are always there, which would be fairly okay I guess.
Turskarama 2y ago
A type system that doesn't do anything? It has that, it's called comments. Before you try to tell me that it's somehow different, consider that the main thing a type system has to be for consistency is accurate. If they types aren't checked by a compiler or interpreter, then someone can change the way the variable is assigned or what the function will work with, and the annotation will just be wrong.
- maleldil 2y ago
  The idea is to have gradual typing, like Python does. Most annotations in Python have no impact on runtime (e.g. parameter types aren't checked), but they are still valuable for external tools to perform type checking. A program with the wrong types will still run, but you will get type errors from the checker. One difference is that Python specifies the type system in PEPs (basically Python's RFCs), while OP didn't ask for that here. This would mean whatever tool is implemented would define the type system.
  - Turskarama 2y ago
    OP did also say "They wouldn't even have to be specified", which is the big difference here needed for a type checker to actually use them over comments.
laurentlb 2y ago
This is something that came up multiple times. I think type information is especially valuable in combination with other IDE features (code completion). My idea was to do type checking in a separate tool (e.g. built on top of Buildifier) and let the interpreter ignore the types. So it could be completely optional. The type system could be gradual, like in Typescript. I don't know when/if it will happen (I'm no longer working at Google, so it's harder to make large contributions like this).
gue5t 2y ago
Having done some nontrivial Bazel/Starlark hacking, I completely agree that lightweight static types would be a good usability improvement. But I want to point out that Starlark is actually not Turing complete, which is imo one of the more interesting characteristics it has. Recursion is forbidden (https://github.com/bazelbuild/starlark/blob/master/spec.md#functions https://github.com/bazelbuild/starlark/blob/master/spec.md#f...) and loops must be structural; there is no while loop or other unbounded iteration construct. Starlark is one of the more capable and mainstream non-Turing-complete languages out there, and doesn't resemble the other common ones which mostly show up in theorem provers. On the one hand I think the logic in a build system that needs to reason about incremental builds absolutely should be guaranteed to terminate, but in some particularly painful situations I've had to resort to iteration over smart-contract-style "gas" parameters. EDIT: as a parting shot, dhall is another non-Turing-complete language in common usage, but its claim to fame is that it gets used in places that arguably shouldn't be doing any computation at all.

by jez 2y ago

kccqzy 2y ago

A type system is a very good thing, but it directly contradicts one of the goals for this language, simplicity. As someone who has written type inference code for plain Hindley-Milner type systems and those with subtyping, I can tell you this is very much an open research problem. Inferred types, understandable type errors, expressive language: choose two out of three. If you sacrifice good type inference and require users to specify type annotations themselves they will not like it especially considering users' mental model of this language comes from Python; if you sacrifice understandable type errors, users will reject the whole system as soon as they encounter a type error; if you sacrifice expressiveness you are taking away features users want like subtyping. If you want something that's ignored by Bazel and only used by some other tools you already have it: docstrings. You can enforce docstrings to be of a certain format and contain type annotations. Be the solution you want to see: be that hobbyist that writes a type checker and language server.

vlovich123 2y ago
I don’t get this argument as it seems at odds with the existence proof of Python itself having optional typing, type inference, understandable type errors and an expressive language. What am I missing?
- kccqzy 2y ago
  Here's an elementary litmus test that anyone slightly experienced with type systems will know. How do you type the omega combinator in Python? lambda x: x(x) What about the application of the omega combinator to itself? (lambda x: x(x))(lambda x: x(x)) How do you type the Y combinator in Python? lambda f: (lambda x: f(x(x)))(lambda x: f(x(x))) Depending on the choice of the type system you can either answer: this cannot be assigned a type in which case your type system is too weak to express many real-world programs, or it does have a type but then your type system is so sophisticated that people using this language (just for writing BUILD rules) won't be able to understand type errors in this type system. I have yet to find a middle ground. In case you claim this is impractical functional programming, bear in mind you can write the same thing using classes in object-oriented programming. --- Okay let's not even talk about these weird-looking "combinators" even though they have a rich history. Consider this function: lambda x: {'this': x, 'next': x + 1} What is its type? Again the answer depends on plenty of choices that need to be made by the type system designer. Do you force dictionaries to have a single type for values? If so, many users used to Python will reject your system for being too inflexible. If not, will you now introduce row polymorphism in your type system? Will you now introduce depth subtyping and width subtyping in your type system? (For example if a function only needs field 'x' in a dictionary but the caller passes a dictionary with both fields 'x' and 'y' should not result in an error; that's why you need subtyping.) Now let's consider the lowly plus operator. In real Python the plus operator can work on integers, floats, strings, sets, etc. Let's say your type inference algorithm uses the RHS to find that x must be an integer. But that's wrong; it could still be a float. Can you now write a type for that expression? Hint: it involves record types, intersection types, type variables and other things that would not be comprehensible.
  - 2y ago

smeenai 2y ago

starlark-rust (used by Buck2) supports this! They're immensely useful for grokking complex build code, as you said. https://github.com/facebook/starlark-rust/blob/main/docs/types.md https://github.com/facebook/starlark-rust/blob/main/docs/typ...

fire_lake 2y ago

Given that “types” are passed around like values in Bazel this may prove complicated to support.

bqmjjx0kac 2y ago
Given that is deterministic, it should be possible to just run the code and record the set of types that reach every parameter and variable. A bit expensive, perhaps. And it breaks down if the code is in an intermediate state. Like, "I just deleted a comma, where did my type annotations go?"
- coder543 2y ago
  Are you saying that every function can only be called with a consistent set of types in the parameters? It’s not possible to call a function two times and supply parameters that have different fields on them? Unless that is true, the end result might not be ideal. You could certainly record the information that is there at every line of code at runtime, and you could probably calculate the union of the parameter types to find only the fields that are always there, which would be fairly okay I guess.

Turskarama 2y ago

A type system that doesn't do anything? It has that, it's called comments. Before you try to tell me that it's somehow different, consider that the main thing a type system has to be for consistency is accurate. If they types aren't checked by a compiler or interpreter, then someone can change the way the variable is assigned or what the function will work with, and the annotation will just be wrong.

maleldil 2y ago
The idea is to have gradual typing, like Python does. Most annotations in Python have no impact on runtime (e.g. parameter types aren't checked), but they are still valuable for external tools to perform type checking. A program with the wrong types will still run, but you will get type errors from the checker. One difference is that Python specifies the type system in PEPs (basically Python's RFCs), while OP didn't ask for that here. This would mean whatever tool is implemented would define the type system.
- Turskarama 2y ago
  OP did also say "They wouldn't even have to be specified", which is the big difference here needed for a type checker to actually use them over comments.

laurentlb 2y ago

This is something that came up multiple times. I think type information is especially valuable in combination with other IDE features (code completion). My idea was to do type checking in a separate tool (e.g. built on top of Buildifier) and let the interpreter ignore the types. So it could be completely optional. The type system could be gradual, like in Typescript. I don't know when/if it will happen (I'm no longer working at Google, so it's harder to make large contributions like this).

gue5t 2y ago

Having done some nontrivial Bazel/Starlark hacking, I completely agree that lightweight static types would be a good usability improvement. But I want to point out that Starlark is actually not Turing complete, which is imo one of the more interesting characteristics it has. Recursion is forbidden (https://github.com/bazelbuild/starlark/blob/master/spec.md#functions https://github.com/bazelbuild/starlark/blob/master/spec.md#f...) and loops must be structural; there is no while loop or other unbounded iteration construct. Starlark is one of the more capable and mainstream non-Turing-complete languages out there, and doesn't resemble the other common ones which mostly show up in theorem provers. On the one hand I think the logic in a build system that needs to reason about incremental builds absolutely should be guaranteed to terminate, but in some particularly painful situations I've had to resort to iteration over smart-contract-style "gas" parameters. EDIT: as a parting shot, dhall is another non-Turing-complete language in common usage, but its claim to fame is that it gets used in places that arguably shouldn't be doing any computation at all.