4 ms·

A brief history of “type” (2015)

66 points by mr_golyadkin 9y ago

dvt 9y ago
Interesting article, but I had a hunch, and after some research, I found that the first use of "type" was actually in 1945(ish), in Konrad Zuse's Plankalkül[1]. I wouldn't be surprised if there's something even earlier. My hunch was motivated by the fact that Frege had already made the very insightful distinction between functional and non-functional types in the 1890s, and that type theory had already been around for a fairly long time (at least since Russell and Whitehead's Principia). In other words, just about everything had already been formalized, you just needed to have someone come in and say "computer programs are better behaved when data has a type". In the case of Plankalkül, the types of variables are stored as single bits[2]. [1] http://zuse.zib.de/file/zuse_archive-0233.pdf?id=http%3A//zuse.zib.de/file/1rUAfKDkirW8o3gT/21/1c/70/9e-d718-4b4e-be7b-ed9b620f5683/0/original/092be0ebdd0784fee570ef37eee273c7.pdf http://zuse.zib.de/file/zuse_archive-0233.pdf?id=http%3A//zu... [2] http://www.cs.ru.nl/bachelorscripties/2010/Bram_Bruines___0213837___Plankalkul.pdf http://www.cs.ru.nl/bachelorscripties/2010/Bram_Bruines___02...
deathanatos 9y ago
> So the confusion between programming-language and type-theory senses of the word began with the very first paper to use the latter. Okay … but what's the confusion, exactly? Wikipedia defines type theory as[1], > In type theory, every "term" has a "type" and operations are restricted to terms of a certain type. Which sounds very much like how programs use it: terms in expressions in statically typed languages do have a type; in some, functions themselves, much like Wikipedia's addOne example, have a type. Whereas the Wikipedia article for type system says[2], > Assigning a data type, termed typing, gives meaning to a sequence of bits such as a value in memory or some object such as a variable. This is, I feel, a better definition. Or at least, it gets at what programmers are concerned about: the meaning of the sequence of bits (and from that meaning, the set of valid possible values and operations, and more importantly, that not all values (of differing types) are valid in all operations; I would argue that the bits aren't so much involved, since there are multiple ways to store the same sets of values. E.g., Unicode strings can be stored in a number of bit forms). [1]: https://en.wikipedia.org/wiki/Type_theory https://en.wikipedia.org/wiki/Type_theory [2]: https://en.wikipedia.org/wiki/Type_system https://en.wikipedia.org/wiki/Type_system
- DonbunEf7 9y ago
  The confusion stems from the popular usage of type system, which Benjamin Pierce defines thus, "A type system is a syntactic method for enforcing levels of abstraction in programs." [0] Note that it does not have to be a type-theoretic type system! This is precisely the source of the confusion. Bit patterns don't have to matter. There are languages like Haskell which have type-theoretic type systems and no bit patterns specified [1]. There are also languages like C, which has non-type-theoretic type systems and lots of things to say about bits, and languages like ANS FORTH, which has no type system at all and could reinterpret bit patterns. There are also languages which have features generally referred to as type systems, and which fit Pierce's definition, but which are not just not type-theoretic, but don't resemble any kind of system which discriminates values based on membership in a set. For example, Pony and Rust both have syntactic forms for adding memory semantics to values, and their type-checking routines check the memory semantics oblivious to the bits being stored. Pony additionally can check certain causality properties. Monte has auditors, which are syntactically-specified objects which enforce semantic properties of other objects by examining their ASTs [2]. In summary, "type system" means what Pierce says it means: there is syntax, the syntax describes abstract properties of the program, the properties can be checked by syntax-guided computation, and programs can be rejected as invalid if the check fails. [0] https://www.cis.upenn.edu/~bcpierce/tapl/ https://www.cis.upenn.edu/~bcpierce/tapl/ [1] https://www.haskell.org/onlinereport/basic.html https://www.haskell.org/onlinereport/basic.html [2] http://monte.readthedocs.io/en/latest/auditors.html http://monte.readthedocs.io/en/latest/auditors.html
  - _0ffh 9y ago
    Then again, apart from the explicit (like bitwise operations and bitfields), even C tries to be hands-off about the encoding of its types. The reason for the infamous undefinedness of signed integer overflow is precisely that C tries to be agnostic about their encoding (which mostly comes down to two's complement vs sign bit).
  - pron 9y ago
    > Note that it does not have to be a type-theoretic type system! This is precisely the source of the confusion. What do you mean by "type theoretic"? Once you have a formal system where your objects are divided into sorts and your syntactic expressions are constrained by those sorts such that expressions may be ill-formed when the sorts are mismatched (by some definition), then you have a type theory on your hands. > the properties can be checked by syntax-guided computation Not all type systems can be checked by computation (some are undecidable).

66 points by mr_golyadkin 9y ago

dvt 9y ago

Interesting article, but I had a hunch, and after some research, I found that the first use of "type" was actually in 1945(ish), in Konrad Zuse's Plankalkül[1]. I wouldn't be surprised if there's something even earlier. My hunch was motivated by the fact that Frege had already made the very insightful distinction between functional and non-functional types in the 1890s, and that type theory had already been around for a fairly long time (at least since Russell and Whitehead's Principia). In other words, just about everything had already been formalized, you just needed to have someone come in and say "computer programs are better behaved when data has a type". In the case of Plankalkül, the types of variables are stored as single bits[2]. [1] http://zuse.zib.de/file/zuse_archive-0233.pdf?id=http%3A//zuse.zib.de/file/1rUAfKDkirW8o3gT/21/1c/70/9e-d718-4b4e-be7b-ed9b620f5683/0/original/092be0ebdd0784fee570ef37eee273c7.pdf http://zuse.zib.de/file/zuse_archive-0233.pdf?id=http%3A//zu... [2] http://www.cs.ru.nl/bachelorscripties/2010/Bram_Bruines___0213837___Plankalkul.pdf http://www.cs.ru.nl/bachelorscripties/2010/Bram_Bruines___02...

deathanatos 9y ago

> So the confusion between programming-language and type-theory senses of the word began with the very first paper to use the latter. Okay … but what's the confusion, exactly? Wikipedia defines type theory as[1], > In type theory, every "term" has a "type" and operations are restricted to terms of a certain type. Which sounds very much like how programs use it: terms in expressions in statically typed languages do have a type; in some, functions themselves, much like Wikipedia's addOne example, have a type. Whereas the Wikipedia article for type system says[2], > Assigning a data type, termed typing, gives meaning to a sequence of bits such as a value in memory or some object such as a variable. This is, I feel, a better definition. Or at least, it gets at what programmers are concerned about: the meaning of the sequence of bits (and from that meaning, the set of valid possible values and operations, and more importantly, that not all values (of differing types) are valid in all operations; I would argue that the bits aren't so much involved, since there are multiple ways to store the same sets of values. E.g., Unicode strings can be stored in a number of bit forms). [1]: https://en.wikipedia.org/wiki/Type_theory https://en.wikipedia.org/wiki/Type_theory [2]: https://en.wikipedia.org/wiki/Type_system https://en.wikipedia.org/wiki/Type_system

DonbunEf7 9y ago
The confusion stems from the popular usage of type system, which Benjamin Pierce defines thus, "A type system is a syntactic method for enforcing levels of abstraction in programs." [0] Note that it does not have to be a type-theoretic type system! This is precisely the source of the confusion. Bit patterns don't have to matter. There are languages like Haskell which have type-theoretic type systems and no bit patterns specified [1]. There are also languages like C, which has non-type-theoretic type systems and lots of things to say about bits, and languages like ANS FORTH, which has no type system at all and could reinterpret bit patterns. There are also languages which have features generally referred to as type systems, and which fit Pierce's definition, but which are not just not type-theoretic, but don't resemble any kind of system which discriminates values based on membership in a set. For example, Pony and Rust both have syntactic forms for adding memory semantics to values, and their type-checking routines check the memory semantics oblivious to the bits being stored. Pony additionally can check certain causality properties. Monte has auditors, which are syntactically-specified objects which enforce semantic properties of other objects by examining their ASTs [2]. In summary, "type system" means what Pierce says it means: there is syntax, the syntax describes abstract properties of the program, the properties can be checked by syntax-guided computation, and programs can be rejected as invalid if the check fails. [0] https://www.cis.upenn.edu/~bcpierce/tapl/ https://www.cis.upenn.edu/~bcpierce/tapl/ [1] https://www.haskell.org/onlinereport/basic.html https://www.haskell.org/onlinereport/basic.html [2] http://monte.readthedocs.io/en/latest/auditors.html http://monte.readthedocs.io/en/latest/auditors.html
- _0ffh 9y ago
  Then again, apart from the explicit (like bitwise operations and bitfields), even C tries to be hands-off about the encoding of its types. The reason for the infamous undefinedness of signed integer overflow is precisely that C tries to be agnostic about their encoding (which mostly comes down to two's complement vs sign bit).
- pron 9y ago
  > Note that it does not have to be a type-theoretic type system! This is precisely the source of the confusion. What do you mean by "type theoretic"? Once you have a formal system where your objects are divided into sorts and your syntactic expressions are constrained by those sorts such that expressions may be ill-formed when the sorts are mismatched (by some definition), then you have a type theory on your hands. > the properties can be checked by syntax-guided computation Not all type systems can be checked by computation (some are undecidable).