when will I learn not to use GADTs for anything involving syntax
Conversation
for me, the answer is no
1
1
Is your code on git? Would be curious to look
1
github.com/robrix/seq/blo
Not pictured is the current object of my frustration, evaluation of terms to values, which has to contend with the fact that variables can be of either polarity, and yet I really don't want to have four environments (-/+ * value/cont).
2
1
My advice is to never, ever use multiple environments. Instead use a single environment where each member has additional info (is this a positive/negative variable? a value/continuation?).
1
2
McBride and Atkey's QTT stuff merged the linear and unrestricted contexts to make dependently typed linearity less terrible (I think the issue was to do with when types might depend on linear things?). No clue if that applies here though.
(also aware that you're probably far more across this stuff than me, sorry 😅)
1
This is also the direction the Graded Types folks have gone in. I find it makes everything simpler - metatheory, implementation, datatypes. I would be interested to see an example where a unified context *isn't* simpler to deal with.
1
3
Show replies