What is Expressiveness in a Computer Language

[Rob Thorpe]

Chris Smith wrote:
> Rob Thorpe <robert.thorpe at antenova.com> wrote:
> > A language is latently typed if a value has a property - called it's
> > type - attached to it, and given it's type it can only represent values
> > defined by a certain class.
>
> I'm assuming you mean "class" in the general sense, rather than in the
> sense of a specific construct of some subset of OO programming
> languages.

Yes.

> Now I define a class of values called "correct" values.  I define these
> to be those values for which my program will produce acceptable results.
> Clearly there is a defined class of such values: (1) they are
> immediately defined by the program's specification for those lines of
> code that produce output; (2) if they are defined for the values that
> result from any expression, then they are defined for the values that
> are used by that expression; and (3) for any value for which correctness
> is not defined by (1) or (2), we may define its "correct" values as the
> class of all possible values.

I'm not talking about correctness, I'm talking about typing.

>  Now, by your definition, any language
> which provides checking of that property of correctness for values is
> latently typed.

No, that isn't what I said.  What I said was:
"A language is latently typed if a value has a property - called it's
type - attached to it, and given it's type it can only represent values
defined by a certain class."

I said nothing about the values producing correct outputs, or being
correct inputs.  I only said that they have types.

What I mean is that each value in the language is defined by two peice
of information, its contents X and its type T.

>  Of course, there are no languages that assign this
> specific class of values; but ANY kind of correctness checking on values
> that a language does (if it's useful at all) is a subset of the perfect
> correctness checking system above.  Apparently, we should call all such
> systems "latent type systems".

No, I'm speaking about type checking not correctness.

>  Can you point out a language that is not
> latently typed?

Easy, any statically typed language is not latently typed.  Values have
no type associated with them, instead variables have types.

If I tell a C program to print out a string but give it a number it
will give an error telling me that the types mismatch where the
variable the number is held in is used to assign to a variable that
must hold a string.  Similarly if I have a lisp function that prints
out a string it will also fail when given a number, but it will fail at
a different point, it will fail when the type of the value is examined
and found to be incorrect.

> I'm not trying to poke holes in your definition for fun.  I am proposing
> that there is no fundamental distinction between the kinds of problems
> that are "type problems" and those that are not.  Types are not a class
> of problems; they are a class of solutions.

Exactly.  Which is why they are only tangentially associated with
correctness.
Typing is a set of rules put in place to aid correctness, but it is not
a system that attempts to create correctness itself.

>  Languages that solve
> problems in ways that don't assign types to variables are not typed
> languages, even if those same problems may have been originally solved
> by type systems.

Well, you can think of things that way.  But to the rest of the
computing world languages that don't assign types to variables but do
assign them to values are latently typed.

> > Untyped and type-free mean something else: they mean no type checking
> > is done.
>
> Hence, they don't exist, and the definitions being used here are rather
> pointless.

No they aren't, types of data exist even if there is no system in place
to check them.  Ask an assembly programmer whether his programs have
string and integers in them and he will probably tell you that they do.