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
--
http://mail.python.org/mailman/listinfo/python-list
