7
$\begingroup$

Most dependent type theories aim for some notion of correctness in two respects:

  1. The type system must be decidable.
  2. 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$

$\endgroup$
  • $\begingroup$ You can have fixed points without $\mathsf{Type} : \mathsf{Type}$. Ulrich Berger's habilitation has a domain-theoretic model of such a type theory. My gut feeling is that we cannot have decidable type checking for dependent types and fixed points at the same time because that would require decidable checking of equality of terms defined using fixed points (exercise!). So, one wonders how practical that would be. $\endgroup$ – Andrej Bauer Jun 26 '18 at 14:30
  • $\begingroup$ Right. My gut feeling was also we couldn't have decidable type checking which is why I mentioned semi-decidability. It's up to the programmer to ensure that no intractable terms are evaluated by modern type checkers already so requesting that no infinite terms be evaluated is a Small Step™ away from the current state of things. For instance CoC w/ fix is semi-decidable. I'm also aware that you can avoid $Type : Type$ but I'm interested not just in bolting on a fixed point term and fixed point type formers but in some unification of the two separate concepts. That seems to demand Type : Type $\endgroup$ – Jake Jun 26 '18 at 17:34
  • $\begingroup$ Here is a dependently typed language implemented with Type : Type, github.com/sweirich/pi-forall, however I don't thing there is a fixpoint construction $\endgroup$ – user833970 Jul 7 '18 at 2:49
5
$\begingroup$

I think the idea of unifying type and term-level fixpoints is natural, though I have to admit I'm not sure that reducing the number of constructions of a system is not always a recipe for conceptual simplicity.

One source I have for a system that takes this approach is the $\Pi\Sigma$ system:

$\Pi\Sigma$: Dependent Types Without the Sugar, Altenkirch, Danielsson, Löh and Oury.

You might also want to look at these slides by Khulmann on equi-recursive types versus iso-recursive types: equi-recursive types embody the kind of type-level recursion you are interested in (iso-recursive types have explicit folding and unfolding). As you suspect, type-checking with equi-recursive types is tougher (but not impossible!).

As a final remark, adding equi-recursive types to an otherwise consistent system does not make it inconsistent, if positivity constraints are respected.

$\endgroup$
  • $\begingroup$ Thanks! "equi-recursive" was a term I've somehow missed. Googeling it now it seems ubiquitous. Also "Dependent Types without Sugar" seems like a real instance of the vague lazy evaluation idea I had...though with iso-recursive types it would seem. $\endgroup$ – Jake Jul 9 '18 at 4:33
  • $\begingroup$ @Jake, yes, I think that iso-types use guards to control unfolding, which feels a lot like lazy evaluation of sorts. It seems type-checking with them (and general syntactic considerations) are much easier with iso rather than equi. $\endgroup$ – cody Jul 9 '18 at 12:24

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.