What is Expressiveness in a Computer Language

[Chris Uppal]

Andreas Rossberg wrote:
> Chris Uppal wrote:
> >
> > > > It's worth noting, too, that (in some sense) the type of an object
> > > > can change over time[*].
> > >
> > > No. Since a type expresses invariants, this is precisely what may
> > > *not* happen. If certain properties of an object may change then the
> > > type of
> > > the object has to reflect that possibility. Otherwise you cannot
> > > legitimately call it a type.
> >
> > Well, it seems to me that you are /assuming/ a notion of what kinds of
> > logic can be called type (theories), and I don't share your
> > assumptions.  No offence intended.
>
> OK, but can you point me to any literature on type theory that makes a
> different assumption?

'Fraid not.  (I'm not a type theorist -- for all I know there may be lots, but
my suspicion is that they are rare at best.)

But perhaps I shouldn't have used the word theory at all.  What I mean is that
there is one or more logic of type (informal or not -- probably informal) with
respect to which the object in question has changed it categorisation.   If no
existing type /theory/ (as devised by type theorists) can handle that case,
then that is a deficiency in the set of existing theories -- we need newer and
better ones.

But, as a sort of half-way, semi-formal, example: consider the type environment
in a Java runtime.  The JVM does formal type-checking of classfiles as it loads
them.  In most ways that checking is static -- it's treating the bytecode as
program text and doing a static analysis on it before allowing it to run (and
rejecting what it can't prove to be acceptable by its criteria).  However, it
isn't /entirely/ static because the collection of classes varies at runtime in
a (potentially) highly dynamic way.  So it can't really examine the "whole"
text of the program -- indeed there is no such thing.  So it ends up with a
hybrid static/dynamic type system -- it records any assumptions it had to make
in order to find a proof of the acceptability of the new code, and if (sometime
in the future) another class is proposed which violates those assumptions, then
that second class is rejected.


> > I see no reason,
> > even in practise, why a static analysis should not be able to see that
> > the set of acceptable operations (for some definition of acceptable)
> > for some object/value/variable can be different at different times in
> > the execution.
>
> Neither do I. But what is wrong with a mutable reference-to-union type,
> as I suggested? It expresses this perfectly well.

Maybe I misunderstood what you meant by union type.  I took it to mean that the
type analysis didn't "know" which of the two types was applicable, and so would
reject both (or maybe accept both ?).  E..g  if at instant A some object, obj,
was in a state where it to responds to #aMessage, but not #anotherMessage; and
at instant B it is in a state where it responds to #anotherMessage but not
#aMessage.  In my (internal and informal) type logic, make the following
judgements:

    In code which will be executed at instant A
        obj aMessage.                "type correct"
        obj anotherMessage.       "type incorrect"

    In code which will be executed at instant B
        obj aMessage.                 "type incorrect"
        obj anotherMessage.        "type correct"

I don't see how a logic with no temporal element can arrive at all four those
judgements, whatever it means by a union type.

    -- chris