Conversation

Arnaud Spiwack
@aspiwack
A fascinating thread. It kind of illustrate how PLT hasn't found a way, yet, to write systems which both express their idea clearly and yet are precise. To be fair, though, PLT is one of the communities with the highest standard for article-writing.
Quote Tweet
James Wilcox
@wilcoxjay
·
PL twitter: quick, what's the scariest screenshot you can find of a paper with an overwhelming amount of inference rules?
Show this thread
1
6
Arnaud Spiwack
@aspiwack
PLT articles tend to be divided in two movements: a clear explanation of the system's ideas, and a precise, comprehensive, description of the system. But it *is* sad that we can't seem to have the two be the one and the same. Looking forward to the time where this is solved.
1
5
James Wood
@laMudri
We write our typing rules in assembly language (sequent calculus) for the sake of brevity and immediacy. We should isolate the high-level concepts that make our systems work, write them down, and provide a compiler to sequent calculus. Natural deduction is a good start.
2
2
Arnaud Spiwack
@aspiwack
I don't find sequent calculus to be much lower level than natural deduction (all these systems are natural deduction). That being said, I don't disagree with the sentiment. But I don't have a solution either 🙂
1
3
James Wood
@laMudri
I should clarify: the distinction I'm making is about use of sequents vs use of hypothetical judgements, rather than the distinction between right/left vs intro/elim. If you see a ‘Γ’, the system has already been translated into a sequent calculus before being presented.
1
1
Arnaud Spiwack
@aspiwack
Ah, I see. It makes sense, the context is generally a distraction, and removing distraction increases clarity. This is one reason why we try to eliminate boilerplate in code. On the other hand, the rule for implication in such natural deduction style does my head in pretty bad.
2
2
Paolo G. Giarrusso
@Blaisorblade
I don't get ND either, and I'm unsure it's just habit. If Gamma were a problem, I'd thread it implicitly like martin-lof (only show added entries). I've considered using monads for threading other params, but I doubt they'd be an improvement, even if they were standard.
3
2