haskellocamlcoqagdadependent-type

Can a dependently typed language be Turing complete?


It seems as though dependently typed languages are often not Turing complete. Why can we not allow every function to have general recursion (which would make the language Turing complete), instead of only allowing a more restricted form of recursion?

Is something preventing creators of dependently typed languages from allowing all functions to be capable of general recursion?

For example:


Solution

  • What you have read is misinformation.

    You can see for instance in IO.Base that the Agda standard library ships with a combinator called forever that happily executes an IO action until the end of times (or, more likely, the IO action eventually decides to call either exitSuccess or exitFailure):

    forever : IO {a} ⊤ → IO {a} ⊤
    

    Of course you will not find a function fix : (A → A) → A but that is because the type has to be honest about the possibility of non-termination (just like types in Haskell have to be honest about the possibility of mutation, or input-output, or failure). To encapsulate such effects you typically use monads. Above we used the IO monad but there are other monads capturing the idea of non-termination, cf. McBride's Turing-Completeness Totally Free