I’m fairly certain they’re not suggesting you need to know type theory for ML, but that theorem provers should have more ML libraries. My wife does some ML as a postdoc at Stanford and I doubt she’d even know what type theory is.