227 reads

The Basics of a Standard Type Inference Technique

by Leandro T. C. MeloSeptember 24th, 2020

Too Long; Didn't Read

Since C# 3.0, developers may declare implicitly typed variables with the type of an initializer. Type inference is a common feature among mainstream programming languages. The de facto type inference discipline adopted in typical functional languages is that of Hindley-Milner’s type system. In this article, I will describe (at a superficial level) the core ideas behind a constraint-based approach to type-inclusion. A constraint language is composed by its own syntactic language, and by the language which we are modelling; C# type is a constraint language.

Companies Mentioned

featured image - 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 implicitly typed variables with the

var

keyword (in C++ 11, a similar feature was introduced — re-targeting the then-existing

auto

keyword). This functionality, however, falls under a provision: a declaration must be accompanied by an initializer.

Although one would not expect to see ML and Haskell’s “whole-program type inference” in C#, could this initializer requirement be relaxed? Why does it exist, altogether?

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

var

-declared variable is accompanied with an initializer? The accurate reply to this question is: because the language specification says so; it is not because the type would not be inferable otherwise. Consider function

The two statements above (a declaration- and an expression-statement) are not fundamentally different from the single statement

var num = 42;

. In fact, if permitted, the Intermediate Language (IL) code produced for the former would probably be equal to that produced for the latter. Also, one may easily observe that

int

is a valid replacement for

var

To set the stage for our discussion, let us quote — with minor adjustments for pedagogical reasons — the relevant fragment of the C# specification to which var is subject:

“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 definitely assigned before we attempt to obtain its value. Let us also quote the language specification fragment that states such mandatory assignment.

“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

var num; num = 42;

is equivalent to

var num = 42;

, and the fact that a variable must be assigned before being used, could we slightly stretch the functionality provided by

var

Hindley-Milner, Constraints, and Unification

In our small and trivial function

, it is clear that

int

is a valid type for the program variable

num

. 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 Hindley-Milner’s type system.

Here, I will describe (at a superficial level) the core ideas behind a constraint-based variation of Hindley-Milner, alongside a simplified version of a popular constraint-generation and constraint-solving technique that builds on the unification framework to implement such a type system. The setup I present is more elaborate than what would be essential to our discussion about

var

— to make it comprehensible in the event one would like to further extend it.

A Constraint Language

A primary component of a constraint-based 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 modelled language. We refer to a C# type (e.g., an

int

System.DateTime

) by 𝝉, and to a type variable , which is a type too, by 𝜶.

The BNF grammar of our constraint language is as follows. C is a constraint.

C ::= def f : 𝜶 in C | ∃𝜶. C | C ^ C | 𝝉 = 𝝉

The first constraint form, def, introduces a function identified by f, whose type is 𝜶. (A function type is denoted with the classical arrow notation.) The second form, ∃, is an existential constraint which indicates that 𝜶 “holds” some type that may be employed in a constraint. The ^ operator, appearing in the third constraint form, is logical conjunction — think of it as the & operator 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, decl_type(𝒗), which designates the declared type of a 𝒗ariable, and type_of(𝓵), which designates the type of a 𝓵iteral.

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 generate the constraint associated with a program. This task is usually accomplished in a syntax-directed manner, i.e., we traverse the program’s Abstract Syntax Tree (AST) and, while doing so, generate a constraint that is sound in respect to the modelled language. Below is how a constraint for

could look like:

def

string

→

void

in ∃𝜶1. decl_type(

num

) = 𝜶1 ^ 𝜶1 = type_of(

)

A constraint implies the typing of a program. But for it to be really useful, type variables must be instantiated. This is achieved by solving the constraint. Let us do that for the one generated for

def is intrinsic to scope; there are various ways to deal with it, e.g., through De Bruijn Indices. We assume that a function comprises a single naming environment and conflicts never happen. Also,
```
f
```
is not called recursively, none of the expressions in its body mention the parameter
```
name
```
, its
```
void
```
return is uninteresting, and it contains no local functions inside it. These allow us to reduce the previous constraint as follows.

∃𝜶1. decl_type(
```
num
```
) = 𝜶1 ^ 𝜶1 = type_of(
```
42
```
)

Because the type variable 𝜶1 does not occur free in the constraint, we may eliminate the existential quantification.

decl_type(
```
num
```
) = 𝜶1 ^ 𝜶1 = type_of(
```
42
```
)
We now evaluate operator calls. type_of(
```
42
```
) evaluates to
```
int
```
; for decl_type(
```
num
```
), we introduce a fresh type variable for each program variable, and store the corresponding mappings in a set — this set is referred to as 𝜓.

𝜶2 = 𝜶1 ^ 𝜶1 =
```
int
```
where 𝜓 = { (
```
num
```
, 𝜶2) }

At this point, our constraint is in a normal format such that it is eligible for a final solving stage by an off-the-shelf framework.

Unification and Typing

What remains from the partly-solved constraint of function

is two equalities. A solution to those is a substitution, from type variables to types, that will ideally render the constraint in question satisfiable. This is exactly what unification provides us with. Specifically, as the result of a successful unification, we have a “special” substitution that is referred to as the most general unifier (mgu), which, in turn, suggests a 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 applied both on the remaining constraint, 𝜶1 =
```
int
```
, and on 𝜓. The application of a substitution is denoted with juxtaposition, therefore: 𝝈C = [𝜶2 ↦ 𝜶1]𝜶1 =
```
int
```
and 𝝈𝜓 = [𝜶2 ↦ 𝜶1]{ (
```
num
```
, 𝜶2) }.
a) The former operation has no effect, for that 𝜶2 does not appear further.
b) The latter, 𝝈𝜓, results in 𝜓 = { (
```
num
```
, 𝜶1) }.

Lastly, we move on to the constraint that follows, 𝜶1 =
```
int
```
, and repeat the process from the beginning.

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

int

against a

string

. Our example terminates without any error, after the second iteration, when [𝜶1 ↦

int

] is computed and applied on 𝜓, leaving it as:

𝜓 = { (num, int) }

The mapping above tells us that

int

is a solution as the type of program variable

num

. If the constraint that we generated for

is indeed sound, then replacing

var

for

int

in the original source-code must yield a well typed C# program, according to the language’s typing judgements.

In a formal semantics, typing judgements are defined by means of inference rules like this one, for a basic (symmetric) assignment.

The above rule says that, under the judgement of the typing environment 𝚪, whenever the type of an assignment is 𝝉, then the type of its left-hand-side expression and its right-hand-side expression are 𝝉 as well. However, in a constraint-based setting, the constraint — or 𝜓 in our formulation — must be accounted as part of the environment too, enriching the rule as follows.

Back to the C# Universe

We have seen that, from a technical standpoint, it is possible to stretch the functionality of C#’s

var

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 D language already exists — pun intended.)

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, as-is. We know that the compiler would have no problem to infer the type of

num

int

, but would developers find that an intelligible approach? Consider this function

, a slightly incremented

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

dynamic

keyword in C# 4.0 prompted a confusion between said new keyword and

var

. The developer’s intention was perhaps to write

like this:

In spite of the contrast between

var

and

dynamic

, as a language designer, one wants to avoid potential confusion. Therefore, it might indeed be sensible to forbid non-initializing

var

-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

var

and

static

are combined, as in this C## version of

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

var dynamic

as a synonym of the plain

dynamic

Type Conversions, Subtyping, and Generics

The foremost advantage of requiring that a

var

-declared variable is accompanied by an initializer 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 use, our inference needs to account for further possibilities when typing a valid program.

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

int

, but we may not type

as such; otherwise, the subsequence assignment would trigger a compilation error, given that the type of literal

1.6180F

float

, but no coercion from

float

int

is available. One correct alternative is to type

float

— keep in mind that C# allows developers to define implicit/explicit type conversions.

In the presence of subtype polymorphism, the situation is similar.

Now, a compilation error would be triggered if we inferred, based on the first assignment, the type of

. To avoid this error, one may naively think that always inferring a top type is a solution to this situation; leading to

as the type

, and, likewise,

double

as the type of

in function

conv

. But that strategy does not work in general, because there might be further uses of the implicitly typed variable that impose a specific type: a call

w.b()

sub

, or a call

whoops(v)

conv

, where

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

var static

-declared variables in C##. A notorious challenge is parametric polymorphism; put into that bucket covariance and contravariance as well, features that are 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:

Type schemes and let-polymorphism, for fine-grained control over generalization and instantiation of types.
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 nominal or 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),

var

was originally conceived for anonymous types. 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.

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