What is Expressiveness in a Computer Language

[Chris Uppal]

Andreas Rossberg wrote:

> So what you are suggesting may be an interesting notion, but it's not
> what is called "type" in a technical sense. Overloading the same term
> for something different is not a good idea if you want to avoid
> confusion and misinterpretations.

Frivolous response: the word "type" has been in use in the general sense in
which I wish to use it for longer than that.  If theorists didn't want ordinary
people to abuse their technical terms they should invent their own words not
borrow other people's ;-)

Just for interest, here's one item from the OED's entry on "type" (noun):

    The general form, structure, or character distinguishing
    a particular kind, group, or class of beings or objects;
    hence transf. a pattern or model after which something is made.

And it has supporting quotes, here are the first and last:

1843 Mill Logic iv. ii. §3 (1856) II. 192
    When we see a creature resembling an animal, we
    compare it with our general conception of an animal;
    and if it agrees with that general conception, we include
    it in the class. The conception becomes the type of comparison.

1880 Mem. J. Legge vi. 76
    Every creature has a type, a peculiar character of its own.

Interestingly the first one is from:
    John Stuart Mill
    A System of Logic
(but it's not mathematical logic ;-).

OK, I admitted I was being frivolous.  But I really don't see why a type system
(as understood by type theorists) /must/ have no runtime element.  Just as I
wouldn't stop calling a type system a "type system" if it were designed to work
on incomplete information (only part of the program text is available for
analysis) and so could only make judgements of the form "if X then Y".


[JVM dynamic class loading]
> Incidentally, I know this scenario very well, because that's what I'm
> looking at in my thesis :-).

<grin/>


> All of this can easily be handled
> coherently with well-established type machinery and terminology.

I'd be interested to know more, but I suspect I wouldn't understand it :-(


> A type system states
> propositions about a program, a type assignment *is* a proposition. A
> proposition is either true or false (or undecidable), but it is so
> persistently, considered under the same context. So if you want a type
> system to capture temporal elements, then these must be part of a type
> itself. You can introduce types with implications like "in context A,
> this is T, in context B this is U". But the whole quoted part then is
> the type, and it is itself invariant over time.

But since the evolving type-attribution that I'm thinking of also includes time
as a static element (at each specific time there is a specific attribution of
types), the dynamic logic can also be viewed as invarient in time, since each
judgement is tagged with the moment(s) to which it applies.

But there we go.  I don't expect you to agree, and though I'll read any reply
with interest, I think I've now said all I have to say in this particular
subthread.

Cheers.

    -- chris