What is Expressiveness in a Computer Language

[Chris Smith]

Chris F Clark <cfc at shell01.TheWorld.com> wrote:
> Chris Smith <cdsmith at twu.net> writes: 
> > I thought about this in the context of reading Anton's latest post to
> > me, but I'm just throwing out an idea. 
>  
> I wrote:
> > I think there is some sense of convergence here.
> 
> Apologies for following-up to my own post, but I forgot to describe
> the convergence.
> 
> The convergence is there is something more general that what type
> theorists talk about when discussing types.  Type theory is an
> abstraction and systemization of reasoning about types.  This more
> general reasoning doesn't need to be sound, it just needs to be based
> aound "types" and computations.

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.  Something becomes a 
type the instant someone conceives of a type system that uses it.  We 
could try to define a dynamic type system, as you seem to say, as a 
system that checks against only what can be known about some ideal type 
system that would be able to prove the program valid... but I 
immediately begin to wonder if it would ever be possible to prove that 
something is a dynamic type system for a general-purpose (Turing-
complete) language.

If you could define types for a dynamic type system in some stand-alone 
way, then this difficulty could be largely pushed out of the way, 
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.  So 
back to that problem again.

You also wrote:
> I consider any case where a program gives a function outside of its
> domain a "type error", because an ideal (but unacheivable) type system
> would have prevented it.  That does not make all errors, type errors,
> because if I give a program an input within its domain and it
> mis-computes the result, that is not a type error.

So what is the domain of a function?  (Heck, what is a function?  I'll 
neglect that by assuming that a function is just an expression; 
otherwise, this will get more complicated.)  I see three possible ways 
to look at a domain.

(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.)

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.)

Is that a fair description of where we are in defining types, then?

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