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.
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."
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).
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
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.
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?
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.
icefox | 20 hours ago
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...
withoutboats | 3 hours ago
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.
pervognsen | 9 hours ago
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."
isuffix | 17 hours ago
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
portisn't missing, butOptional. 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.[OP] Gabriella439 | 14 hours ago
Short version is: because you don't really need to reject
f(it's an unnecessary restriction). The version where the invalid field access returnsnull : forall (a : Type) . Optional ais (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 handlingnullwill still fail with a type error).olliej | 8 hours ago
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
osa1 | 3 hours ago
Wow, that docs directory is a gold mine. Thanks for sharing.
olliej | 2 hours ago
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
pta2002 | an hour ago
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.
thunderseethe | 19 hours ago
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?
[OP] Gabriella439 | 19 hours ago
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:
… then Grace will infer this type for the expression:
thunderseethe | 18 hours ago
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?[OP] Gabriella439 | 14 hours ago
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.
thunderseethe | 13 hours ago
Thanks for explaining! That makes alot of sense.
[OP] Gabriella439 | 11 hours ago
You're welcome! ^^