So you'd have:
{
?A : Type,
op : [A, A] -> A,
}
Which could be sugar for:
{
?A : Type,
op : { ?0 : A, ?1 : A, default : A },
}
Conversation
And then something like this maybe:
{
add-int-magma : Magma.{A = Int} = {
op = [x, y] => x + y,
},
test-add-int : Int = add-int-magma.op.[1, 3],
}
2
1
This:
add-int-magma.op.[1, 3]
would elaborate to:
add-int-magma.op.{0 = 1, 1 = 3}.default
2
1
But this might break a bunch of nice stuff in the type system and might be a really ✨Bad✨ idea. 😅
2
2
Like I think generally it's considered good to have nice categorical models of your type systems, and alterations like this might break a bunch of that stuff? Or at least be a rather ad-hoc extension? All the category theory stuff is a bit mysterious to me though. 😰
1
Heh, don't know much about the sequent calculus - have only really messed around with natural deduction. Takes a long time to get my head around the judgements though - especially if they aren't presented in a syntax-directed style.
1
Yeah me too - I think sequent calculus can have multiple conclusions to the right of the turnstile? But I think there are deeper things than that - I've just never seen a side-by-side comparison. I think for whatever reason in PL research natural deduction is more popular?
2
I really don't understand the explanation here, which seems to try to distinguish it from natural deduction: ncatlab.org/nlab/show/sequ
1
has attempted to explain it to me in the past - something to do with in natural deduction you can make your proof tree get larger as you attempt to get to the leaves? So it's harder to know if you are going to finish or not? I might have got that wrong though. 😬
The most usual way to understand the difference, ime, is to call something "natural deduction" when it uses intro and elim rules, and "sequent calculus" when it uses only intro rules.
1
2
Typically sequent calculi allow you to introduce formulas in different locations, which is how you (roughly) get the effect of intro and elim.
1
1
Show replies