Type theory is a unifying theory of program semantics. It is one among many, each of which is a facet of one whole. In particular, the theory of algebraic and coalgebraic data types is a unifying theory for computation that allows one to derive efficient algorithms automatically. It does not encompass all algorithms design by a long shot, it is actually quite niche, but as a coherent mathematical theory that gets to the essence of computation, it is very promising.

I highly recommend this book to anyone who has access to a library and is interested in seeing algorithms from the thousand-mile-high point of view: https://www.amazon.com/Algebra-Programming-Prentice-Hall-Int...

I suppose the point of my comment is that theoretical computer science is actually a field with a lot of unifying theories that approach computation in coherent ways. Applied computer science is much, much messier because it is interested in the particularities and flaws of real world computational models and getting practical results now, leaving explanations to come later.

There are unifying theories of inference for AI, but they don't really cover deep neural networks. There are a few tantalizing hints that deep learning is intimately related to profound concepts in physics (renormalization) and functional programming.

For a demonstration,

I recommend the "Going Deep" show episodes of Erik Meijer and Brian Beckman, http://channel9.msdn.com/search?term=erik+meijer+brian+beckm...

plus the book "Algebra of Programming" by Richard Bird, Oege de Moor http://www.amazon.com/Algebra-Programming-Prentice-Hall-Inte...