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
Replying to
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).
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
Well, that thread starts with extraction to F-omega, which is impredicative. And if you want to extract a predicative system to F/Haskell (like Agda... sort of does?), I’m gonna ask (off the top of my head) how do you figure out what becomes a kind?
1
1
Show replies
Replying to
I sort of see that, it just takes some inlining to compute conventional rules, which is hard when you lost the habit of using pen and paper (or virtual versions thereof).
1