Conversation

for me, the answer is no

I'm messing around with a polarized sequent calculus thing and wanted to index (co)terms by polarity… just one bit of information! just the one! and I crashed headlong into a wall.

Zanzi

@tangled_zans

Is your code on git? Would be curious to look

seq/Polarized.hs at main · robrix/seq

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).

github.com

a µµ̃ calculus with pretty-printing and evaluating interpreters - seq/Polarized.hs at main · robrix/seq

rntz

@arntzenius

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?).

12:19 AM · Aug 3, 2022Twitter Web App

I mean, agreed, but the problem moves around, e.g. the variable is negative but the value at that index is positive. Resolvable, but still, ew. (Counter to what I just said, I pretty strongly prefer leaving Γ and Δ separate. Would love to know more about why you'd combine them!)

Brendan Zabarauskas

@brendanzab

Aug 3

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.

Replying to

and

(also aware that you're probably far more across this stuff than me, sorry 😅)

Replying to

and

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.