What is Expressiveness in a Computer Language

[Chris Smith]

Chris F Clark <cfc at shell01.TheWorld.com> wrote:
> Do you reject that there could be something more general than what a 
> type theorist discusses?  Or do you reject calling such things a type?

I think that the correspondence partly in the wrong direction to 
describe it that way.  If someone were to stand up and say "every 
possible but of reasoning about program correctness or behavior is type 
reasoning", then I'd be happy to say that formal type systems are a 
subset of that kind of reasoning.  However, that's quite the statement 
to ask of anyone.  So far, everyone has wanted to say that there are 
some kinds of reasoning that are type reasoning and some that are not.  
If that is the case, then a formal type system is in that sense more 
general than this intuitive notion of type, since formal type systems 
are not limited to verifying any specific category of statements about 
program behavior (except, perhaps that they are intended to verify 
guarantees, not possibilities; I don't believe it would fit all 
definitions of formal types to try to verify that it is possible for a 
program to terminate, for example).

What I can't agree to is that what you propose is actually more general.  
It is more general in some ways, and more limited in others.  As such, 
the best you can say is that is analogous to formal types in some ways, 
but certainly not that it's a generalization of them.

> Let you write: 
> > because we could say that anything that checks types is a type system,
> > and then worry about verifying that it's a sound type system without
> > worrying about whether it's a subset of the perfect type system. 
>  
> I'm particularly interested if something unsound (and perhaps 
> ambiguous) could be called a type system.

Yes, although this is sort of a pedantic question in the first place, I 
believe that an unsound type system would still generally be called a 
type system in formal type theory.  However, I have to qualify that with 
a clarification of what is meant by unsound.  We mean that it DOES 
assign types to expressions, but that those types are either not 
sufficient to prove what we want about program behavior, or they are not 
consistent so that a program that was well typed may reduce to poorly 
typed program during its execution.  Obviously, such type systems don't 
prove anything at all, but they probably still count as type systems.

(I'll point out briefly that a typical, but not required, approach to 
type theory is to define program semantics so that the evaluator lacks 
even the rules to continue evaluating programs that are poorly typed or 
that don't have the property of interest.  Hence, you'll see statements 
like one earlier in this thread that part of type-soundness is a 
guarantee that the evaluation or semantics doesn't get stuck.  I 
actually think this is an unfortunate confusion of the model with the 
thing being modeled, and the actual requirement of interest is that the 
typing relation is defined so that all well-typed terms have the 
interesting property which we are trying to prove.  It is irrelevant 
whether the definition of the language semantics happens to contain 
rules that generalize to ill-typed programs or not.)

I suspect, though, that you mean something else by unsound.  I don't 
know what you mean, or whether it could be considered formally a type 
system.

> > 1. The domain is the set of inputs to that expression which are going to 
> > produce a correct result. 
> > 
> > 2. The domain is the set of inputs that I expected this expression to 
> > work with when I wrote it. 
> > 
> > 3. The domain is the set of inputs for which the expression has a 
> > defined result within the language semantics. 

> Actually, I like 2 quite well.  There is some set in my mind when I'm
> writing a particular expression.  It is likely an ill-defined set, but
> I don't notice that.  That set is exactly the "type".

I don't actually mind #2 when we're talking about types that exist in 
the programmer's mind.  I suspect that it may get some complaint along 
the lines that in the presence of type polymorphism, programmers don't 
need to be (perhaps rarely are) thinking of any specific set of values 
when they write code.  I would agree with that statement, but point out 
that I can define at least my informal kind of set by saying, for 
instance, "the set of all inputs on which X operations make sense".

I believe there is more of a concrete difference between #1 and #2 than 
you may realize.  If we restrict types to considering the domain of 
functions without regard to the context in which they are called, then 
there are plenty of inputs on which this function does its own job quite 
well, but a global analysis tool may be able to conclude that if that 
input has been passed in, then this program already beyond the 
possibility of producing a correct result.  #1 would, therefore, be a 
more global form of analysis than #2, rather than being merely a 
question of whether you are fallible or not.

> Expanding that a little.  I expect the language to catch type errors
> where I violate model 3.

So would I.  (Actually, that's another pesky question; if the language 
"catches" it, did the error even occur, or did the expression just gain 
a defined result such that domain #3 is indistinguishable from the set 
of all possible inputs.  I tend to agree with Chris Uppal, I suppose, 
that the latter is really the case, so that dynamic type systems in 
languages, if they are sound, prevent concept #3 from ever being in 
question.  But, of course, you don't think about it that way, which 
distinguishes 2 from 3.)

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