Why? This was my also my understanding, you either have some inference (even if not everywhere), or absolutely none. What am I missing?
This Tweet is from a suspended account. Learn more
Conversation
This Tweet is from a suspended account. Learn more
2
1
This Tweet is from a suspended account. Learn more
Yeah, I was pretty surprised initially to see that Dhall required so many annotations - it seems like it could really benefit from having a synthesis mode in its type checker! I don't know if they have considered and rejected it for some reason though. 🤔
1
It has been considered and rejected on the grounds of "too hard to specify". But the next plan with Dhall is to make the spec machine verified, so that will no longer apply
1
Oh, what were the barriers here? Bidirectional type checking tends to be pretty simple when disentangled from constraint-based type inference!
1
Dhall has neither, it takes what is basically the easiest to specify approach, even if it's means lots of annotations (e.g., empty lists)
1
2
FWIW, this is how I'd do lists bidirectionally:
Γ ⊢ x₀ ⇐ A … Γ ⊢ xₙ ⇐ A
─────────────
Γ ⊢ [x₀, …, xₙ] ⇐ List A
This means you can pull type annotations down from the top. That said it doesn't help if you have a list on its own, in synthesis position.
1
1
But yeah, it's pretty close to the regular rules - you just need to annotate what mode the different rules are in. Granted, it does get more complicated if you want to have special cases, eg. synthesizing the type of a list if all the elements can be synthesized as well.
That rule would look something like this:
Γ ⊢ x₀ ⇒ A … Γ ⊢ xₙ ⇒ A
────────────
Γ ⊢ [x₀, …, xₙ] ⇒ List A