23
$\begingroup$

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.

Improve this question
$\endgroup$
6
  • 6
    $\begingroup$ I think you already have your answer: there is no accepted definition of weak and strong typing. $\endgroup$
    – svick
    Commented Jun 9, 2012 at 18:22
  • $\begingroup$ I wouldn't find that hard to believe, but I ask the question in the hope that there is one I just haven't heard about :) or at least a definition more authoritative than what some guy who edited a wiki reckons is the case. $\endgroup$
    – Ben Millwood
    Commented Jun 9, 2012 at 18:25
  • 3
    $\begingroup$ For some more discussion about this, see this related question on SO. $\endgroup$
    – svick
    Commented Jun 9, 2012 at 18:31
  • 1
    $\begingroup$ To reinforce svick's point, it's not possible to find an authority reference on something which is not accepted. Anything claiming to be authorative would simply be wrong (since any number of counter-examples could be provided). $\endgroup$
    – edA-qa mort-ora-y
    Commented Jun 10, 2012 at 5:13
  • $\begingroup$ Well, there's a difference between someone writing a paper that says "here's the One True Definition that everyone agrees on" and someone writing a paper that says "here's the definitions that I'm going to use for this paper, though I know there are others". Even the latter would be better than what I know so far. I think you may be right though, in which case, what do people have to say about the different sorts of type system? Is the dynamic/static distinction, at least, concrete? $\endgroup$
    – Ben Millwood
    Commented Jun 10, 2012 at 10:34

3 Answers 3

Reset to default
18
$\begingroup$

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.

Improve this answer
$\endgroup$
7
  • $\begingroup$ Can you give some references for the historic development? "the absence of run-time type errors means nothing" -- do you mean compile-time here? $\endgroup$
    – Raphael
    Commented Jun 17, 2012 at 12:56
  • $\begingroup$ Here is a paper on Euclid that showed up on Google Scholar. I recall seeing several papers in the 70's, where languages were claimed to be strongly typed. It was generally thought of as a sales pitch. $\endgroup$
    – Uday Reddy
    Commented Jun 17, 2012 at 13:56
  • 1
    $\begingroup$ @Raphael. I did mean "run-time type errors". To get to run-time, the program would have to get past the static type checker in the first place. The point is that a strongly typed language, e.g., Java, will give type errors at run-time when it can't check them at compile-time. A type hole language, e.g., C, will let the run-time produce garbage instead of giving errors. $\endgroup$
    – Uday Reddy
    Commented Jun 17, 2012 at 14:01
  • 1
    $\begingroup$ @benmachine. See the section on "type checking" in the Euclid paper I cited. I think the main point is that "strongly typed" is a buzz word. It is not a technical notion. At best, the technical content of it is to mean that there are no type holes. $\endgroup$
    – Uday Reddy
    Commented Jun 19, 2012 at 18:47
  • 1
    $\begingroup$ On a typical modern implementation where two different integer types have the same representation (e.g. both int and long being 32 bits, or both long and long long being 64, a program that uses a pointer to one such type to write some storage and uses a pointer of the other type to read it, will not generally trigger a detectable run-time error, but may arbitrarily malfunction in arbitrary other ways. Modern C thus loses the type-safety present of other languages, without gaining any of the semantics which quality implementations of Ritchie's language had formerly offered in exchange. $\endgroup$
    – supercat
    Commented Sep 7, 2016 at 19:26
7
$\begingroup$

The paper Uday Reddy found in his answer, On Understanding Types, Data Abstraction, and Polymorphism (1985), gives the following answers:

Programming languages in which the type of every expression can be determined by static program analysis are said to be statically typed. Static typing is a useful property, but the requirement that all variables and expressions are bound to a type at compile time is sometimes too restrictive. It may be replaced by the weaker requirement that all expressions are guaranteed to be type consistent although the type itself may be statically unknown; this can be generally done by introducing some run-time type checking. Languages in which all expressions are type consistent are called strongly typed languages. If a language is strongly typed, its compiler can guarantee that the programs it accepts will execute without type errors. In general, we should strive for strong typing and adopt static typing whenever possible. Note that every statically typed language is strongly typed, but the converse is not necessarily true.

Improve this answer
$\endgroup$
7
  • $\begingroup$ posted as community wiki since I don't deserve the credit for finding this. $\endgroup$
    – Ben Millwood
    Commented Jun 13, 2012 at 15:03
  • $\begingroup$ The issue I have here is related to svick's first comment. While it may be nice that you have found a definition of strong typing, this is certainly not a commonly accepted definition. $\endgroup$
    – edA-qa mort-ora-y
    Commented Jun 14, 2012 at 3:57
  • $\begingroup$ @edA-qamort-ora-y: on what basis do you say that? Do you have something better than anecdotal evidence for what is and is not commonly accepted? Any citations? (I get that you might have a valid point even if not, but I still think the above answers my question; even if there is no consensus, it's good to know at least one of the serious academic answers). $\endgroup$
    – Ben Millwood
    Commented Jun 14, 2012 at 11:35
  • 1
    $\begingroup$ I can't really prove the absence of an agreed upon definition can I? It is not logically possible. However, the Wikipedia articles on strong typing does provide a lot of evidence, and references, for disagreement and contradiction. en.wikipedia.org/wiki/Strong_typing $\endgroup$
    – edA-qa mort-ora-y
    Commented Jun 14, 2012 at 11:39
  • $\begingroup$ @edA-qamort-ora-y: The citations from Wikipedia aren't actually that helpful: some aren't academic, others are cited for reasons other than defining the terms. The Typeful Programming paper does seem promising, but only refers to the definitions very briefly in passing; perhaps it's worth editing in to my answer anyway. With regards proof-of-absence, I think evidence of controversy/disagreement among people who know what they are talking about would suffice for me (which indeed, the Typeful Programming paper may give me). $\endgroup$
    – Ben Millwood
    Commented Jun 14, 2012 at 11:56
6
$\begingroup$

Authoritative answers can be found in Cardelli and Wegner's survey article: On Understanding Types, data abstraction and polymorphism.

Mind you that, while "strong typing" has an accepted meaning, "weak typing" doesn't. Any failure of strong typing might be considered weak and people might differ on what kind of failure is acceptable and what isn't.

Improve this answer
$\endgroup$
6
  • $\begingroup$ Alternate URL: lucacardelli.name/Papers/OnUnderstanding.A4.pdf $\endgroup$
    – AProgrammer
    Commented Jun 11, 2012 at 9:28
  • $\begingroup$ Excellent, that's just what I wanted. The paper takes a bit of reading, so I think there ought to be an answer which summarises the salient points. Should I edit them into your answer, or post my own community wiki answer? Either way, I'm going to give it a couple more days in case anyone else has any input, then accept whatever's left :) $\endgroup$
    – Ben Millwood
    Commented Jun 11, 2012 at 10:49
  • $\begingroup$ @benmachine. The full paper is well worth reading, but the high-level conceptual issues are covered in just the first couple of sections. $\endgroup$
    – Uday Reddy
    Commented Jun 11, 2012 at 20:29
  • 4
    $\begingroup$ I still think it should be summarised on this page. The link might expire later on. $\endgroup$
    – Ben Millwood
    Commented Jun 12, 2012 at 1:59
  • $\begingroup$ @benmachine. You are welcome to post a summary as your own answer to your question. $\endgroup$
    – Uday Reddy
    Commented Jun 12, 2012 at 12:37

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.