All Turing categories are unityped; that is, for a given Turing-complete language, there exists a Turing category whose objects are like the types of programs in that language, and among those objects is a Turing object, a universal representation of all of those programs which needs no other objects in order to compute. (Without loss of generality, assume only one Turing object; but, it is legal for a Turing category to have more than one.)

This fact completes Silva’s ironies quoted in the article. Quoting WP on type systems:

Static type checking for Turing-complete languages is inherently conservative. That is, if a type system is both sound (meaning that it rejects all incorrect programs) and decidable (meaning that it is possible to write an algorithm that determines whether a program is well-typed), then it must be incomplete (meaning there are correct programs, which are also rejected, even though they do not encounter runtime errors).

This is precisely because such systems are trying to assign subobjects of the Turing object to each program, and while every program is an element of the Turing object, the subobjects do not cleanly partition the Turing object and there are some programs which don’t seem to be elements of any subobject. In C++, for example, consider the following procedure:

int f(int x) { return f(x); }

This snippet might appear to have the type of functions from int to int, but I don’t actually know which function it is designating, and I doubt that it actually designates one. Similarly, in Haskell, I can define:

f x = f x

and the type system incorrectly guesses that it is a function from any type to any other type. This is the “inherently conservative” behavior of static type-checking.