He means that it's impossible to write such a function from the natural numbers. It's possible for all finite types such as UInt in Swift. In general, you can

He means that it's impossible to write such a function from the natural numbers. It's possible for all finite types such as UInt in Swift. In general, you can do this exhaustive search with any "compact" type and there are a lot of compact types. In particular, the (total continuous) functions from a discrete (i.e. a type with decidable equality) into a compact type are compact. And as the article shows, the (total continuous) functions from a compact into a discrete type are discrete. Together with the observation that the type of natural numbers is discrete and that every finite type is compact and discrete already gives you infinitely many compact types to play with. One caveat with this whole work (which goes back to Martin Escardo by the way) is that this doesn't work with general recursion. E.g. in a language with general recursion you can write a program kleene : (nat -> bool) -> bool which computes the paths in the Kleene tree, where roughly "all total computable paths are terminating, but all uncomputable paths diverge". However, if you have a (total) language with, e.g., only structural recursion, everything works out and you can apply this epsilon operator to arbitrary programs.