You are correct in the sense that the language isn't Turing complete to guarantee that the language is strongly terminating. The language being strongly terminating means that 1) there is a Normal Form for the type of an expression and 2) the number of steps to reach Normal Form is finite. All programs definable in Epigram have a normal form (i.e. result) and this normal form (result) is reachable in finite time. Therefore hanging and infinite loops are impossible.
However, these aspects are unrelated to the fact that Epigram is dependently typed. We could easily implement a Turing complete dependently typed language or implement a non-dependently typed language which is not Turing complete.
I'm not entirely sure what the problem is you are thinking of in thought 1. Could you elaborate?
However, these aspects are unrelated to the fact that Epigram is dependently typed. We could easily implement a Turing complete dependently typed language or implement a non-dependently typed language which is not Turing complete.
I'm not entirely sure what the problem is you are thinking of in thought 1. Could you elaborate?