Lambda the Ultimate

Types are fundamental to both logic and computation:
* Types are fundamental to avoiding contradictions in logic. For example, proper use of types avoids all the known paradoxes. See Types in logic.
* Types are fundamental to computation. For example, in the Actor Model it is necessary to know the type of Actor in order to send it a message. See Types in computation.

The issue of types arose in another LtU discussion where it seemed tangential but since the topic is fundamental, it is worthy of discussion because there seems to be a great deal of confusion and controversy on the part of both theoreticians and practitioners.