It's generally dangerous to allow non-terminating computation into your types since it means you can no longer trust the logic of your type system (Turing compl

It's generally dangerous to allow non-terminating computation into your types since it means you can no longer trust the logic of your type system (Turing completeness implies logical inconsistency). One way to limit the completeness of a language is to replace fixed-point recursion (as is embodied in the Y combinator and all recursive languages which are complete) by induction/coinduction. These two concepts "divide general recursion in half" such that you can get a lot of work done without actually having completeness/inconsistency. Haskell for instance has induction via folds and coinduction via unfolds, but since we're allowed to "cross the streams" in folds and unfolds you end up with general recursion and inconsistency. Coq disallows stream crossing.