34
$\begingroup$

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.

$\endgroup$
  • 2
    $\begingroup$ I guess you are looking for a concrete example? I'm not familiar with Idris, but in Isabelle/HOL you can't write (or rather, compile) functions that don't always terminate (worse, you need to give a termination proof). $\endgroup$ – Raphael Jan 8 '14 at 10:32
  • $\begingroup$ Something along these lines yeah - I wasn't entirely sure if there would be something quite niche case like you can't encode a language with certain properties in the type system, or whether it would be a bit more general (e.g. as you said, all functions must be proven to terminate) $\endgroup$ – Squidly Jan 8 '14 at 10:55
  • 1
    $\begingroup$ Guess this mis-assumption comes from Edwin Brady saying that Idris is "Pacman complete". I think his main point by saying "Pacman complete" instead of "Turing complete", is that he wants to underline the importance of languages being easily compile-able by human brains and not only machines!.. silly languages such as BrainFuck is surely Turing complete, but it can take a human brain quite a while to comprehend code written in BrainFuck, thus developing, and even more important maintaining, a Pacman program in BrainFuck takes quite an effort.. $\endgroup$ – Michelrandahl Jan 10 '16 at 10:12
  • $\begingroup$ @Mitzh Not really. I think it's because I misunderstood something I heard him say in a talk. $\endgroup$ – Squidly Jan 11 '16 at 13:22
48
$\begingroup$

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.

$\endgroup$
  • 4
    $\begingroup$ The man himself. What is productivity in this context? $\endgroup$ – Squidly Apr 22 '14 at 9:44
  • 5
    $\begingroup$ Dual to termination: while an inductive definition must terminate (by consuming all of its data) a coinductive definition must be productive - in practice this means, brieflt, that any recursive call must be guarded by a constructor. I've found this explanation to be the clearest (ymmv): adam.chlipala.net/cpdt/html/Coinductive.html $\endgroup$ – Edwin Brady Apr 22 '14 at 17:58
13
$\begingroup$

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).

$\endgroup$
  • 3
    $\begingroup$ "what useful program cannot be written in a Turing-incomplete language?" A Java virtual machine. $\endgroup$ – David Richerby Jan 8 '14 at 21:48
  • $\begingroup$ @DavidRicherby Can't you? Is the JVM really Turing-complete? There's a limit on the size of an individual object, can you arrange to allocate and access an unbounded number of object? For example, in C, the answer seems to be no because there are only finitely many pointer values. $\endgroup$ – Gilles Jan 8 '14 at 21:52
  • $\begingroup$ For readers interested in that part, we have another post about why there can not be programming language for exactly the always terminating languages. $\endgroup$ – Raphael Jan 8 '14 at 22:31
  • 3
    $\begingroup$ @Gilles I take your point but isn't it more or less equivalent to saying that no actual programming language is Turing-complete? After all, any implementation is going to run into the kind of barriers you mention. That seems like quite a large elephant to have in the room while considering what Idris loses by not being Turing-complete. Does it lose more than any other language, for example? If you forbid unbounded external storage (e.g., the program stopping to say "please insert next/previous disk") then any language is trivially not Turing-complete so any question about that case is vacuous. $\endgroup$ – David Richerby Jan 9 '14 at 13:16
  • 3
    $\begingroup$ @DavidRicherby My comments (but not my answer) are in programming language theory geek mode. If you take the formal specification of SML (for example), it is possible to design (but of course not implement in the physical world) an implementation of the language that can simulate all computable programs. This is not so in C, because the finiteness of memory is built into the language (sizeof(void*)). In my answer, I treat languages in an idealized way, so SML or C would be considered Turing-complete. $\endgroup$ – Gilles Jan 9 '14 at 17:35

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.