I'd agree with his definition and your point simultaneously. Type system with only 0-th order types are still useful for optimization and error capture, but hig

I'd agree with his definition and your point simultaneously. Type system with only 0-th order types are still useful for optimization and error capture, but higher order structures and higher order polymorphism are both incredibly useful and more powerful than 0-th order types.