What is Expressiveness in a Computer Language

[Chris F Clark]

Chris Smith <cdsmith at twu.net> writes: 
 
> Unfortunately, I have to again reject this idea.  There is no such
> restriction on type theory.  Rather, the word type is defined by type
> theorists to mean the things that they talk about. 
 
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?
 
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.  I definitely consider such 
things type systems.  However, I like my definitions very general and 
vague.  Your writing suggests the opposite preference.  To me if 
something works in an analogous way to how a known type system, I tend
to consider it a "type system".  That probably isn't going to be at 
all satisfactory to someone wanting a more rigorous definition. Of 
course, to my mind, the rigorous definitions are just an attempt to 
capture something that is already known informally and put it on a
more rational foundation.
 
> So what is the domain of a function?  (Heck, what is a function? 
...
> (I need a word here that implies something like a set, but I don't care 
> to verify the axioms of set theory.  I'm just going to use set.  Hope 
> that's okay.) 
 
Yes, I meant the typical HS algebra definition of domain, which is a 
set, same thing for function.  More rigorous definitions can be 
sustituted as necessary and appropriate.
 
> 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. 
> 
> So the problem, then, more clearly stated, is that we need something 
> stronger than #3 and weaker than #1, but #2 includes some psychological 
> nature that is problematic to me (though, admittedly, FAR less 
> problematic than the broader uses of psychology to date.) 
 
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 approximate
that set and it's relationships to other sets in my program with the
typing machinery of the language I am using.  That is the static (and
well-founded) type.  It is however, only an approximation to the ideal
"real" type.  If I could make that imaginary mental set concrete (and
well-defined), that would be exactly my concept of type.
 
Now, that overplays the conceptual power in my mind.  My mental image
is influenced by my knowledge of the semantics of the language and
also any implementations I may have used.  Thus, I will weaken 2 to be
closer to 3, because I don't expect a perfectly ideal type system,
just an approximation.  To the extent that I am aware of gotchas in
the language or a relavent implementation, I amy write extra code to
try and limit things to model 1.  Note that in my fallible mind, 1 and
2 are identical.  In my hubris, I expect that the extra checks I have
made have restricted my inputs to where model 3 and 1 coincide.

Expanding that a little.  I expect the language to catch type errors
where I violate model 3.  To the extent model 3 differs from model 1
and my code hasn't added extra checks to catch it, I have bugs
resulting from undetected type errors or perhaps modelling errors.  To
me they are type errors, because I expect that there is a typing
system that captures 1 for the program I am writing, even though I
know that that is not generally true.

As I reflect on this more, I really do like 2 in the sense that I
believe there is some abstract Platonic set that is an ideal type
(like 1) and that is what the type system is approximating.  to the
sense that languages approximate either 1 or 2, those facilites are
type facilities of a language.  That puts me very close to your
(rejected) definition of type as the well-defined semantics of the
language.  Except I think of types as the sets of values that the
language provides, so it isn't the entire semantics of the language,
just that part which divides values into discrete sets which are
approriate to different operations (and detect inaapropriate values).

-Chris