What can Idris not do by giving up Turing completeness?

Question

I know that Idris has dependent types but isn't turing complete. What can it not do by giving up Turing completeness, and is this related to having dependent types?

I guess this is quite a specific question, but I don't know a huge amount about dependent types and related type systems.

Answer 1

Idris is Turing Complete! It does check for totality (termination when programming with data, productivity when programming with codata) but doesn't require that everything is total.

Interestingly, having data and codata is enough to model Turing Completeness since you can write a monad for partial functions. I did this, years ago, in Coq - it's probably bitrotted by now but here it is nevertheless: http://eb.host.cs.st-andrews.ac.uk/Partial/partial.v.

You do need one escape to actually run such things, but Idris allows you to do that.

Idris won't reduce partial functions at the type level, in order to keep type checking decidable. Also, only total programs can reasonably be believed as proofs.

Answer 2

First, I assume you've already heard of the Church-Turing thesis, which states that anything we call “computation” is something that can be done with a Turing machine (or any of the many other equivalent models). So a Turing-complete language is one in which any computation can be expressed. Conversely, a Turing-incomplete language is one in which there is some computation that cannot be expressed.

Ok, that wasn't very informative. Let me give an example. There is one thing you cannot do in any Turing-incomplete language: you can't write a Turing machine simulator (otherwise you could encode any computation on the simulated Turing machine).

Ok, that still wasn't very informative. the real question is, what useful program cannot be written in a Turing-incomplete language? Well, nobody has come up with a definition of “useful program” that includes all the programs someone somewhere has written for a useful purpose, and that doesn't include all Turing machine computations. So designing a Turing-incomplete language in which you can write all useful programs is still a very long-term research goal.

Now there are several very different kinds of Turing-incomplete languages out there, and they differ in what they can't do. However there is a common theme: Turing-complete languages must include some way to conditionally terminate or keep going for a time that is not bounded by the program size, and a way for the program to use an amount of memory that depends on the input. Concretely, most imperative programming languages provide these abilities through while loops and dynamic memory allocation respectively. Most functional programming languages provide these abilities through recursion and data structure nesting.

Idris is strongly inspired by Agda. Agda is a language designed for proving theorems. Now proving theorems and running programs are very closely related, so you can write programs in Agda just like you prove a theorem. Intuitively, a proof of the theorem “A implies B” is a function that takes a proof of theorem A as an argument and returns a proof of theorem B.

Since the goal of the system is to prove theorems, you can't let the programmer write arbitrary functions. Imagine the language allowed you to write a silly recursive function that just called itself:

oops : A -> B
oops x = oops x

You can't let the existence of such a function convince you that A implies B, or else you would be able to prove anything and not just true theorems! So Agda (and similar theorem provers) forbid arbitrary recursion. When you write a recursive function, you must prove that it always terminates, so that whenever you run it on a proof of theorem A you know that it will construct a proof of theorem B.

The immediate practical limitation of Agda is that you cannot write arbitrary recursive functions. Since the system must be able to reject all non-terminating functions, the undecidability of the halting problem (or more generally Rice's theorem) ensures that there are terminating functions that are rejected as well. An added practical difficulty is that you have to help the system to prove that your function does terminate.

There is a lot of ongoing research on making proof systems more programming-language-like without compromising their guarantee that if you have a function from A to B, it's as good as a mathematical proof that A implies B. Extending the system to accept more terminating functions is one of the research topics. Other extension directions include coping with such “real-world” concerns as input/output and concurrency. Another challenge is to make these systems accessible to mere mortals (or perhaps convince mere mortals that they are in fact accessible).

I'm not familiar with Idris. It is a take on the challenges I just mentioned. As far as I understand from a cursory glance at the 2013 preprint, Idris is Turing-complete, but includes a totality checker. The totality checker verifies that every function annotated with the keyword total terminate. The language fragment that only contains Idris programs where every function is total is similar in expressive power to Arda (probably not an exact match due to differences in the type theory, but close enough that you wouldn't notice unless you deliberately tried).

For other examples of languages that are not Turing-complete in different ways, see What are the practical limitations of a non-turing complete language like Coq? (which this answer is to a large extend taken from).