There are a lot of typing paradigms running around these days without clear definitions. One of the difficulties is that any given phrase carries a number of different meanings, including (but not necessarily limited to) the phrase's apparent meaning from its constituent words, the phrase's common usage in any one of a number of different communities, the originator's intended meaning of the phrase, the original intended application domain of the paradigm, or the subsequent historical application domain of the paradigm.
Here's what I tend to mean by the following phrases. Disclaimer: I try to keep a balance between the aforementioned categories of meaning, although my community's common usage generally takes precedence. In any case there's a lot of vagueness and variability in the terminology, not to mention controversy. Read this at your own risk.
static typing: systems for reasoning about and enforcing inherent language invariants algorithmically and without involving program evaluation. In order to guarantee the invariants, the runtime semantics is only allowed to evaluate statically well-typed programs.
dynamic typing: systems for enforcing inherent language invariants incrementally during program evaluation via runtime checks.
soft typing: systems for detecting possible violations of imposed (i.e., not inherent) language invariants algorithmically and without involving program evaluation. The runtime semantics does not depend on programs being well-typed according to the soft typing algorithm.
optional typing: systems for detecting possible violations of imposed language invariants algorithmically and without involving program evaluation. The runtime semantics does not depend on program being well-typed according to the optional typing algorithm. (Come to think of it, I can't come up with a distinction between soft typing and optional typing off-hand.)
pluggable typing: systems of optional typing that admit any number of different static checking algorithms.
hybrid typing: systems for enforcing inherent language invariants algorithmically both via static reasoning and dynamic checks. This paradigm was originally introduced as a way to combine the static guarantees of statically typed languages with the more expressive annotation languages of dynamic contract systems.
gradual typing: systems for enforcing inherent language invariants algorithmically both via static reasoning and dynamic checks. This paradigm was originally introduced to facilitate program evolution by permitting incremental annotation of programs.
strong/weak typing: your guess is as good as mine.
8 comments:
strong/weak typing: your guess is as good as mine.
Hahah yea there seems to be no end to the political discussions around strong/weak typing ;) I think we just get rid of those words instead of more holy wars.
Here is one of those articles
http://blog.tmorris.net/strong-type-systems/
No one argument is likely to change my opinion of those terms; they've simply been used to mean too many things in too many different contexts. They're pretty much hopeless. It's not something wrong with the phrases per se, just the fact that they've been polluted by such a long history of mutually incompatible definitions.
I've always known strong typing to mean a type system which cannot be circumvented via casting or otherwise worked around (intentionally or not). Most everything nowadays is strongly typed. C would be weakly typed. Sometimes people thing weak to mean dynamic and strong to mean static, but, well, they're wrong!
The biggest difference is the thing that actually has a type. In Lisp for example it's an property of the value, whereas in Java it's a property of the variable/pointer.
I personally prefer that the value has an type.
John: what you're getting at is probably closer to the notion of safety, meaning, a language which protects its abstractions.
(As a side note, most of these definitions can be circumvented by not guaranteeing anything: even C protects its abstractions if you consider its only guarantee to be the integrity of the single datatype of bits. Similarly, you could claim Scheme is statically typed by considering its type system to be a very simple one: the Scheme "static type checker" rejects ill-formed S-expressions and programs containing free variables.)
Still, "strong" typing is so overloaded in different contexts, and generally in a way that has a more precise term that's preferable. I believe "safety" is a better term for what you're talking about, meaning "a language that protects its abstractions." In the case of static type systems, it means type soundness.
gmlk: this is a pretty common but very basic misunderstanding of type systems. The guarantee provided by a static type system has to be stronger than a guarantee on variables, because it must ensure that all compound expressions are well-typed, not just variable references. I recommend reading TAPL to get an introduction to the subject.
A couple nitpicks -
I think it's wrong to say that the fact that (car 5) is an error is an imposed invariant. In my mind, it's just as inherent as the invariant that you can't do 'hd 5'. Therefore, I would say that soft typing is, like static typing, checking inherent invariants. (Phillipe's work also checks imposed invariants, but that isn't usually called soft typing.)
Also, for most meanings of the word "Scheme", free variables aren't rejected.
samth: I agree the words "inherent" and "imposed" are suboptimal. I didn't mean to suggest a value judgment. I was trying to get at the idea that the runtime semantics of ML relies on the type checker guaranteeing that you'll never take the head of 5, which preserves an invariant of the system that you can't ever perform that ill-defined operation, whereas the runtime semantics of Scheme does not rely on a soft type checker running, so it must perform a runtime check to preserve the invariant that you can't ever perform that ill-defined operation.
So it's an "inherent" invariant in both ML and Scheme (in the sense that it's guaranteed by the runtime semantics) that the actual ill-defined operation of taking the head of 5 is never performed; it's an "imposed" invariant in Scheme with a soft type checker that you'll never execute code that attempts to take the head of 5 and gets a runtime error.
Re: free variables, fair enough. I am not particularly knowledgeable about the Scheme standard. In mzscheme it's a static error to have a free variable in a module, so let's just assume that's what I was talking about.
Post a Comment