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. 🤔
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
Show replies