I found out about graded modalities earlier today, when i was reading the quantitative type theory paper and they mentioned qtt was a graded modality.
Conversation
Both granule and qtt both lack dependent types. Granule has type to kind promotion, and qtt has a sort of useless pi-type, but neither has full blown dependent types. Also, linear types are known to be incompatible with the pi type. I suspect gmtt is incompatible with mltt?
2
1
Also, QTT is full blown dependent types. Their calculus is indeed a minimal calculus, but it doesn't put any restriction, as far as I recall, on dependency. The difference between our work and theirs is that we track data usage in specifications, but they don't, and...
1
2
we use graded modalities.
1
2
I guess I must be confused. Here's the syntactic categories from the qtt paper. There are usages and precontexts. Then S, T, U are pretypes, and M, N, O are preterms. I don't see type variables defined for pretypes, so are variables not used on the type level?
3
Computational variables, `x`, can appear in the type `El(M)`, but it seems there isn't a `Type` universe, and so there is no polymorphism in this setting, which makes sense, as it would just add to the complexity of the paper.
1
Actually, I am wrong, I just saw `Set`. So a variable of type `Set` would be a type variable.
1
I think the hard part with QTT is in understanding how `El(M)` works, which is where the dependency comes in.
2
Some examples of dependency are given in Hofmann's paper, which the QTT paper is building upon. As far as I'm aware, distinguishing between types and expressions-coding-types is a common thing in metatheory, and also certain styles of TT-in-TT. tcs.ifi.lmu.de/mitarbeiter/ma
1
3
What advantages does this representation give? And might it be useful for implementations as well?
It avoids an ambiguity between `El((x : A) -> B)` and `(x : El(A)) -> El(B)` when defining the interpretation of the syntax -- if the `El` is slient, these correspond to two different typing derivations that you need to make sure have the same interpretation.
1
2
Show replies