Do you think type theory has a role to play in providing the mathematics needed for Big Data? https://www.simonsfoundation.org/quanta/20131004-the-mathematical-shape-of-things-to-come/