The Basics of a Standard Type Inference Technique

Type inference is a common feature among mainstream programming languages. The functional ones, like ML and Haskell, are pioneers in exploring this programming paradigm where the declaration of a variable or a function may omit a type annotation. Today, even classic imperative languages such as C++ offer, to a certain extent, a kind of type inference. C# is not an exception to the ever-increasing popularity of inference-enabled languages: since C# 3.0, developers may declare with the (in C++ 11, a similar feature was introduced — re-targeting the then-existing ). This functionality, however, falls under a provision: a declaration must be accompanied by an . implicitly typed variables var keyword auto keyword initializer Although one would not expect to see ML and Haskell’s “whole-program type inference” in C#, could this requirement be relaxed? Why does it exist, altogether? initializer Is it due to any limitation or just a matter of taste? Could the variable's type be inferred from arbitrary ? expressions If yes, what are trade-offs from a language-design perspective? In this article, I will describe the foundation of a standard type inference technique and ramble about the questions above. Non-initializing Declarations What do you answer when someone asks: why is it necessary, in C#, that a local -declared variable is accompanied with an The accurate reply to this question is: because the ; it is not because the type would not be inferable otherwise. Consider function . var initializer? language specification says so f The two above (a and an ) are not fundamentally different from the single . In fact, if permitted, the (IL) code produced for the former would probably be equal to that produced for the latter. Also, one may easily observe that is a valid replacement for in . statements declaration- expression-statement statement var num = 42; Intermediate Language int var f To set the stage for our discussion, let us quote — with minor adjustments for pedagogical reasons — the relevant fragment of the to which var is subject: C# specification “When the local variable type is specified as var… the declaration is an implicitly typed local variable declaration, whose type is inferred from the type of the associated initializer expression.” Another characteristic of C# is that a variable must be before we attempt to obtain its value. Let us also quote the language specification that states such mandatory assignment. definitely assigned fragment “For an initially unassigned variable to be considered definitely assigned… , an assignment to the variable must occur in every possible execution path…” It is not my intent to enter the pedantic realm of language specifications. Yet, based on our (informal) observation that is equivalent to , and the fact that a variable must be assigned before being , could we slightly stretch the functionality provided by ? var num; num = 42; var num = 42; used var Hindley-Milner, Constraints, and Unification In our small and trivial function , it is clear that is a valid type for the program variable . But, in a general setup, reasoning about the typing relations among a set of expressions demands a systemic approach. The de facto type inference discipline adopted in typical functional languages is that of . f int num Hindley-Milner’s type system Here, I will describe (at a superficial level) the core ideas behind a of Hindley-Milner, alongside a simplified version of a popular technique that builds on the to implement such a type system. The setup I present is more elaborate than what would be essential to our discussion about — to make it comprehensible in the event one would like to further extend it. variation constraint-based and constraint-generation constraint-solving unification framework var A Constraint Language A primary component of a inference technique is a constraint language. A constraint language is composed by its own syntactic elements, and by the types of the (programming) language which we are modelling; in our case, C# is the language. We refer to a C# type (e.g., an or ) by 𝝉, and to a , which is a type too, by 𝜶. constraint-based modelled int System.DateTime type variable The grammar of our constraint language is as follows. C is a constraint. BNF C ::= : 𝜶 C | 𝜶 C | C C | 𝝉 𝝉 def f in ∃ . ^ = The first constraint form, , introduces a function identified by , whose type is 𝜶. (A function type is denoted with the classical .) The second form, , is an constraint which indicates that 𝜶 “holds” some type that may be employed in a constraint. The operator, appearing in the third constraint form, is — think of it as the in C#. The last form is a constraint that expresses type equality; it is on this one that we will focus. Moreover, our constraint language is equipped with two builtin operators, (𝒗), which designates the declared type of a 𝒗ariable, and (𝓵), which designates the type of a 𝓵iteral. def f arrow notation ∃ existential ^ logical conjunction & operator decl_type type_of A constraint language must also have its semantics defined. But, except for the equality of types, I will not do so in this article — that would entail a longer discussion… and one that is expendable for this general presentation. Having said that, the semantic definition that we have for 𝝉 𝝉 is straightforward: that of . = mathematical equality Constraint Generation and Constraint Solving Supplied with a constraint language, we may the constraint associated with a program. This task is usually accomplished in a manner, i.e., we traverse the program’s (AST) and, while doing so, generate a constraint that is in respect to the language. Below is how a constraint for could look like: generate syntax-directed Abstract Syntax Tree sound modelled f : → 𝜶1 ( ) 𝜶1 𝜶1 ( ) def f string void in ∃ . decl_type num = ^ = type_of 42 A constraint implies the typing of a program. But for it to be really useful, must be instantiated. This is achieved by the constraint. Let us do that for the one generated for . type variables solving f is intrinsic to scope; there are various ways to deal with it, e.g., through . We assume that a function comprises a single naming environment and conflicts never happen. Also, is not called recursively, none of the in its body mention the parameter , its return is uninteresting, and it contains no inside it. These allow us to reduce the previous constraint as follows. 𝜶1 ( ) 𝜶1 𝜶1 ( ) def De Bruijn Indices f expressions name void local functions ∃ . decl_type num = ^ = type_of 42 Because the 𝜶1 does not in the constraint, we may eliminate the existential quantification. ( ) 𝜶1 𝜶1 ( ) type variable occur free decl_type num = ^ = type_of 42 We now evaluate operator calls. ( ) evaluates to ; for ( ), we introduce a type variable for each program variable, and store the corresponding mappings in a set — this set is referred to as . 𝜶2 𝜶1 𝜶1 = { ( , 𝜶2) } type_of 42 int decl_type num fresh 𝜓 = ^ = int where 𝜓 num At this point, our constraint is in a such that it is eligible for a final solving stage by an off-the-shelf framework. normal format Unification and Typing What remains from the partly-solved constraint of function is two equalities. A solution to those is a , from to types, that will ideally render the constraint in question . This is exactly what provides us with. Specifically, as the result of a successful unification, we have a “special” substitution that is referred to as the (mgu), which, in turn, suggests a . f substitution type variables satisfiable unification most general unifier principal type Provided with an implementation of unification, this is how to proceed. Initially, we unify the first constraint of the conjunction, 𝜶2 𝜶1. The return is a substitution of 𝜶2 for 𝜶1, written as 𝝈 = [𝜶2 ↦ 𝜶1]. = Next, 𝝈 must be both on the remaining constraint, 𝜶1 , and on . The application of a substitution is denoted with , therefore: 𝝈C = [𝜶2 ↦ 𝜶1]𝜶1 and 𝝈 = [𝜶2 ↦ 𝜶1]{ ( , 𝜶2) }. a) The former operation has no effect, for that 𝜶2 does not appear further. b) The latter, 𝝈 , results in = { ( , 𝜶1) }. applied = int 𝜓 juxtaposition = int 𝜓 num 𝜓 𝜓 num Lastly, we move on to the constraint that follows, 𝜶1 , and repeat the process from the beginning. = int This iteration goes on until the entire constraint is processed or an error happens, e.g., due to an attempt of unifying incompatible types likes an against a . Our example terminates without any error, after the second iteration, when [𝜶1 ↦ ] is computed and on , leaving it as: int string int applied 𝜓 = { (num, int) } 𝜓 The mapping above tells us that is a solution as the type of program variable . If the constraint that we generated for is indeed , then replacing for in the original source-code must yield a well typed C# program, according to the language’s typing . int num f sound var int judgements In a , typing judgements are defined by means of like this one, for a basic (symmetric) assignment. formal semantics inference rules The above rule says that, under the judgement of the 𝚪, whenever the type of an assignment is 𝝉, then the type of its left-hand-side and its right-hand-side are 𝝉 as well. However, in a setting, the constraint — or in our formulation — must be accounted as part of the environment too, enriching the rule as follows. typing environment expression expression constraint-based 𝜓 Back to the C# Universe We have seen that, from a technical standpoint, it is possible to stretch the functionality of C#’s a bit further. But at what “cost”? There are trade-offs to be aware of. To have a sense of those, let us pretend that we are extending C# into a fictitious language named C##. (We shall not “resolve” the double hash, since a already exists — pun intended.) var D language Of course, I will not go into every possible language-design aspect here; I would not know all of them myself, as a matter of fact. So the upcoming sections are just a glimpse of the highlights. The Dynamic Typing Confusion Suppose that, in C##, we decided to accept the syntax of our original function, . We know that the compiler would have no problem to infer the type of as , but would developers find that an intelligible approach? Consider this function , a slightly incremented . f as-is num int g f The error above may be obvious to some, but, apparently, not to all. This affirmation is in view of the fact that the introduction of the in C# 4.0 prompted a . The developer’s intention was perhaps to write like this: dynamic keyword confusion between said new keyword and var g In spite of the contrast between and , as a language designer, one wants to avoid potential confusion. Therefore, it might indeed be sensible to forbid non-initializing -declarations in C##. However… what if we demand, for a non-initializing implicitly typed variable, an extra level of consciousness from the developer? For example, that the keywords and are combined, as in this C## version of . var dynamic var var static g A collateral coolness of the above approach is that it reuses an existing keyword. This change is subtle. Whether or not it would effectively eliminate doubts for the general audience, I cannot tell, though. Toward “consistency”, we could also enable as a synonym of the plain . var dynamic dynamic Type Conversions, Subtyping, and Generics The foremost advantage of requiring that a -declared variable is accompanied by an is that there is no ambiguity in deciding what the variable's type is. By giving away this obligation, yet retaining the requirement that variables must be assigned prior to their , our inference needs to account for further possibilities when typing a valid program. var initializer use Inferring a type that renders an individual assignment correct, but which fails to type another assignment to the same implicitly typed variable. Inferring multiple unequal types that render all assignments to the implicitly typed variable correct. This situation is exemplified by function . conv The type of the literal is , but we may not type as such; otherwise, the subsequence assignment would trigger a compilation error, given that the type of literal is , but no from to is available. One correct alternative is to type as — keep in mind that C# allows developers to define . 42 int v 1.6180F float coercion float int v float implicit/explicit type conversions In the presence of , the situation is similar. subtype polymorphism Now, a compilation error would be triggered if we inferred, based on the first assignment, the type of as . To avoid this error, one may naively think that always inferring a is a solution to this situation; leading to as the type , and, likewise, as the type of in function . But that strategy does not work in general, because there might be further of the implicitly typed variable that impose a specific type: a call in , or a call in , where is . w C top type A w double v conv uses w.b() sub whoops(v) conv whoops void whoops(float p) {} There are other language constructs that I do not mention in these basic examples that would also demand special care in the non-initializing behavior of -declared variables in C##. A notorious challenge is ; put into that bucket as well, features that are . var static parametric polymorphism covariance and contravariance supported by C#’s generics It is certainly possible to deal with many (maybe all) of the difficulties I just presented in a nice way. However, advances in our type inference technique and constraint language would be necessary — alongside eventual syntax hints. A few to consider are: and , for fine-grained control over and of types. Type schemes let-polymorphism generalization instantiation Constraints in the form of type inequalities, i.e., 𝝉 ≤ 𝝉, whose implied semantics may of a subtype: 𝝉 <: 𝝉 . Its interpretation, in turn, depend, among other matters, on whether the system is or . nominal structural Is it Worth It? After all this rambling, the natural question is: would it be worth it or anyhow beneficial to incorporate, in C#, the feature we have been discussing about? The language specification could be amended in the following (loose) way: “When the local variable type is specified as var… the declaration is an implicitly typed local variable declaration, whose type is inferred from the type of the associated initializer expression; ” if said variable is specified as var static, its type is inferred from assignment expressions involving it. That being said — and as a disclaimer — , I do not feel in position to make a thorough evaluation of this “proposal”. Apart from the technicalities, a primary aspect to consider is the actual/practical benefit (if any) implied in such a feature. To my understanding (I am not affiliated to Microsoft), was originally conceived for . Yet, I believe that extending its functionality to non-anonymous types was likely a choice of convenience. Then, under the subjectiveness of what is convenient…, one may just as well wish to write the code as in function below. var anonymous types z Thank you for reading! I hope you have enjoyed the text — if you did, I would be curious to hear your feedback; and even more grateful if you share this article further. Read behind a paywall at https://medium.com/p/stretching-the-reach-of-implicitly-typed-variables-in-c-16882318a92

The Basics of a Standard Type Inference Technique

Too Long; Didn't Read

Companies Mentioned

@ltcmelo

RELATED STORIES