Coroutine, as a powerful programming construct, is widely used in asynchronous applications to replace thread-based programming or the callback hell. Using coroutines makes code more readable and maintainable, for its ability to transfer control while keeping the literal scope. However, reasoning about coroutine behavior can be challenging without proper typing. We propose a type notation and calculus for composing asymmetric, first-class, stackless coroutines. Given the types of a list of coroutines, we can compute a composed type matching the collective behavior of the coroutines, so that the input and output can be type-checked by a type system. Our coroutine types can model the data received by or yielded from a coroutine, which be of coroutine types as well. On top of our type calculus, we discuss its soundness and evaluation issues, then provide four application scenarios of our coroutine types. Not only can our types be used in modern programming languages, such as Python, but also model program behaviors in OCaml and even Prolog.

翻译：协程作为一种强大的编程构造，被广泛应用于异步应用中，以取代基于线程的编程或回调地狱。协程能够在保持字面作用域的同时转移控制权，从而使代码更具可读性和可维护性。然而，若无恰当的类型标注，对协程行为的推理将颇具挑战。我们提出了一种用于组合非对称、一等公民、无栈协程的类型表示法与演算系统。给定一组协程的类型，我们可以计算出与该协程集体行为匹配的组合类型，从而使得输入和输出能够通过类型系统进行类型检查。我们的协程类型能够对协程接收或产出的数据进行建模，这些数据本身也可以属于协程类型。基于我们的类型演算，我们讨论了其健全性与评估问题，并提供了协程类型的四种应用场景。我们的类型不仅可应用于现代编程语言（如Python），还能对OCaml乃至Prolog中的程序行为进行建模。