patternCritical
What can Idris not do by giving up Turing completeness?
Viewed 0 times
idriscanwhatcompletenessturingnotgiving
Problem
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.
I guess this is quite a specific question, but I don't know a huge amount about dependent types and related type systems.
Solution
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.
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.
Context
StackExchange Computer Science Q#19577, answer score: 58
Revisions (0)
No revisions yet.