What is Expressiveness in a Computer Language

[Chris Uppal]

Chris Smith wrote:

> > It would be interesting to see what a language designed specifically to
> > support user-defined, pluggable, and perhaps composable, type systems
> > would look like. [...]
>
> You mean in terms of a practical programming language?  If not, then
> lambda calculus is used in precisely this way for the static sense of
> types.

Good point.  I was actually thinking about what a practical language might look
like, but -- hell -- why not start with theory for once ? ;-)


> I think Marshall got this one right.  The two are accomplishing
> different things.  In one case (the dynamic case) I am safeguarding
> against negative consequences of the program behaving in certain non-
> sensical ways.  In the other (the static case) I am proving theorems
> about the impossibility of this non-sensical behavior ever happening.

And so conflating the two notions of type (-checking) as a kind of category
error ?  If so then I see what you mean, and it's a useful distinction, but am
unconvinced that it's /so/ helpful a perspective that I would want to exclude
other perspectives which /do/ see the two as more-or-less trivial variants on
the same underlying idea.

> I acknowledge those questions.  I believe they are valid.  I don't know
> the answers.  As an intuitive judgement call, I tend to think that
> knowing the correctness of these things is of considerable benefit to
> software development, because it means that I don't have as much to
> think about at any one point in time.  I can validly make more
> assumptions about my code and KNOW that they are correct.  I don't have
> to trace as many things back to their original source in a different
> module of code, or hunt down as much documentation.  I also, as a
> practical matter, get development tools that are more powerful.

Agreed that these are all positive benefits of static declarative (more or
less) type systems.

But then (slightly tongue-in-cheek) shouldn't you be agitating for Java's type
system to be stripped out (we hardly /need/ it since the JVM does latent typing
anyway), leaving the field free for more powerful or more specialised static
analysis ?


> (Whether it's possible to create the same for a dynamically typed
> language is a potentially interesting discussion; but as a practical
> matter, no matter what's possible, I still have better development tools
> for Java than for JavaScript when I do my job.)

Acknowledged.  Contrary-wise, I have better development tools in Smalltalk than
I ever expect to have in Java -- in part (only in part) because of the late
binding in Smalltalk and it's lack of insistence on declared types from an
arbitrarily chosen type system.


> On
> the other hand, I do like proving theorems, which means I am interested
> in type theory; if that type theory relates to programming, then that's
> great!  That's probably not the thing to say to ensure that my thoughts
> are relevant to the software development "industry", but it's
> nevertheless the truth.

Saying it will probably win you more friends in comp.lang.functional than it
looses in comp.lang.java.programmer ;-)

    -- chris