What can Idris not do by giving up Turing completeness?

Problem Detail: 

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.

Asked By : Squidly

Answered By : Edwin Brady

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.

Best Answer from StackOverflow

Question Source : http://cs.stackexchange.com/questions/19577