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
One more concern: AFAIK the only _predicative_ type system around with only 2 levels is the SML type/module system — the module system has 2 universes, ditto the core system, and I'm now unsure if those align exactly — I hope not, else you couldn't use polytypes as type members!
1
1
Replying to
AFAIK I don't actually need to store polytypes in records/modules in the system in question! Just need polymorphic top level definitions.