by contrast, the judgement for a (strict) pair (written ⊗) works a little differently; we’ll look at the elim rule (for reasons that are unlikely to be obvious), with proof terms:
Γ ⊢ x : Y ⊗ Z Γ, y : Y, z : Z ⊢ b : C
----
Γ ⊢ case x of (y, z) -> b : C
Conversation
(cf existentialtype.wordpress.com/2012/08/25/pol for more details. I actually find the argument about polarity in relation to products a tiny bit weak since you could presumably push thunks into the context, but that would certainly not be minimal.)
1
1
Tbh I'm thinkin of going the other way - having a record-like syntax for functions - where functions always have named args. It might be a bit weird though!
2
Yeah that's kind of why I want to focus on using them for non-proof-assistant stuff. As an expressive programming system for working with types, terms, and modules in a unified language. but yeah there are indeed annoyances.
1
1
Been pretty excited with
and Harper's draft paper which addresses some of my terrors to do with trying to move around in this space (I think it'll still involve a lot of me bumbling around in the dark, but it's a big help)