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

[Uday S Reddy]

Prof. Robert Harper writes:

> 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.  So, of
> course, Python and its relatives are and always have been unityped.  Some
> also have refinements to express verification conditions.

I agree that there is something intuitive about the "structural" vs
"descriptive" distinction.  But, if you try to formalize it, you are very
likely to end up with the static vs dynamic distinction.

Almost all mathematicians define a category as consisting of a collection of
objects and a collection of arrows, with operations called "domain" and
"codomain" and say that two arrows <g, f> are "composable" if dom(g) =
cod(f).  So, is this "comosability" structural or descriptive?

[I myself don't define a category that way.  I say that you have a
collection of objects, and for every pair of objects A and B, a collection
Hom(A,B) of arrows from A to B.  Being a structuralist, you know exactly why
I do it that way.]

But does it matter one way or another?  All that matters is whether the type
abstractions are being respected, so that you don't compose the wrong
things and expect to get some sense out of it.  

Cheers,
Uday