What is Expressiveness in a Computer Language

[Chris Smith]

Joachim Durchholz <jo at durchholz.org> wrote:
> Sorry, I have to insist that it's not me who's stretching terms here.
> 
> All textbook definitions that I have seen define a type as the 
> set/operations/axioms triple I mentioned above.
> No mention of immutability, at least not in the definitions.

The immutability comes from the fact (perhaps implicit in these 
textbooks, or perhaps they are not really texts on formal type theory) 
that types are assigned to expressions, and the program is not likely to 
change as it executes.  Even such oddities as "self-modifying code" are 
generally formally modeled as a single program, which reduces to other 
programs as it evaluates just like everything else.  The original 
program doesn't change in the formal model.

Hence the common (and, I think, meaningless) distinction that has been 
made here: that static type systems assign types to expressions 
(sometimes I hear variables, which is limiting and not really correct), 
while dynamic type systems do so to values.  However, that falls apart 
when you understand what formal type systems mean by types.  What they 
mean, roughly, is "that label which we attach to an expressions 
according to fixed rules to help facilitate our proofs".  Since dynamic 
type systems don't do such proofs, I'm having trouble understanding what 
could possibly be meant by assigning types to values, unless we redefine 
type.  That's what I've been trying to do.  So far I've had only limited 
success, although there is definite potential in one post by Chris Uppal 
and another by Chris Clark (or maybe I'm just partial to other people 
named Chris).

-- 
Chris Smith - Lead Software Developer / Technical Trainer
MindIQ Corporation