Question
If a pure type system has a terminating proof language, can we have Type : Type
at the logic level without causing paradoxes (i.e., without causing ∀ (x : *) -> x
to be inhabited)?
Example
Suppose we take a pure type theory such as the Calculus of Constructions, restrict functions to be affine (at most 1 variable uses) and add constructs for stratified duplications - see here for details. That language - which we could call EACC (Elementary Affine Calculus of Constructions) has a normalizing untyped fragment. That is, the reduction of any term - even ill-typed ones - is guaranteed to terminate due to the reduction rules (and, in particular, the restriction that duplicated terms can not change their levels).
Type : Type
possible in an affine type theory?" is a better title? $\endgroup$Type : Type
possible. $\endgroup$