Talk:Type system

Fundamental confusion about what types are in programming, and what are static and dynamic types

Let's start with the confusion first:

   These types formalize and enforce the otherwise implicit categories the programmer uses for algebraic data types

The above claim is false in the sense that it only applies to a group of programming languages, but not all of them. It is easy to see how this would go unnoticed since programming languages popular with the industry today would indeed fit nicely into this description. However, it's important to also mention that initially, types in programming weren't perceived as formalization of algebraic data types (the idea of such is a much more modern construct), but, as optimization instructions for compilers specifying storage requirements. This was the position of ALGOL authors, and, to a large extent, this is the position of many languages that predate ML / Miranda family of languages.

I also don't see why annotations like, for example, instantiation mode in languages in Prolog family would be treated differently from types (functionally, they serve the same purpose: to ensure program's correctness, and, perhaps, to hint the compiler about optimization opportunities). This is while more mainstream languages, like C, for example, can have a lot of modalities added to definitions, indicating whether or not a function needs to be inlined, whether or not the memory allocated to a struct needs to be padded with zeros to be a multiple of some number, whether a function needs to implement a particular calling convention and so on. Similarly, Java's and C++'s checked exceptions and a lot of other such mechanisms, which all fall under the category of "ensuring program's correctness by providing more information at the time of its definition". I don't see a reason for why would they be excluded from the type family. I think, it needs to be stated that the "types as in type theory, a sub-field of mathematical logic =/= types in programming", however, closely related, especially in the context of a lot of modern languages.

Bottom line, I think the quoted statement is (unintentionally) biased towards particular interpretation of what types mean, but it's not general enough to properly reflect the much more diverse reality.

There's another very popular confusion: statically typed languages and dynamically typed languages. A lot of people believe that these things exist, and use this terminology routinely. However, there's no real definition that would support such separation. In fact, if you were to follow whatever claims made by the people believing that a particular language is statically or dynamically typed, you'd easily discover a contradiction. There's another way to interpret what "static" and "dynamic" means, when applied to types. Unfortunately, I cannot quote a source, but the idea isn't mine: it makes it simple and unambiguous, and useful at the same time. Static types are types known at any time before the program is executed (eg. compilation time, or syntax checking time etc.), while dynamic types are the types known at the time of execution time. Thus, for example, a statement in Java of the form List<Integer> x = ...; will assign the static type "List<Integer>" to variable "x", but may assign type "ArrayList<Integer>" at run time. Thus making the distinction meaningful and useful. 109.67.57.250 (talk) 21:38, 3 September 2019 (UTC)

I wrote the first version of that sentence with "data types" but someone added the "algebraic" which I agree changes the meaning badly. Feel free to change this back, I don't have the inclination to get involved in edit wars. TobyK (talk) 17:39, 4 June 2022 (UTC)

No Typing

Anyone reading this article is likely to believe that all programming languages have type checking. They don't (eg Rexx). This article would be improved if it mentioned this (and why one might want to not carry out type checking). Then this article would cover the subject comprehensively. Eg an article describing why whales migrate would be incomplete if it failed to mentions that some wales off the West Coast of America no longer migrate. FreeFlow99 (talk) 18:36, 11 November 2021 (UTC)

I think I would describe REXX as an extreme example of a dynamically-typed language. REXX has one data type, the character string. This also holds for for example Tcl and many command-line interpreters. REXX has the build-in function DATATYPE which will return NUM if its argument conforms to the syntax defined by REXX for numbers, and CHAR otherwise.[1]. What's more, I think the built-in arithmetic operations in REXX are required to raise a condition when given nonnumeric arguments (but I'm not sure). I would call this a run-time type check. Should the article say more about this?

The lead section of the article already explains that type checking "can happen statically (at compile time), dynamically (at run time), or as a combination of both". The section Type system § Static and dynamic type checking in practice talks about the various trade-offs between the varying degrees of static and dynamic type checking.

(A perhaps more extreme example of a language with a single data type would be B where the only data type is the machine word.)

—Tea2min (talk) 12:28, 12 November 2021 (UTC)

And STOIC and FORTH I think, but it is such a long time since I used STOIC I don't remember. Certainly everything that was passed between procedures/functions did so on the stack (as words I think). I don't think there was any static or dynamic type checking.

In any case, the pros and cons of not having type checking, (or having minimal type checking), eg improved performance, or reduced bureaucracy/clutter ought to be included I think. One plausible argument against type checking is: if it only spots errors in programs written by the sort of person who would multiply a man's shoe size by his name, ie the sort of person who doesn't think clearly enough to be allowed to write software that others would rely on, we can expect that person will still manage to multiply a man's shoe size by his bank account number. FreeFlow99 (talk) 15:58, 12 November 2021 (UTC)

This style of thinking is exemplified by 'free and bold estimation', as in the dimensional analysis from physics (see George Gamow's books 'One Two Three... Infinity', 'Thirty years that shook physics' (quantum mechanics), or 'My world-line' (relativity)) and the thinking of other creative thinkers (Gamow was influential in the thinking behind the genetic code). The mathematical rule would be that you may not add the differing units, but that you may multiply them. Once the resultants are of the same type of composite unit, you may add them. --Ancheta Wis   (talk | contribs) 13:38, 18 September 2022 (UTC)

Link to nothing

Under See Also, there is a link to "Typing Rules" which is a page that does not exist. 69.120.241.110 (talk) 16:16, 8 August 2023 (UTC)

I removed it, thanks for pointing it out. MrOllie (talk) 01:27, 9 August 2023 (UTC)

Restoration of anchors

@Naruyoko: I'll manually revert a part of this edit of yours, since I believe that was a mistake. I discovered your edit when investigating why a redirect to a section didn't work. Your edit broke it, by removing some appropriate anchors (which actually were not in any manner "self-referencing", notwithstanding your edit message). (I avoid making reverts without comments; whence this message, in spite of my belief that it was made by mistake. If I'm wrong, you may revert me, but then should also explain your edit here.) Regards, JoergenB (talk) 21:24, 24 January 2025 (UTC)

That is indeed a mistake. Good catch. --Naruyoko (talk) 04:05, 25 January 2025 (UTC)

Merge proposal

I think this page ought to be merged into Data type due to total overlap of the two topics. Types are products of type systems, so any explanation of types will inevitably be an explanation of type systems, as is currently the case on the data type article. However, types are usually discussed and thought of as is, because type systems are only really relevant to inter-language discussion, not intra-language; therefore, the idea of a "type system" isn't really something people think about often. I thus feel that merging the other way around, despite this article being bigger, would be unwise, as "type system" would be a peculiar title for the topic. Kaotao (talk) 08:50, 5 February 2025 (UTC)

Oppose: While there may seem to be overlap between "Type system" and "Data type," these concepts are distinct and merit separate articles.

To clarify, a type system is a formal framework that assigns types to terms according to a set of logical rules. In contrast, a data type refers to a specific collection of values and operations, often in the context of machine representation or database structures.

Your assertion that "[data] types are products of type systems" is inaccurate. The types assigned by a type system are not necessarily data types. For instance, linear types, affine types, and region types express constraints beyond simple value sets or operations. Moreover, in many cases, a term can have multiple possible types (due to subtyping, polymorphism, etc.), but a type system provides rules to select an appropriate one. This distinction highlights why data types can be discussed independently of type systems, even though more advanced types require the structure of a type system to be meaningful.

Additionally, your claim that "the idea of a type system isn’t something people think about often" overlooks its significant role in programming language theory. Type systems are a well-developed academic field, extensively researched and central to programming language design. While the concept of a data type is sometimes examined within type systems (e.g., in Castagna's semantic subtyping research), it is more commonly studied in database theory, as evidenced by specific types like the SQL Server MONEY type.

The existing Data type article does not simply reiterate the Type system article; rather, it serves as a bridge between type theory and database-oriented perspectives. While a significant number of types appear in both articles, the focus differs: the Data type article presents a set-theoretic and practical view, while the Type system article explores the syntactic and logical rules of these types as defined in formal type systems.

Finally, the idea that type systems are irrelevant to intra-language discussion is incorrect. The lambda calculus alone has multiple well-studied type systems, warranting its own article, Typed lambda calculus, which details various approaches such as simple typing, System F, and the Calculus of Constructions.

Given these distinctions, merging Type system into Data type would obscure important conceptual differences and reduce the clarity of both topics. Keeping them separate allows each article to properly address its respective subject matter. Now it is true that the Type system#Specialized type systems section is unsourced and needs a lot of work, but that is not grounds for deleting the whole article, which discusses many concerns of programming language type systems that are completely unrelated to the set of data types it implements (e.g., static vs. dynamic). Mathnerd314159 (talk) 18:49, 5 February 2025 (UTC)

I made this proposal under the assumption that "data type" could encompass both topics and house the combined information of both articles, my bad. If the data type article was generalized into something like "Type (computer science)", then would it be a good merge target? When I said that "type systems aren't something people think about often" I was referring to its WP:COMMONNAME status; I feel that "type (computer science)" would be a more intuitive name than "type system" for most people. The data type article as it stands is rather short, and I feel like housing practical and theoretical aspects in the same article, each backing the other, would be the most efficient way of organizing the information, especially if "data type" is too specific to be the "other half" of this entire article. Accurate definitions and descriptions of type systems and of data types can be provided within the text; if they were merged, the weight allotted to each topic would remain the same. Things staying as they are decreases visibility of type systems, and many readers may miss the vital information contained here as a result. Kaotao (talk) 19:54, 5 February 2025 (UTC)