You don't need infinite loops, all you need are simple inductive types and reduction rules, it has not to be a turing complete language. You can have simple typ

You don't need infinite loops, all you need are simple inductive types and reduction rules, it has not to be a turing complete language. You can have simple typelevel functions in haskell, whilst its typechecker is not turing-complete.