[Solved]: Categorisation of type systems (strong/weak, dynamic/static)

Problem Detail: 

In short: how are type systems categorised in academic contexts; particularly, where can I find reputable sources that make the distinctions between different sorts of type system clear?

In a sense the difficulty with this question is not that I can't find an answer, but rather that I can find too many, and none stand out as correct. The background is I am attempting to improve an article on the Haskell wiki about typing, which currently claims the following distinctions:

• No typing: The language has no notion of types, or from a typed perspective: There is exactly one type in the language. Assembly language has only the type 'bit pattern', Rexx and Tk have only the type 'text', core MatLab has only the type 'complex-valued matrix'.
• Weak typing: There are only few distinguished types and maybe type synonyms for several types. E.g. C uses integer numbers for booleans, integers, characters, bit sets and enumerations.
• Strong typing: Fine grained set of types like in Ada, Wirthian languages (Pascal, Modula-2), Eiffel

This is entirely contrary to my personal perception, which was more along the lines of:

• Weak typing: Objects have types, but are implicitly converted to other types when the context demands it. For example, Perl, PHP and JavaScript are all languages in which "1" can be used in more or less any context that 1 can.
• Strong typing: Objects have types, and there are no implicit conversions (although overloading may be used to simulate them), so using an object in the wrong context is an error. In Python, indexing an array with a string or float throws a TypeError exception; in Haskell it will fail at compile time.

I asked for opinions on this from other people more experienced in the field than I am, and one gave this characterisation:

• Weak typing: Performing invalid operations on data is not controlled or rejected, but merely produces invalid/arbitrary results.
• Strong typing: Operations on data are only permitted if the data is compatible with the operation.

As I understand it, the first and last characterisations would call C weakly-typed, the second would call it strongly-typed. The first and second would call Perl and PHP weakly-typed, the third would call them strongly-typed. All three would describe Python as strongly-typed.

I think most people would tell me "well, there is no consensus, there is no accepted meaning of the terms". If those people are wrong, I'd be happy to hear about it, but if they are right, then how do CS researchers describe and compare type systems? What terminology can I use that is less problematic?

As a related question, I feel the dynamic/static distinction is often given in terms of "compile time" and "run time", which I find unsatisfactory given that whether or not a language is compiled is not so much a property of that language as its implementations. I feel there should be a purely-semantic description of dynamic versus static typing; something along the lines of "a static language is one in which every subexpression can be typed". I would appreciate any thoughts, particularly references, that bring clarity to this notion.

Asked By : Ben Millwood

Answered By : Uday Reddy

Historically, the term "strongly typed programming language" came into use in the 70's in reaction to the existing widely used programming languages, most of which had type holes. Some examples:

• In Fortran, there were things called "COMMON" storage areas, which could be shared across modules, but there were no checks to see if each module was declaring the contents of the COMMON storage with the same types. So, one module could declare that a particular COMMON storage block had an integer and another a floating point number, and the data would get corrupted as a result. Fortran also had "EQUIVALENCE" statements, whereby the same storage could be declared to contain two different objects of different types.

• In Algol 60, the type of procedure parameters was declared as just "procedure", without specifying the types of the parameters of the procedure. So, one could assume that a procedure parameter was an integer-accepting procedure, but pass in a real-accepting procedure as the argument. This would result in the same kind of corruption as the COMMON and EQUIVALENCE statements. (However, Algol 60 did eliminate the older problems.)

• In Pascal, "variant records" were added which were almost exactly like the old EQUIVALENCE statements.

• In C, "type casts" were added whereby any type of data could be reinterpreted as data of a different type. This was a rather deliberate type hole meant for programmers who supposedly know what they are doing.

The strongly typed languages designed in the 70's were meant to eliminate all such type holes. If you drill down into what this means, it means essentially that data representations are protected. It is not possible to view data object of one type as an object of another type which happens to have the same bit pattern as its internal representation. Theoreticians began to use the term "representation independence" to characterize this property instead of the vague idea of "strong typing".

Note that dynamically typed languages like Lisp which perform complete run-time type checking are "strongly typed" in the sense of protecting representations. At the same time, statically typed languages would lose representation independence unless they did array bounds checking. So, they are not "strongly typed" in the strict sense of the term. Due to these anomalous consequences, the term "strongly typed" fell into disuse after the 70's. When the US Department of Defence developed rigorous requirements for the design of Ada, they included the requirement that the language should be "strongly typed". (It seems to have been believed at that time that the idea of "strongly typed" was self-evident. No definition was offered.) All the language proposals submitted in response claimed to be "strongly typed". When Dijkstra analysed all the language proposals, he found that none of them were strongly typed and, in fact, it wasn't even clear what the term meant. See the report EWD663. However, I see that the term is coming back into use now, through a younger generation of researchers who don't know the checkered history of the term.

The term "statically typed" means that all type-checking is done statically and no type errors will arise at run-time. If the language is also strongly typed, that means that there are really no type errors during execution. If, on the other hand, there are type holes in the type system, the absence of run-time type errors means nothing. The results could be completely corrupt.

The new debate about "strong vs weak typing" seems to be about whether certain type conversions should be allowed. Allowing a string where an integer is required is "weak typing" according to these folks. There is some sense to that because attempting to convert a string to an integer may fail, if the string doesn't happen to represent an integer. However, converting an integer to a string doesn't have that problem. Would that be an instance of "weak typing" according to these folks? I have no idea. I notice that the Wikipedia discussions on "weak typing" don't cite any refereed publications. I don't believe that it is a coherent idea.

Note added: The basic point is that the term "strong typing" did not come into use as a technical term with a rigorous definition. It was more like some language designers felt: "our type system is strong; it catches all type errors; it doesn't have type holes" and, so, when they published their language design, they claimed that it was "strongly typed". It was a buzz word that sounded good and people started using it. The Cardelli-Wegner paper was the first one that I have seen where some analysis was provided into what it means. My post here should be thought of as an elaboration of their position.

Best Answer from StackOverflow

Question Source : http://cs.stackexchange.com/questions/2301