Conversation

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
I actually kinda think there aren’t that many, cos the people who aren’t flying solo are probably grad students with clueful advisors. What I wouldn’t give for an actual *teacher* :\
1
6
Brendan Zabarauskas
@brendanzab
Yeah, going solo is _really_ hard going. Seems to take, like, ten times longer do get anywhere. At times like these I'm really thankful for twitter at the very least!
1
2
Show replies