In article <r8t4td14mfc.fsf@nordica.CS.Princeton.EDU>,
>This is my definition of a type system. I should be shot for forgetting some
>people have very different ideas of what a type system is.
Umm. Like everyone else who has ever studied programming languages?
>decidable** typing is what make "type systems" a win as it catches errors at
>compile time rather than at runtime.
It also "catches" correct code and says: "you can't do that." I'm not going to
get into an argument about which is better: I use both. But clearly runtime
typing is also "a win". Compare programming in a language with neither
static nor runtime type checking to one with either. Types are important
whenever they are checked.
I also wonder: what language do you program in that has completely statically
decidable type checking? I don't know of many modern languages that do not
allow you to cast up and down the class hierarchy, at least. Yes, I know
that such languages exist, but from your comment above I do not think that
you are using something like ML. In other words, most languages allow you
to do away with static type checking if you want to. Most Lisps will allow
you to add it if you want it.