Does anyone know why CC as a PTS is often given the rules:
ℛ = { (*,*,*), (*,□,□), (□,*,*), (□,□,□) }
But systems with universe levels often use the rules:
ℛ = { (𝒰_i, 𝒰_j, 𝒰_max(i,j)) | i, j ∈ ℕ }
(□,*,*) doesn't seems to follow the max(i,j) pattern? 🤔
Conversation
For more info: ncatlab.org/nlab/show/pure
• CC: Calculus of constructions (aka. λC)
• PTS: Pure Type System
(s1,s2,s3) is often abbreviated to (s1,s2), where s2 = s3. So I'm confused about the (□,*) rule of CC.
1
3
IIRC that’s F-style impredicativity. It doesn’t show up in the hierarchy because you can only do it once (else, IIUC, you can embed the inconsistent Systems U- or U).
Today, in Coq that’s restricted to (forall X: Prop. P): Prop (when P: Prop). CC is closer to impredicative Set.
1
2
Oh cool! Very interesting. So I'm wondering if it would be fine if I chose the rule (□,*,□) instead of (□,*,*). I don't want a full hierarchy of universes, but I don't want the impredicativity either.
1
2
I could never compute PTSs in my head. That rule looks odd, but if you’re truncating a sound PTS, the result should be type-safe (trivially) and might satisfy preservation (not so sure but I guess).
1
1
Yeah it does look a bit odd on it's own. And yeah, ℛ is always super mind-bending.
The idea is that it's kind of using the 'maximum sort' of the two input types as the sort of the pi type. It's as if we only had two universe levels: 0 and 1 (for * and □ respectively).
2
Hmm, so it seems like the paper I want to try implementing is does have the (□, *) rule… not sure how load bearing it is but it might pay to be careful!
Quote Tweet
“Singleton types here, singleton types there, singleton types everywhere” by Monnier and Haguenauer seems to be extremely close to what I've been after! Thanks @fancytypes for the pointer! twitter.com/fancytypes/sta
Show this thread
2
2
Also, as they hint, predicative CC alone is not so useful without adding inductives. Even impredicative CC can't prove induction on Church-encoded data, as the Cedille papers explain (->Fu-Stump 2014).
And that's why people mostly gave up on PTSes and use primitive inductives.
2
Does a PTS become a not-a-PTS when you add primitive inductives? Because I was going to be ok with doing that - in fact I already have one hard-coded in my rules. Or is it more that the original intention of PTSs that you'd be able to use church encodings for inductive stuff?
1
I guess both? The reusable metatheory of PTS wouldn't apply as-is, but with Church encodings that was probably not a big concern.
OTOH, PTSes can still be useful to study fragments of your system to *some* extent.
1
1
Replying to
Ahh gotcha, yeah that makes sense. Sadly I don't have the resources/expertise to invest in making proofs about metatheory. My thinking behind structuring it as PTS would be that it might at least provide some pointers to those coming after me – in the unlikely event they do.
Oh yeah, I'd also add that I really appreciate your insights into the limits of reusability of the metatheory – it's very helpful! Hopefully I can avoid making too much of a mess in the process - just feel a bit embarrassed about it at times! 😅
1