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:
"1"can be used in more or less any context that
- 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.