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