What is Expressiveness in a Computer Language
Chris Smith
cdsmith at twu.net
Sat Jun 24 23:15:28 EDT 2006
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
More information about the Python-list
mailing list