A bidirectional typechecking puzzle

Recently I stumbled across a bidirectional typechecking puzzle in my Grace programming language that I thought people interested in programming language theory might find interesting.

The context is that Grace is based on a bidirectional typechecking system (specifically: Complete and Easy Bidirectional Typechecking for Higher-Rank Polymorphism) and as Grace evolved I began to run into a few limitations of that approach. Some of these limitations I could workaround with various hacks but recently these workarounds piled up to generate a bizarre bug.

The problem

To illustrate the bug, consider this Grace program:

let authorities = [ { domain: "google.com" }
                  , { domain: "localhost", port: 8080 }
                  ]

for { domain, port = 443 } of authorities

in  "${domain}:${show port}"

You can read this program as describing a list comprehension:

Iterate over each record in the list of authorities and for each one bind the domain and port fields to variables of the same name, defaulting port to 443 if absent. Return "${domain}:${show port}" for each authority record.

I would expect a program like this to return:

[ "google.com:443", "localhost:8080" ]

… but the bugged version would return:

[ "google.com:443", "localhost:443" ]

What gives? The port: 8080 field in the second record is being completely ignored.

Bidirectional typechecking

You might think that this is a problem with Grace's evaluator but actually it's a problem with Grace's typechecker if you can believe that.

The first part of the problem arises out of how Grace infers the type of lists. The type I would like Grace to infer for the list of authorities is:

List { domain: Text, port: Optional Natural }

… which you can read as:

a List of records, each of which has a required domain field storing Text and an Optional port field storing a Natural number

However, that is not the type that Grace actually infers:

>>> :type [ { "domain": "google.com" }, { "domain": "localhost", "port": 8080 } ]
List { domain: Text }

Whoops! Why is that?

Well, it's related to Grace using a bidirectional typechecker, where typechecking operations essentially come in two flavors:

• infer the type of an expression
• check the type of an expression against an expected type

… and while that has some upsides (which I talk about in another post on the appeal of bidirectional typechecking) it has some downsides: you can't easily infer the type of a list because neither of those two operations provides a way to combine two or more element types into an element supertype for the whole list.

Before the bug fix, I'd hack around this by inferring the type of a list like this:

• infer the type of the first element of the list
• check every other element against the inferred type of the first element

… and that's why Grace would infer a type like this:

>>> :type [ { "domain": "google.com" }, { "domain": "localhost", "port": 8080 } ]
List { domain: Text }

… because the type of the first element is { domain: Text } so that would become the element type for the entire list. If you expected a different type then you had to add an explicit type annotation. This wasn't a great solution but it "worked" for a while as a half-measure.

Most of the bidirectional typechecking literature recommends a different solution: require a type annotation on the list because then you can check each element of the list against the expected element type. However, that also didn't sit right with me because I wanted Grace to work with real-world JSON which often has large and complicated schemas. I didn't want users to have to spell out the entire schema as a giant type annotation.

Elaboration

Okay, that explains why the type is wrong but that still doesn't explain why the result of evaluation is wrong. We've been talking about typechecking so far, but how does typechecking affect evaluation?

Well, Grace's typechecker does more than just flag type errors: it also adjusts the expression along the way, a process known as "elaboration". Specifically, when Grace checks a subtype against a supertype the typechecker inserts an explicit coercion converting the subtype to the supertype if they differ.

For example, Grace's evaluator internally represents all Optional values as either null or tagged as some x (for soundness reasons). However, if you input an expression without the tag where an Optional is expected then Grace will automatically insert a tag for you, like this:

>>> [ some 1, 2 ]  # This would be a type mismatch without elaboration
[ some 1, some 2 ]

There the type checker infers that the first element has type Optional Natural and then sees that the second element is a naked Natural number (without the some tag), but rather than flag that as a type error the typechecker helpfully inserts a some tag to fix the type mismatch.

The same thing happens with records, too! Grace supports record subtyping and also coerces the subtype to match the supertype. For example, if you annotate a record with a smaller record type:

>>> { x: 1, y: true }: { x: Natural }
{ "x": 1 }

… the typechecker allows that buuuut will also strip every field not present in the supertype. This coercion is important for soundness and the Appendix explains why in more detail.

This sort of coercion contributed to the bug in the original example, and we can see why if we evaluate the authorities list just by itself:

>>> [ { domain: "google.com" }, { domain: "localhost", port: 8080 } ]
[ { "domain": "google.com" }, { "domain": "localhost" } ]

We get this result because:

• the inferred type of the first element is { domain: Text }
• the second element is checked against that expected type
• the second element matches that type but also has an extra field (port)
• the typechecker strips the port field to match the expected type

I don't believe this coercion is the root cause of the bug (and I explain why in more detail in the Appendix), but we still need to understand coercion to understand the bug.

The solution

The real root of the problem is Grace's hacky solution for inferring the type of a list. It doesn't make sense to treat the type of the first element as the authoritative type for the entire list.

What I ended up doing was adding a new operation for the purpose of correctly inferring the type of the whole list. This new operation computes the most-specific supertype (a.k.a. least upper bound) of two types, defined like this:

C is a supertype of A and B if C is a supertype of A and a supertype of B. C is a most-specific supertype of A and B if C is a subtype of all other supertypes of A and B.

With this operation in hand, we can now infer the type of a list like this:

• infer the type of each element in the list
• compute the most-specific supertype of all of the element types
• check each element in the list against the most-specific supertype
• return the most-specific supertype as the list's overarching element type

If we do this the type checker now infers the correct type of a list like this one:

>>> :type [ { x: 1 }, { y: true } ]
List { x: Optional Natural, y: Optional Bool }

… because what happens is:

• the type checker infers that { x: 1 } has type { x: Natural }
• the type checker infers that { y: true } has type { y: Bool }
• their most-specific supertype is { x: Optional Natural, y: Optional Bool }
• each element is checked against that supertype

The reason we check each element against the supertype is so that each element is correctly elaborated (e.g. to fill in missing somes and nulls):

>>> [ { x: 1 }, { y: true } ]
[ { "x": some 1, "y": null }, { "y": some true, "x": null } ]

After this typechecking fix our original authorities list now has the correct inferred type and elaborated result:

>>> :type [ { domain: "google.com" }, { domain: "localhost", port: 8080 } ]
List { domain: Text, port: Optional Natural }

>>> [ { domain: "google.com" }, { domain: "localhost", port: 8080 } ]
[ { "domain": "google.com", "port": null }
, { "domain": "localhost", "port": some 8080 }
]

… and now our original example:

let authorities = [ { domain: "google.com" }
                  , { domain: "localhost", port: 8080 }
                  ]

for { domain, port = 443 } of authorities

in  "${domain}:${show port}"

… works and returns the expected result:

[ "google.com:443", "localhost:8080" ]

Yeah!

Conclusion

One of the reasons I push hard on bidirectional typechecking is that, despite its complexity, it's the only typechecking framework I've come across that's powerful enough to infer the types of real world JSON. Most simpler typechecking frameworks (like Hindley-Milner inference or similar) stumble on the sort of JSON data that you find in the wild.

I didn't create Grace to be an ergonomic language for working with JSON, but I also didn't ignore JSON support either. My prior experience as the author of Dhall taught me that language users are very passionate¹ about ergonomic JSON interop so I designed Grace's syntax and type system to both be mindful of JSON compatibility, even if it meant increasing the implementation complexity.

If you liked this post you might also like these other posts of mine:

• Datatype unification using Monoids

  This describes a simple algorithm for inferring the type of plain data that is essentially the same algorithm I use to compute the most-specific supertype in Grace.

• The appeal of bidirectional typechecking

  I mentioned this earlier, but this post explains why it's worth learning more about bidirectional typechecking, especially if you plan to implement a language that uses subtyping in some form.

Also, I highly recommend this paper:

• Local Type Inference

  This is one of the pioneering papers behind bidirectional type-checking and is also where I learned some of the above techniques, like least upper bounds and elaborating expressions to an internal language.

Appendix: record coercion

To explain why Grace coerces records to match their supertype, consider this contrived Grace expression:

let f (input: { }) = input.x

in  f { x: 1 }

Should this expression typecheck? If so, what type would we expect the function f to return?

The type should definitely not be Natural:

let f (record: { }): Natural = record.x  # WRONG: type error

in  f { x: 1 }

… because there is no way that a function (f) given an empty record as input can extract a Natural number from that record. It is true that the function f happens to be called on a record that has a field named x, but that function needs to work for any input of type { }, not just the one record we happened to call it on.

Perhaps the typechecker should reject the function f? After all, the function is attempting to access a field which does not exist on the declared input type. Rejecting the access is a sound choice, but then you lose support for other language features we need for operating on real-world JSON data. For example, consider our original example:

let authorities = [ { domain: "google.com" }
                  , { domain: "localhost", port: 8080 }
                  ]

for { domain, port = 443 } of authorities

in  "${domain}:${show port}"

That example is essentially syntax sugar for this equivalent expression:

let authorities = [ { domain: "google.com" }
                  , { domain: "localhost", port: 8080 }
                  ]

for authority of authorities

let default = fold{ some port: port, null: 443 }

in  "${authority.domain}:${show (default authority.port)}"

… so if we were to reject field accesses on missing fields then we wouldn't be able to bind or default potentially absent fields.

As far as I can tell, the only well-behaved design choice that gracefully handles real JSON data is:

• return null if the field is absent
• type the access as forall (a: Type) . Optional a (a type only inhabited by null)

However, if you do this then you must necessarily coerce records to strip fields not present in their supertype. If you don't strip those extra fields then the original contrived example:

let f (input: { }) = input.x

in  f { x: 1 }

… would return 1 : forall (a: Type) . Optional a, which is already problematic because that's an ill-typed expression (only null should ever have that type). However, such an ill-typed expression also lets you break the evaluator, like this:

let f (input: { }) = input.x  # Inferred type: forall (a: Type). Optional a

let default (input: Optional Text) = fold{ some text: text, "" }

in  "${default (f { x: 1 })}!"  # Runtime error if `f` returns `1`

So explicitly coercing records to match their supertype is (in my opinion) the only reasonable behavior when working with real JSON data. In my view, the actual bug was not the coercion, but rather the old hacky solution for inferring the type of a List.

1. … to say the least ↩