Types and Abstractions

I was talking to a friend the other day about what computation is. I mentioned how computation is basically "what a Turing Machine does", that it tries to formalize the intuitive notion of performing a calculation or proof (or any sequence of actions), and how there are a lot of systems that give rise to this phenomenon. In fact, computation is surprisingly easy to come by- we can get it out of a lot of substrates like machines, proof simplification (finding normal forms in certain logics), patterns in Conways game of life, rewriting strings of symbols in the various rewriting systems like universal grammars, and many more.

It is interesting to me that the substrate effect the way we can construct computations and the nature of the structures we construct, and yet there are underlying principals that unite the various systems of universal computation (systems equivalent to Turing Machines). There is always a way to have a computation blow up- nonterminal or the lack of a normal form for example- and there is never a way to tell when this will happen in the general case (if there is then there is no way to compute all things- the system give up being universal). This is not always such a bad thing, really, as it is interesting to work within more restricted systems with nice properties (strong normalization/guaranteed termination). This is analogous to what we do when we introduce layers of abstraction in programming- we introduce a layer of restrictions on the actions of the lower layer, simplifying its use but often removing some things that are useful. The point I want to make here is that type systems are essentially restrictions on untyped universes of structures (bits, lambda terms, machines, strings of symbols, etc) that describe computations (I'm only interested in computation here) in a way that is similar to abstracting over a lower level interface. We can impose rules on the structures and ensure certain properties, while at the same time losing some information and power from the lower layer.

This is a pretty unformed thought, but the point stands- type systems and abstraction seem essentially the same. It seems like the desire to expose all possible power of the lower layer is only possible if we break an abstraction, which is analogous to doing things like adding Y to a type system to get universal computation- we have to give up our clean abstraction and deal with the substrate directly with all its power and complexity. Resist the desire and lose power, give in and lose any nice property you could have gained (this is a simplification, but it is often true).