Conversation

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.

Rob Rix‎

@rob_rix

Mar 30, 2020

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.

Rob Rix‎

@rob_rix

Mar 30, 2020

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.

Brendan Zabarauskas

@brendanzab

Mar 30, 2020

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!

Brendan Zabarauskas

@brendanzab

Mar 30, 2020

These would definitely trip up folks if they weren't careful, and I assume there's many people constantly tripping over the same thing.

Rob Rix‎

@rob_rix

Mar 30, 2020

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* :\

Brendan Zabarauskas

@brendanzab

Mar 30, 2020

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!