[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
Robert Harper" wrote: > The word "type" should be reserved for structural purposes, they codify the "comprehension principles" that constitute the language. Things like "duck types" are "refinements" or "predicates" that are descriptive of the (typed) programs that have a pre-determined operational meaning. The word "type" is definitely overloaded, but adapting from Reynolds [1], I prefer to distinguish these two uses as "intrinsic types" and "extrinsic types" respectively (or i-types and e-types for short). Historically you can find many examples of people using the word type to mean either i-type or e-type, so it is unrealistic to proscribe one or the other usage -- and personally, I really believe that the *tension* between these two perspectives is at the heart of type theory. I agree, though, that a lot of mental energy is wasted because people fail to resolve this linguistic ambiguity. Noam [1] see John C. Reynolds, "The meaning of types -- from intrinsic to extrinsic semantics", BRICS Report RS-00-32.
