3 ms·

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 f

by 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.
  - vlovich123 2y ago
    This seems like a very weird technical explanation that doesn’t actually address my question. Python typing works well in practice and doesn’t suffer from any of the problems you listed. Also, from a brief investigation, according to [1] Haskell also isn’t able to express the omega combinator in its type system (& indeed the answer says very few type systems are able to do so). This suggests this is a very bad litmus test if almost no languages can actually pass it even though a) languages exist with explainable type errors b) the languages are general purpose and fairly expressive c) they support type inference. An obvious example of this is Rust. [1] https://stackoverflow.com/questions/33546004/is-it-possible-to-define-omega-combinator-%CE%BBx-xx-in-modern-haskell https://stackoverflow.com/questions/33546004/is-it-possible-...
    - kccqzy 2y ago
      You have a different definition of "works well" and also a different definition of "type inference" here. Rust doesn't have global type inference. C++'s `auto` doesn't count. Go's `:=` syntax doesn't count. Why not? Because you are adding typing retroactively to a dynamically typed language like Python. If a language was built with typing, you can do this because your initial choice of a type system already constrains the set of valid programs. But a Python-like language where users are already used to having no restrictions on runtime types? Absolutely not. Especially not in a language that encourages duck typing. Let's go back to the omega combinator example. The Stack Overflow link is correct: Haskell cannot assign a type to it. That means the type system is purposefully designed weak enough that the omega combinator cannot be written in the first place! No valid Haskell program has it! Therefore you can totally disregard it. Python is different. You can already write the omega combinator in it. I wrote it three times in this thread. So a bolt-on type system needs to assign a type to it. And you can't. Python does not have a type system that "works well" and will never have one.
      - vlovich123 2y ago
        I think the disagreement is about what “works well” means. You are approaching it from some kind of theoretical purity whereas most people approach it from the perspective of “works for every program I am likely to encounter”. Omega combinators aren’t an example of something typically written in Python. I think you’re making a similar decision about global type inference as the only “true” definition of type inference when clearly more limited type inference already adds a significant amount of utility & there’s not typically that much lost in an inability to avoid typing functions - it’s a bit inconvenient in some places, but overall acts as a way to define the explicit contract between the method body and the rest of the code which makes errors faster to spot and the language compile more quickly. You are correct that the holy grail you’re trying to reach is impossible, but relaxing some constraints still yields a heck of a lot of practical benefit.
deleted 2y ago
[deleted]

by kccqzy 2y ago

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.
- vlovich123 2y ago
  This seems like a very weird technical explanation that doesn’t actually address my question. Python typing works well in practice and doesn’t suffer from any of the problems you listed. Also, from a brief investigation, according to [1] Haskell also isn’t able to express the omega combinator in its type system (& indeed the answer says very few type systems are able to do so). This suggests this is a very bad litmus test if almost no languages can actually pass it even though a) languages exist with explainable type errors b) the languages are general purpose and fairly expressive c) they support type inference. An obvious example of this is Rust. [1] https://stackoverflow.com/questions/33546004/is-it-possible-to-define-omega-combinator-%CE%BBx-xx-in-modern-haskell https://stackoverflow.com/questions/33546004/is-it-possible-...
  - kccqzy 2y ago
    You have a different definition of "works well" and also a different definition of "type inference" here. Rust doesn't have global type inference. C++'s `auto` doesn't count. Go's `:=` syntax doesn't count. Why not? Because you are adding typing retroactively to a dynamically typed language like Python. If a language was built with typing, you can do this because your initial choice of a type system already constrains the set of valid programs. But a Python-like language where users are already used to having no restrictions on runtime types? Absolutely not. Especially not in a language that encourages duck typing. Let's go back to the omega combinator example. The Stack Overflow link is correct: Haskell cannot assign a type to it. That means the type system is purposefully designed weak enough that the omega combinator cannot be written in the first place! No valid Haskell program has it! Therefore you can totally disregard it. Python is different. You can already write the omega combinator in it. I wrote it three times in this thread. So a bolt-on type system needs to assign a type to it. And you can't. Python does not have a type system that "works well" and will never have one.
    - vlovich123 2y ago
      I think the disagreement is about what “works well” means. You are approaching it from some kind of theoretical purity whereas most people approach it from the perspective of “works for every program I am likely to encounter”. Omega combinators aren’t an example of something typically written in Python. I think you’re making a similar decision about global type inference as the only “true” definition of type inference when clearly more limited type inference already adds a significant amount of utility & there’s not typically that much lost in an inability to avoid typing functions - it’s a bit inconvenient in some places, but overall acts as a way to define the explicit contract between the method body and the rest of the code which makes errors faster to spot and the language compile more quickly. You are correct that the holy grail you’re trying to reach is impossible, but relaxing some constraints still yields a heck of a lot of practical benefit.

deleted 2y ago

[deleted]