4 ms·

That's a completely arbitrary definition, and it is wrong. Type inference limited to the initialization point is still type inference, and actually most languag

That's a completely arbitrary definition, and it is wrong. Type inference limited to the initialization point is still type inference, and actually most languages before Rust and Swift that have local type inference (C#, D, C++11) are limited to type inference at the declaration/initialization point.

catnaroek 10y ago
> That's a completely arbitrary definition, and it is wrong. The definition is very simple - the inference engine must use nontrivial inference rules to reconstruct the types. The rule “given P then P” alone doesn't quite cut it, which means that ”given that 0 is an int, then something that's initialized to 0 is an int“ also doesn't quite cut it. Calling what Go, C# and C++11 have “type inference” is akin to calling Python a statically typed language because it has a trivial type system with exactly one static type. > actually most languages before Rust and Swift that have local type inference (C#, D, C++11) are limited to type inference at the declaration/initialization point. Then they just have unidirectional type propagation - which is perfectly fine, just not type inference.
- deleted 10y ago
  [deleted]
- Raphael_Amiard 10y ago
  > The definition is very simple - the inference engine must use nontrivial inference rules to reconstruct the types. Where exactly is this rule coming from ? What is the source of your definition ? And if it is the authoritative definition, why don't you go rewrite the wikipedia page, which is then wrong ? https://en.wikipedia.org/wiki/Type_inference https://en.wikipedia.org/wiki/Type_inference > The rule “given P then P” alone doesn't quite cut it "Doesn't quite cut it" sounds like a very precise and scientific definition ! Also your categorization of C# is wrong, even by your own definition, because of function types inference and of subtyping, which makes the algorithm non trivial. > Then they just have unidirectional type propagation - which is perfectly fine, just not type inference. Again: 1. This is wrong, even by your own definition. You can have local type inference limited to the initialization point, and have non trivial resolution rules. See this paper by Benjamin Pierce for an example : http://www.cis.upenn.edu/~bcpierce/papers/lti-toplas.pdf http://www.cis.upenn.edu/~bcpierce/papers/lti-toplas.pdf 2. Where is this definition even coming from ? In my book, unidirectional type propagation is a form of type inference, and it quite logically follows: The type is inferred. The fact that you chose to draw a line, say, to flow sensitive inference (in the case of Rust and Swift) or to global unification style inference (ala ML) is a completely arbitrary definition, and one that I have to this day never encountered. Indeed, I can't find any online resource that agrees with you. Most language documentations, including C#, C++ and Go, call this type inference. Most researchers call any mechanism where a language infers the type, type inference, even the mechanism that allows you to call generic without specifying the type of the instantiation, as in this paper : https://www.researchgate.net/profile/Erik_Meijer/publication/221321900_Lost_in_translation_Formalizing_proposed_extensions_to_C/links/0c960538ae979a41f8000000.pdf https://www.researchgate.net/profile/Erik_Meijer/publication... I have absolutely never encountered any definition of type inference which draws this line, and for good reasons, because it doesn't make any sense.
  - catnaroek 10y ago
    You are right about C#: The type of `x => x + 1` can't be said to be anything other than "inferred". I stand corrected. But I disagree with the rest of your post. From the point of view of type inference, what matters is the nature of the type constraints that the type checking algorithm generates: (0) Traditional type checking: All type constraints are of the form “T1 = T2”, where both “T1” and “T2” are closed type expressions. There is nothing to infer. (1) Type propagation: All type constraints are of the form “X = T”, where “X” is a type variable and “T” is a closed type expression. Again, there is nothing to infer, but we might need to propagate “T” between places. Say, from the RHS to the LHS of a variable initialization. (2) Type inference: Type constraints are arbitrary type expressions, which must be solved using a unification algorithm. As for why type propagation doesn't count as type inference: http://lambda-the-ultimate.org/node/4771#comment-75771 http://lambda-the-ultimate.org/node/4771#comment-75771
deleted 10y ago
[deleted]

catnaroek 10y ago

> That's a completely arbitrary definition, and it is wrong. The definition is very simple - the inference engine must use nontrivial inference rules to reconstruct the types. The rule “given P then P” alone doesn't quite cut it, which means that ”given that 0 is an int, then something that's initialized to 0 is an int“ also doesn't quite cut it. Calling what Go, C# and C++11 have “type inference” is akin to calling Python a statically typed language because it has a trivial type system with exactly one static type. > actually most languages before Rust and Swift that have local type inference (C#, D, C++11) are limited to type inference at the declaration/initialization point. Then they just have unidirectional type propagation - which is perfectly fine, just not type inference.

deleted 10y ago
[deleted]
Raphael_Amiard 10y ago
> The definition is very simple - the inference engine must use nontrivial inference rules to reconstruct the types. Where exactly is this rule coming from ? What is the source of your definition ? And if it is the authoritative definition, why don't you go rewrite the wikipedia page, which is then wrong ? https://en.wikipedia.org/wiki/Type_inference https://en.wikipedia.org/wiki/Type_inference > The rule “given P then P” alone doesn't quite cut it "Doesn't quite cut it" sounds like a very precise and scientific definition ! Also your categorization of C# is wrong, even by your own definition, because of function types inference and of subtyping, which makes the algorithm non trivial. > Then they just have unidirectional type propagation - which is perfectly fine, just not type inference. Again: 1. This is wrong, even by your own definition. You can have local type inference limited to the initialization point, and have non trivial resolution rules. See this paper by Benjamin Pierce for an example : http://www.cis.upenn.edu/~bcpierce/papers/lti-toplas.pdf http://www.cis.upenn.edu/~bcpierce/papers/lti-toplas.pdf 2. Where is this definition even coming from ? In my book, unidirectional type propagation is a form of type inference, and it quite logically follows: The type is inferred. The fact that you chose to draw a line, say, to flow sensitive inference (in the case of Rust and Swift) or to global unification style inference (ala ML) is a completely arbitrary definition, and one that I have to this day never encountered. Indeed, I can't find any online resource that agrees with you. Most language documentations, including C#, C++ and Go, call this type inference. Most researchers call any mechanism where a language infers the type, type inference, even the mechanism that allows you to call generic without specifying the type of the instantiation, as in this paper : https://www.researchgate.net/profile/Erik_Meijer/publication/221321900_Lost_in_translation_Formalizing_proposed_extensions_to_C/links/0c960538ae979a41f8000000.pdf https://www.researchgate.net/profile/Erik_Meijer/publication... I have absolutely never encountered any definition of type inference which draws this line, and for good reasons, because it doesn't make any sense.
- catnaroek 10y ago
  You are right about C#: The type of `x => x + 1` can't be said to be anything other than "inferred". I stand corrected. But I disagree with the rest of your post. From the point of view of type inference, what matters is the nature of the type constraints that the type checking algorithm generates: (0) Traditional type checking: All type constraints are of the form “T1 = T2”, where both “T1” and “T2” are closed type expressions. There is nothing to infer. (1) Type propagation: All type constraints are of the form “X = T”, where “X” is a type variable and “T” is a closed type expression. Again, there is nothing to infer, but we might need to propagate “T” between places. Say, from the RHS to the LHS of a variable initialization. (2) Type inference: Type constraints are arbitrary type expressions, which must be solved using a unification algorithm. As for why type propagation doesn't count as type inference: http://lambda-the-ultimate.org/node/4771#comment-75771 http://lambda-the-ultimate.org/node/4771#comment-75771

deleted 10y ago

[deleted]