Answers to other questions have explained that all Agda programs are terminating.
My understanding is that the termination of any valid Adga program is a requirement governed by Agda's advanced dependent type system. This strict requirement seems that it would eliminate many errors. However, it also seems the prohibition of non-terminating programs would prevent the language from being able to express some useful programs. A server, for example, is a program in which the possibility of non-termination is a critical aspect of it's function.
Is it possible to write a server in Agda? I figure it's possible to practically get around the non-termination restriction in this case by setting the server to eventually terminate in a billion years or something. But I'm wondering if there is some trick of the type system that can permit Agda to express some such non-terminating programs, perhaps only those which reach a static closed cycle of some sort. If not, then theoretically could such a trick ever be invented?
Without that possibility it seems the Agda concept is fundamentally limited in the set of useful programs it can express.
All Agda programs need to be total. Which means that:
Productivity means that any finite observation of the process needs to return an answer in a finite amount of time. A server will be a corecursive program offering the user a set of commands they can issue, returning a response in finite time and (if applicable) offering the next set of commands.