[TYPES] Types of expressions in dynamic languages: "un-typed" or "uni-typed"?

[Noam Zeilberger]

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.