Conversation

Rob Rix‎
@rob_rix
but with higher-order unification, all of those holes are existentially-bound metavariables, and now you have to think about all of the in-scope variables they could depend on. so you can bind at the outside & type them as functions of local variables…
1
4
Rob Rix‎
@rob_rix
…or you can bind them locally, leaving their types alone, but then potentially have to move them outwards if you can’t solve them locally, moving them leftwards through the context and extending their type as you go to deal with each local at a time.
1
2
Rob Rix‎
@rob_rix
binding them at the outside is the most straightforward I guess, tho IIRC it gets Weird™ given that some of the context is typing some of the rest of the context, i.e. you’ll have kinds and types in there, and you have to make sure they don’t get permuted or it’s unsound.
1
2
Rob Rix‎
@rob_rix
e.g. `f` binds `a : ?` implicitly as well as `x : a`, so (now naming the meta ?k), you have ?k : Type, a : ?k, x : a
1
2
Rob Rix‎
@rob_rix
another bit that tripped me up for a long time was that my constraint solver is no longer just doing unification, it’s computing judgemental equality, and hence also normalization, evaluation under binders, etc. much larger scope.
1
2
Rob Rix‎
@rob_rix
and the rules for pattern unification—when it’s ok to solve metas, and why—are super non-obvious to me, even after reading Miller’s papers (and every other thing I could find written on the topic whatsoever for the past three years) I still have only the vaguest intuition.
1
3
Rob Rix‎
@rob_rix
there’s this super deep relationship between heterogeneous substitution, normalization by evaluation, pattern unification, &c., and much of it depends on the kind of dependently-typed language you’re designing; & the design space is vast & underdescribed.
1
4
Rob Rix‎
@rob_rix
e.g., the assertion repeated in a few places that “e.g. Reed’s typing modulo trick won’t cut it for ‘full-spectrum dependent types’” doesn’t really tell me anything about why, or even what the hell ‘full-spectrum dependent types’ is supposed to mean, and context merely hints.
2
4
Brendan Zabarauskas
@brendanzab
Ohh, this is all really helpful! Might take me a while to unpack - I haven't gone as deep as you, but it rings many bells from looking at
@andrasKovacs6
's elaboration-zoo a while back. It's super handy to have some of these problems stated explicitly in this way though!
2
2
Rob Rix‎
@rob_rix
glad I could help! and please feel free to dive deeper into any of this that you’d like, or anything you pick up as you go. I’m still very much novice in all of this; it’s proven one of the hardest nuts to crack that I’ve yet encountered in CS, which is saying rather a lot.
2
2
Show replies