Record type inference

Question

In the following code snippet

type myrec1 = {x: int; y: int}
type myrec2 = {x: int; y: int; z: int}

let p1 = {x = 1; y = 1}  // Error. p1 compiler assumes p1 has the type myrec2

// It works with additional type specification
let p1: myrec1 = {x = 1; y = 1}
let p2: myrec2 = {x = 1; y = 1; z = 1}

The line with the comment does not compile. For some reason the type checker cannot figure out that the type for p1 should be myrec1. Is it because this case of type inference is simply unsolvable or is it just a limitation of F# type inference?

Answer 1

From here:

The labels of the most recently declared type take precedence over those of the previously declared type

So if you do it like this:

type myrec2 = {x: int; y: int; z: int}
type myrec1 = {x: int; y: int}

let p1 = {x = 1; y = 1}

then it will work.

For your reading pleasure from here (the F# 3.0 Spec):

field-initializer : long-ident = expr

6.3.5 Record Expressions

In this case our field-initializer is not a single identifier, so it uses "Field Label Resolution" from 14.1.9.

Each field-initializeri has the form field-labeli = expri. Each field-labeli is a long-ident, which must resolve to a field Fi in a unique record type R as follows:

·         If field-labeli is a single identifier fld and the initial type is known to be a record type R<,...,> that has field Fi with name fld, then the field label resolves to Fi.

·         If field-labeli is not a single identifier or if the initial type is a variable type, then the field label is resolved by performing Field Label Resolution (see §14.1) on field-labeli. This procedure results in a set of fields FSeti. Each element of this set has a corresponding record type, thus resulting in a set of record types RSeti. The intersection of all RSeti must yield a single record type R, and each field then resolves to the corresponding field in R.

14.1.9 Field Label Resolution

Our long-ident is a FieldLabel, so it's looked up using the FieldLabels table described in 8.4.2.

Field Label Resolution specifies how to resolve identifiers such as field1 in { field1 = expr; ... fieldN = expr }. Field Label Resolution proceeds through the following steps:

1.     Look up all fields in all available types in the Types table and the FieldLabels table (§8.4.2).

2.     Return the set of field declarations.

8.4.2     Name Resolution and Record Field Labels

As noted here, the FieldLabels table is used in Name Resolution for Members (14.1).

For a record type, the record field labels field1 ... fieldN are added to the FieldLabels table of the current name resolution environment unless the record type has the RequireQualifiedAccess attribute. Record field labels in the FieldLabels table play a special role in Name Resolution for Members (§14.1): an expression’s type may be inferred from a record label. For example: type R = { dx : int; dy: int } let f x = x.dx // x is inferred to have type R In this example, the lookup .dx is resolved to be a field lookup.

14.1.4Name Resolution in Expressions This section seems a bit fuzzy, but I think it uses Name Resolution at this point. As noted at the end, return the first item if there are more than one.

Given an input long-ident, environment env, and an optional count n of the number of subsequent type arguments <,...,>, Name Resolution in Expressions computes a result that contains the interpretation of the long-ident<,...,> prefix as a value or other expression item, and a residue path rest. How Name Resolution in Expressions proceeds depends on whether long-ident is a single identifier or is composed of more than one identifier. If long-ident is a single identifier ident:

1.     Look up ident in the ExprItems table. Return the result and empty rest.

2.     If ident does not appear in the ExprItems table, look it up in the Types table, with generic arity that matches n if available. Return this type and empty rest.

3.     If ident does not appear in either the ExprItems table or the Types table, fail.

...

If the expression contains ambiguities, Name Resolution in Expressions returns the first result that the process generates.

The part which you're interested in is the very last line above: "returns the first result that the process generates".

Answer 2

This behavior is by design. I can't say if it's a limitation of F#'s type inference, or a limitation of type inference algorithms in general; if you think about it, there are two options though:

1. Given a record expression {x = 1; y = 1}, match the 'x' and 'y' fields against the last type to declare either of them. This is the easiest to understand, and it's how the F# compiler implements the record type inference.

2. Try to determine the 'best fit' based on the fields of the types in the current scope. (I think this is what you are asking about.)

   However, this algorithm could lead to other issues; specifically, for a record expression {x = 1; y = 1} the compiler can't tell if you meant to create an expression of type myrec1, or if you meant to create an expression of myrec2 and you forgot to assign a value to the z field.

   Also, what should the compiler do if you declare two types with the exact same fields? E.g., what if you add:

   type myrec3 = {x: int; y: int}
   

In other words, there is no such thing as a free lunch -- you can increase the "power" of the type inference, but it'll cost you some accuracy in the error diagnosis you get from the compiler.

Answer 3

If you want record types with similarly named fields, the way to distinguish between them is this:

let p1 = {myrec1.x = 1; y = 1}

Answer 4

Since there are no type annotations, the compiler infers the record type from the labels but those of the first type are not sufficiently distinct from the labels of the second so the latter takes precedence and p1 is inferred to be of type myrec2. Use different labels in order to avoid type annotations and get the expected type inference behavior:

type myrec1 = {x1: int; y: int}
type myrec2 = {x2: int; y: int; z: int}

let p1 = {x1 = 1; y = 1}