A bidirectional typechecking puzzle
54 points by Gabriella439
54 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...
You’ve suggested you’re making an argument for principle types but seem to have made an argument against type inference in general. But I doubt you think it’s wrong that the type of “true” is inferred from the expression.
The design question here is nuanced and there are a spectrum of valid answers. I think full inference is problematic for the reason you described, but full checking is also obviously irksome, so there is some middle ground you have to land on.
In regard to principle types I think it’s fine to give them up but you need to be careful, as the author here is, that the additional context produces a monotonic result, so you don’t get an error based only on the order of evaluation. Dunfield-Krishnaswami manage to sidestep the issue by restricting the set of language features but if you want record subtyping you need to change the algorithm.
Yeah I was half-assedly trying to describe principle types, thank you. "I know what the type has to be from looking at one expression" vs "I build up a picture of the type by looking at multiple disjoint expressions". You can make the latter work, like Rust's number types, but you have to be careful about how you do it, also like Rust's number types. But being able to take a bunch of half-assed dirty unstructured data, throw it into a program, and ask it to make me a schema that describes it? That sounds like a data scientist's dream. Copy-paste said schema, modify your copy to become what it should be, and you could almost generate a program to do validation and cleanup for you...
Isn't this an example of the "greedy instantiation" problem discussed in section 5.1.1 of the Bidirectional Typing paper?
"In its original setting [i.e. Cardelli's 1993 paper], this greedy method’s vulnerability to argument order was rather unfortunate. In a setting of predicative higher-rank polymorphism without other forms of subtyping [i.e. the Complete and Easy paper], however, it can work nicely. The “tabby-first problem” cannot arise because the only way a type can become strictly smaller is by being strictly more polymorphic, and if the first argument is polymorphic we would be instantiating 𝛼 with a polymorphic type, which would violate predicativity."
There is of course swift which has a bidirectional type inference (well part inference part constraint solving), with high kinded and higher ranked types, and class based inheritance and polymorphism, and almost all the features all the time :D
The core system is described here (there is an actual name for the system but I cannot for the life of me remember it): https://github.com/swiftlang/swift/blob/main/docs/TypeChecker.md
Note thtat swift also has the infamous "could not type check expression in reasonable time" problem, which is annoyingly common with SwiftUI, though thankfully the last updates seem to be getting a lot better at that.
Dammit, I'd swear I included a comment about it being formally undecidable (correctly "resolvable" by heuristics or something). I think I got so side tracked trying to remember the blasted name of the system I forgot to include that actually important bit :D
As for swiftui, I don't have much experience. For me the misery pit has always been lambdas type inference: oh you have a typo? well your expression (the entire lambda) is wrong, good luck!
Ah ha, I found it after a while. It's the knuth-bendix completion algorithm (https://en.wikipedia.org/wiki/Knuth–Bendix_completion_algorithm) and if you want to go all in on understanding and how it applies to swift you can read this 643 page document (684 including index, citations, and appendices) document: https://download.swift.org/docs/assets/generics.pdf
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.