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:
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