A bidirectional typechecking puzzle
37 points by Gabriella439
37 points by Gabriella439
Congrats on turning the Complete And Easy paper into something that functions! And a good example of where bidi's greedy nature can cause subtle issues. (Not a knock against it, inference always has issues, the best you can do is decide which ones you want.) And also why, IMO, subtyping and type coercion are usually anti-features.
If you treat the data as a source of truth for the types, then you're really not going to be able to check if the data is malformed or not. You'll just get incorrect types when there's a mistake rather than an informative error, as demonstrated. Though now that I read again you're the creator of Dhall (<3) so you probably know more about this than me... Now that I think more, being able to take a bunch of data and generate a schema for it is interesting idea that deserves research. Just not sure I would call it "type checking", since types are kiiiiinda assumed to be prescriptive, not descriptive...
I don't think I really understand why you're not just rejecting f? It's accessing a field of a record that has a type which can never have that field, this is almost certainly a bug in the program that I'd want a type checker to tell me about.
I think it differs from the authority example because the type of port isn't missing, but Optional. I don't see how rejecting missing fields requires rejecting optional fields. In particular, you can also coerce { domain: "google.com" } to the value { domain: "google.com", port: null } since you're already coercing values based on types.
Short version is: because you don't really need to reject f (it's an unnecessary restriction). The version where the invalid field access returns null : forall (a : Type) . Optional a is (in my opinion) strictly better than the version that rejects the invalid field access. It permits more valid programs (like the desugared version) and still fails on ill-typed programs (e.g. a program which tries to use the accessed value without handling null will still fail with a type error).
The immediate thought that jumps to my mind is: row types solve this! I imagine you considered that already. Do row types fall over here because of how they interact with subtyping?
Grace has row types and row polymorphism! Grace calls rows "fields" but otherwise they're exactly the same.
In fact, the most-specific supertype algorithm takes row types into account.
For example, if you do something like:
\record0 record1 ->
let _ = record0.x
let _ = record1.y
in [ record0, record1 ]
… then Grace will infer this type for the expression:
forall (a : Type) .
forall (b : Type) .
forall (c : Fields) .
{ x: b, y: a, c } -> { y: a, x: b, c } -> List { x: b, y: a, c }
Neat! Given that, I would expect our inference of { domain: String } to leave an open row variable as { domain: String, c }. And then subtype against { domain: String, port: Option } to give us { domain: String, port: Option, d } with c being { port: Option, d }. Where does that break?
You don't want to assert any element type in the list is a subtype of any other element type in the list, because once you add directionality to the relationship between two element types it will break on an example like [ { x: some 1, y: 1 }, { x: 1, y: some 1 } ]. Using your approach the two inferred element types would be { x: Optional Natural, y: Natural, a } and { x: Natural, y: Optional Natural, b } and neither of those two types is a subtype of one another (even with the addition of the unsolved row variables).
The only way to fix that is to make the supertype computation symmetric (meaning that neither of the two input types is treated as a supertype or subtype of the other type), but then if you do that you reinvent the most-specific supertype solution I mentioned in the post, which works with or without the unsolved row type variable. However, it's faster and simpler without the introduction of extra unsolved row type variables so that's why I don't introduce them.