Actually, since computers are turing complete, perhaps it's more like 'computers are naturally recursively typed' and there is an analogous impossibility theorem for encoding some coinductive type in the same way? Perhaps I just don't understanding enough yet.