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.
