I think he meant the type ∀α. α → α. At least in Haskell, there is only one non-⊥ function of this type: id. Moreover, there is no non-⊥ value of the type ∀α.

I think he meant the type ∀α. α → α. At least in Haskell, there is only one non-⊥ function of this type: id. Moreover, there is no non-⊥ value of the type ∀α. α. There is a tool called Djinn which can actually provide functions of such sufficiently constrained types. Another example would be the type ∀α.∀β. (α, β) → α, which only contains fst. Even types that contain an infinite number of functions can have interesting constraints from polymorphism like this. For example, the type ∀α. [α] → [α] contains a whole bunch (for sufficiently infinite values of "whole bunch" :P) of different functions. However, you are guaranteed that the functions can only affect the structure of the list: the function cannot create or modify values of type α in the list. So the function reverse would have this type, but a function which added 1 to each element of the list could not. Moreover, a function of this type would always have to map [] to [].