Most dependent type theories aim for some notion of correctness in two respects:
- The type system must be decidable.
- The type system must be consistent. e.g. $\forall \tau. \tau$ should not be provable.
The first is a topic that has been debated a bit. You could relax this requirement to semi-decidability. The second has not been debated as a desirable property but many have mentioned that $Type : Type$ would be useful for "practical" programming languages. I've become interested in what such a "practical" programming language might look like. In this question, I'll use "practical" to mean "computationally complete and not directly intended to be used for any kind of proof". The debate over whether that is a fitting definition is another topic. For instance the calculus of constructions equipped with a fixed pointer operator of type $\Pi A : Type. (A \to A) \to A$ would qualify as such a "practical" programming language. Such a language would be inconsistent but would (I think) still be type safe and computationally complete.
Additionally, most type systems have a third property, generally called "type safety." This property ensures that well-typed programs "don't get stuck" (not sure who I got that quote from). In actual practice, there is generally a way to violate type safety but I'll include in my definiton of "practical" that the language must be type safe. For such "practical" programming languages consistency is generally moot, but type safety is still a desirable property and the main property trying to be achieved in systems like System-F for instance. In such systems, the range of allowed well-typed terms is expanded as far as possible while type safety is still met. You can generally make these systems computationally complete by adding a fixed point term to the theory.
Dependent type theory almost completely blurs the line between types and terms. The remaining distinction between the two is just what types are just terms $\tau$ such that $\tau : \mathcal{U}$ where $\mathcal{U}$ is some distinguished term in the theory (or cumulative hierarchy or such). This uniformity is a very aesthetically pleasing property.
There is an analogue of fixed points over terms for types often just known as a fixed point type or $\mu$-type. Such types generally come with a "wrap" and "unwrap" terms to manipulate terms of these fixed point types. This diverges from the term level equivalent of fixed points. This, however, seems somewhat unavoidable as if you consider adding a fixed point term in a system with $Type : Type$ it doesn't actually let you make useful types like the natural numbers (but you can use it to make type familes like $Fin$ by recursion over non-type terms). The expected result there is just your type checker infinitely looping. As an example consider the type $fix \,\, Type \,\, (\lambda A : Type. 1 + A)$ as an attempt at defining the natural numbers. Unless there is some clever trick I'm missing it doesn't seem like this terminates or produces a useful type. The thought springs to my mind that if types were evaluated lazily somehow that this would be fine but I don't have a clear picture on how that should work.
Are there any works that consider semi-decidable type systems that have $Type : Type$ and allow for fixed point types to be used? Can fixed point terms and fixed point types be unified? How would one account for least and greatest fixed points of types in such a case? In a nutshell is there any literature on type safe "practical" programming languages? Ideally I'd like to see this in the case of $Type : Type$
