8 ms·

Where does the name "algebraic data type" come from?

noelwelsh 2y ago
I tried to figure out the history of algebraic data types for a little bibliographic section in my book (Book is https://scalawithcats.com/ https://scalawithcats.com/ Chapter 2 is algebraic data types. My history is much less thorough than the linked post!) I'm glad I seemed to have got it correct. The evolution of programming language features is quite interesting. The first presentations of a concept often are very rough as people struggle to present an idea in terms of what is currently known. Even terminology can change a lot. E.g. generalized algebraic data types started out as, variously, indexed types, first-class phantom types, and more, before the current terminology was adopted. (Adoption by a reasonably widely used language, in this case Haskell, helps to fix terminology.) I wouldn't be surprised if the term indexed types comes back into vogue if future languages start taking codata more seriously.
defrost 2y ago
Tangential reference to Robin Milner .. couple of big contributions to formal logic in computing, Turing Award, FRS (Fellow Royal Society), FRSE (Fellow Royal Society Edinburgh), etc. Four Doctoral students .. and this gem: Doctoral advisor: None, as Milner never did a PhD https://en.wikipedia.org/wiki/Robin_Milner https://en.wikipedia.org/wiki/Robin_Milner
- jffhn 2y ago
  15 or 20 years ago there was an online video of Milner giving a talk at Inria, about building the "tower of digital computing" (I recall this expression), but since I never managed to find it again.
  - layer8 2y ago
    “Tower of (informatic) models”, possibly: https://citeseerx.ist.psu.edu/document?repid=rep1&type=pdf&doi=f2e0ae7d516fe47a95395bea16a13809ab7489cf https://citeseerx.ist.psu.edu/document?repid=rep1&type=pdf&d... https://www.cl.cam.ac.uk/archive/rm135/models-for-kahn.pdf https://www.cl.cam.ac.uk/archive/rm135/models-for-kahn.pdf
    - jffhn 2y ago
      Thanks, I also recall he was talking about G. Kahn as in the second pdf, so both must originate from this colloquium: https://ercim-news.ercim.eu/en68/in-brief/colloquium-in-memory-of-gilles-kahn https://ercim-news.ercim.eu/en68/in-brief/colloquium-in-memo...
- deleted 2y ago
  [deleted]
lupire 2y ago
The article pains to distinguish "free algebra" from "sums and products", but a "free algebra" is a ring, and a ring is an abstract representation of sums and products. Yes, for the mathematician there are finer distinctions, but after a first pass of data compression for the lay audience, they are the same thing. When your workday programmer understands that AND and OR are sums and products, and concatenation is a non-commutative product (sets are commutative, but lists are not), they are halfway to free algebra in one day, without a masters degree in mathematics. The written language of free algebra usually uses the + and • symbols. https://en.m.wikipedia.org/wiki/Free_algebra https://en.m.wikipedia.org/wiki/Free_algebra
- sreekotay 2y ago
  Under rated reply. (Though I think here the author means "free algebra" in the colloquial sense)
  - 082349872349872 2y ago
    More "ring theory sense" than "colloquial sense", at least among my colloquy?
- js8 2y ago
  > that AND and OR are sums and products Perhaps you meant to say that AND and XOR are products and sums.
  - klysm 2y ago
    It seems fair to think of OR as a 'saturating' sum
    - js8 2y ago
      The issue is then boolean functions do not form a polynomial ring with this "sum", because unlike XOR, OR is not a group operation - it doesn't have a well defined inverse.
beanjuiceII 2y ago
[flagged]
Joker_vD 2y ago
Oh no, you talked about Miranda without saying in a footnote that "Miranda™ is a trademark of Research Software Limited"! Now you will get a stern letter from David Turner!
- deleted 2y ago
  [deleted]
- syrak 2y ago
  Is that something he did to people who mis-cited his language?!
  - Joker_vD 2y ago
    I don't know. But I've read quite a number of papers on type systems, type inferences and functional languages in general from late 80s and early 90s, and every time they mention Miranda, there is this footnote that says that "Miranda is a trademark of Research Software Limited", e.g. [0][1][2], so there has to be a reason why they did this. Sure, Turner himself did that as well, see "History of Haskell" [3], "3.8. Haskell and Miranda": As required to safeguard his trademark, Turner always footnoted the first occurrence of Miranda in his papers to state it was a trademark of Research Software Limited. In response, some early Haskell presentations included a footnote "Haskell is not a trademark". but that doesn't really explains why others did... so a hypothesis that maybe he did send people who didn't attribute Miranda's trademark a letter of complaint seems somewhat amusing, you know? A small in-joke for those people who brushed against the FP research of the early 90s. [0] https://dl.acm.org/doi/pdf/10.1145/75277.75283 https://dl.acm.org/doi/pdf/10.1145/75277.75283 [1] https://christopherclack.com/images/Documents/kielty-1997.pdf https://christopherclack.com/images/Documents/kielty-1997.pd..., bottom of p. 3 [2] https://citeseerx.ist.psu.edu/document?repid=rep1&type=pdf&doi=2fecac2065e733147a14bc1fd8ec5c8ce5e1012f https://citeseerx.ist.psu.edu/document?repid=rep1&type=pdf&d... [3] https://www.microsoft.com/en-us/research/wp-content/uploads/2016/07/history.pdf https://www.microsoft.com/en-us/research/wp-content/uploads/...
    - syrak 2y ago
weinzierl 2y ago
The article begins with how ADTs existed in the 80s, before they were called like that, and the ADT Wikipedia article also mentions the language Hope as origin from the 80s. Record and Variant types were definitely in Pascal and likely already in ALGOL in the 60s. Why wouldn't these qualify as ADTs by another name equally?
- IshKebab 2y ago
  I'm not a type theorist and the article isn't super clear IMO, but it sounds like they definitely would. The "algebraic data type" name was obsolete pretty much immediately, in the same way that nobody talks about horseless carriages now. It exists just to confuse people and is probably best avoided.
  - noelwelsh 2y ago
    I think it's still useful as many languages (still!) have no equivalent to the Or / sum type part of algebraic data types.
- fanf2 2y ago
  Algol 60 did not have record or structure types. Record types did not really become a thing until the mid-1960s around the time of CPL (1963) - Algol W (1966)
  - deleted 2y ago
    [deleted]
  - trealira 2y ago
    ALGOL 68 did have structs and unions, however, which might be what they meant by "ALGOL in the 60s." That doesn't contradict what you say, though, since 1968 is already in the late 1960s.
- noelwelsh 2y ago
  I didn't recall anything like ADTs in Pascal, but I last used it a very long time ago, so I dug into it. A "record with variant part"[1] seems to be equivalent in expressive power to ADTs. However Pascal lacks the other part of the equation, which is the guarantees when taking apart such a type that you will handle all cases, a.k.a exhaustivity checking. In general, I think too much material focuses on the data defining part of algebraic data types, and not the data using part, known as strucural recursion, which is arguably more useful. (You tend to use data more than you define it.) It's also interesting that more "modern" libraries have forgotten these lessons. E.g. Python and Go have nothing like algebraic data types. [1]: https://www.freepascal.org/docs-html/ref/refsu15.html https://www.freepascal.org/docs-html/ref/refsu15.html
kccqzy 2y ago
I've always thought a nifty thing about algebraic data types is the ability to deduce their size (in the set theoretic sense, the number of possible elements) by algebra. Consider Bool which is a fundamental primitive type with size 2. Now consider the product type Bool × Bool × Bool (a three-tuple), it's clear that it has size 2×2×2=8. On the other hand if we have the sum type Bool + Bool + Bool (a discriminated union), it's also clear it has size 2+2+2=6. And this works with recursion too. The list type whose element type is A is defined as either Nil or an element plus the remainder of the list: that's exactly L(A)=1+A*L(A). And that directly solves to L(A)=1/(1-A). If you've studied generating functions or even just Taylor series, you know this can be expanded into 1+A+A^2+A^3+… which perfectly matches the intuition of a list having any number of elements. What if I want to define a special list that only allows even number of elements? It would be L(A)=1+A*A*L(A), or 1/(1-A^2) which expands to 1+A^2+A^4+… Both of course are "infinite" but it allows us to distinguish precisely what kind of "infinity."
- kqr 2y ago
  This also helps with figuring out isomorphisms, i.e. when two types are equivalent. So for example, if someone tries to represent an "Either Bool Bool" (2+2 cases) with three cases, we see immediately there's a singularity in there which represents at least two of the possible values of the original, i.e. we won't be able to losslessly round trip.
  - perihelions 2y ago
    This works with function types too. You can get a hint that objects with signature A -> (A -> A) have an isomorphism with objects of signature (A × A) -> A, by observing that the cardinalities are equal as algebraic expressions, ( |A|^|A| )^|A| = |A|^( |A|*|A| ). That one's just "currying" [0]. [0] https://en.wikipedia.org/wiki/Currying https://en.wikipedia.org/wiki/Currying
    - Sharlin 2y ago
      Yep, that’s one of the more mind-blowing "tricks" as it were. Maybe less moreso, but still nifty, is that |T -> bool| = |bool|^|T| = 2^|T| …which also happens to be the number of subsets of a set of size |T|. And indeed that’s what a predicate function is, a subset-generator; for every subset there is exactly one predicate that picks the members of that subset from the larger set.
derriz 2y ago
I’m pretty sure Miranda did not allow the user to directly define term rewriting rules for algebraic data types. Obviously this is from decades ago so my memory could be faulty but I used it a lot for a year or two and do not remember that feature.
- syrak 2y ago
  That's surprising! I (author of the blog) just repeated what's in the 1985 paper. The feature might actually have been removed, or never even been implemented. One would have to find an implementation to check.
  - derriz 2y ago
    Could be. This overview from the end of 1986 - https://www.cs.kent.ac.uk/people/staff/dat/miranda/Overview.html https://www.cs.kent.ac.uk/people/staff/dat/miranda/Overview.... - fairly matches my recollection of the language and doesn't mention such a feature.
    - syrak 2y ago
      Thanks! Here we go: "Note: In versions of Miranda before release two (1989) it was possible to associate "laws" with the constructors of an algebraic type, which are applied whenever an object of the type is built. For details see Turner 1985, Thompson 1986. This feature was little used and has since been removed from the language. "
      - derriz 2y ago
        Cool - mystery solved!
      - 082349872349872 2y ago
        fwiw I unwittingly retrod this path; looking back at early versions of my algebraic type library there were all sorts of provisions for automatic smart constructors (commutativity, identities, etc., surely inspired by Goguen) that got dropped from later versions for lack of use.
kragen 2y ago
i'd forgotten that clu had pattern matching! it's interesting and surprising that full-fledged adts come from hehner's universal algebra
burakemir 2y ago
Let's define a mapping F to act as a "signature-step" of an algebraic data type with operations op as a map (functor) from X to Sum_op X^arity(op). This involves a sum of products (or coproduct of products). See "Recursive types for free" https://homepages.inf.ed.ac.uk/wadler/papers/free-rectypes/free-rectypes.txt https://homepages.inf.ed.ac.uk/wadler/papers/free-rectypes/f...

I tried to figure out the history of algebraic data types for a little bibliographic section in my book (Book is https://scalawithcats.com/ https://scalawithcats.com/ Chapter 2 is algebraic data types. My history is much less thorough than the linked post!) I'm glad I seemed to have got it correct. The evolution of programming language features is quite interesting. The first presentations of a concept often are very rough as people struggle to present an idea in terms of what is currently known. Even terminology can change a lot. E.g. generalized algebraic data types started out as, variously, indexed types, first-class phantom types, and more, before the current terminology was adopted. (Adoption by a reasonably widely used language, in this case Haskell, helps to fix terminology.) I wouldn't be surprised if the term indexed types comes back into vogue if future languages start taking codata more seriously.

defrost 2y ago

Tangential reference to Robin Milner .. couple of big contributions to formal logic in computing, Turing Award, FRS (Fellow Royal Society), FRSE (Fellow Royal Society Edinburgh), etc. Four Doctoral students .. and this gem: Doctoral advisor: None, as Milner never did a PhD https://en.wikipedia.org/wiki/Robin_Milner https://en.wikipedia.org/wiki/Robin_Milner

jffhn 2y ago
15 or 20 years ago there was an online video of Milner giving a talk at Inria, about building the "tower of digital computing" (I recall this expression), but since I never managed to find it again.
- layer8 2y ago
  “Tower of (informatic) models”, possibly: https://citeseerx.ist.psu.edu/document?repid=rep1&type=pdf&doi=f2e0ae7d516fe47a95395bea16a13809ab7489cf https://citeseerx.ist.psu.edu/document?repid=rep1&type=pdf&d... https://www.cl.cam.ac.uk/archive/rm135/models-for-kahn.pdf https://www.cl.cam.ac.uk/archive/rm135/models-for-kahn.pdf
  - jffhn 2y ago
    Thanks, I also recall he was talking about G. Kahn as in the second pdf, so both must originate from this colloquium: https://ercim-news.ercim.eu/en68/in-brief/colloquium-in-memory-of-gilles-kahn https://ercim-news.ercim.eu/en68/in-brief/colloquium-in-memo...
deleted 2y ago
[deleted]

lupire 2y ago

The article pains to distinguish "free algebra" from "sums and products", but a "free algebra" is a ring, and a ring is an abstract representation of sums and products. Yes, for the mathematician there are finer distinctions, but after a first pass of data compression for the lay audience, they are the same thing. When your workday programmer understands that AND and OR are sums and products, and concatenation is a non-commutative product (sets are commutative, but lists are not), they are halfway to free algebra in one day, without a masters degree in mathematics. The written language of free algebra usually uses the + and • symbols. https://en.m.wikipedia.org/wiki/Free_algebra https://en.m.wikipedia.org/wiki/Free_algebra

sreekotay 2y ago
Under rated reply. (Though I think here the author means "free algebra" in the colloquial sense)
- 082349872349872 2y ago
  More "ring theory sense" than "colloquial sense", at least among my colloquy?
js8 2y ago
> that AND and OR are sums and products Perhaps you meant to say that AND and XOR are products and sums.
- klysm 2y ago
  It seems fair to think of OR as a 'saturating' sum
  - js8 2y ago
    The issue is then boolean functions do not form a polynomial ring with this "sum", because unlike XOR, OR is not a group operation - it doesn't have a well defined inverse.

beanjuiceII 2y ago

[flagged]

Joker_vD 2y ago

Oh no, you talked about Miranda without saying in a footnote that "Miranda™ is a trademark of Research Software Limited"! Now you will get a stern letter from David Turner!

deleted 2y ago
[deleted]
syrak 2y ago
Is that something he did to people who mis-cited his language?!
- Joker_vD 2y ago
  I don't know. But I've read quite a number of papers on type systems, type inferences and functional languages in general from late 80s and early 90s, and every time they mention Miranda, there is this footnote that says that "Miranda is a trademark of Research Software Limited", e.g. [0][1][2], so there has to be a reason why they did this. Sure, Turner himself did that as well, see "History of Haskell" [3], "3.8. Haskell and Miranda": As required to safeguard his trademark, Turner always footnoted the first occurrence of Miranda in his papers to state it was a trademark of Research Software Limited. In response, some early Haskell presentations included a footnote "Haskell is not a trademark". but that doesn't really explains why others did... so a hypothesis that maybe he did send people who didn't attribute Miranda's trademark a letter of complaint seems somewhat amusing, you know? A small in-joke for those people who brushed against the FP research of the early 90s. [0] https://dl.acm.org/doi/pdf/10.1145/75277.75283 https://dl.acm.org/doi/pdf/10.1145/75277.75283 [1] https://christopherclack.com/images/Documents/kielty-1997.pdf https://christopherclack.com/images/Documents/kielty-1997.pd..., bottom of p. 3 [2] https://citeseerx.ist.psu.edu/document?repid=rep1&type=pdf&doi=2fecac2065e733147a14bc1fd8ec5c8ce5e1012f https://citeseerx.ist.psu.edu/document?repid=rep1&type=pdf&d... [3] https://www.microsoft.com/en-us/research/wp-content/uploads/2016/07/history.pdf https://www.microsoft.com/en-us/research/wp-content/uploads/...
  - syrak 2y ago

weinzierl 2y ago

The article begins with how ADTs existed in the 80s, before they were called like that, and the ADT Wikipedia article also mentions the language Hope as origin from the 80s. Record and Variant types were definitely in Pascal and likely already in ALGOL in the 60s. Why wouldn't these qualify as ADTs by another name equally?

IshKebab 2y ago
I'm not a type theorist and the article isn't super clear IMO, but it sounds like they definitely would. The "algebraic data type" name was obsolete pretty much immediately, in the same way that nobody talks about horseless carriages now. It exists just to confuse people and is probably best avoided.
- noelwelsh 2y ago
  I think it's still useful as many languages (still!) have no equivalent to the Or / sum type part of algebraic data types.
fanf2 2y ago
Algol 60 did not have record or structure types. Record types did not really become a thing until the mid-1960s around the time of CPL (1963) - Algol W (1966)
- deleted 2y ago
  [deleted]
- trealira 2y ago
  ALGOL 68 did have structs and unions, however, which might be what they meant by "ALGOL in the 60s." That doesn't contradict what you say, though, since 1968 is already in the late 1960s.
noelwelsh 2y ago
I didn't recall anything like ADTs in Pascal, but I last used it a very long time ago, so I dug into it. A "record with variant part"[1] seems to be equivalent in expressive power to ADTs. However Pascal lacks the other part of the equation, which is the guarantees when taking apart such a type that you will handle all cases, a.k.a exhaustivity checking. In general, I think too much material focuses on the data defining part of algebraic data types, and not the data using part, known as strucural recursion, which is arguably more useful. (You tend to use data more than you define it.) It's also interesting that more "modern" libraries have forgotten these lessons. E.g. Python and Go have nothing like algebraic data types. [1]: https://www.freepascal.org/docs-html/ref/refsu15.html https://www.freepascal.org/docs-html/ref/refsu15.html

kccqzy 2y ago

I've always thought a nifty thing about algebraic data types is the ability to deduce their size (in the set theoretic sense, the number of possible elements) by algebra. Consider Bool which is a fundamental primitive type with size 2. Now consider the product type Bool × Bool × Bool (a three-tuple), it's clear that it has size 2×2×2=8. On the other hand if we have the sum type Bool + Bool + Bool (a discriminated union), it's also clear it has size 2+2+2=6. And this works with recursion too. The list type whose element type is A is defined as either Nil or an element plus the remainder of the list: that's exactly L(A)=1+A*L(A). And that directly solves to L(A)=1/(1-A). If you've studied generating functions or even just Taylor series, you know this can be expanded into 1+A+A^2+A^3+… which perfectly matches the intuition of a list having any number of elements. What if I want to define a special list that only allows even number of elements? It would be L(A)=1+A*A*L(A), or 1/(1-A^2) which expands to 1+A^2+A^4+… Both of course are "infinite" but it allows us to distinguish precisely what kind of "infinity."

kqr 2y ago
This also helps with figuring out isomorphisms, i.e. when two types are equivalent. So for example, if someone tries to represent an "Either Bool Bool" (2+2 cases) with three cases, we see immediately there's a singularity in there which represents at least two of the possible values of the original, i.e. we won't be able to losslessly round trip.
- perihelions 2y ago
  This works with function types too. You can get a hint that objects with signature A -> (A -> A) have an isomorphism with objects of signature (A × A) -> A, by observing that the cardinalities are equal as algebraic expressions, ( |A|^|A| )^|A| = |A|^( |A|*|A| ). That one's just "currying" [0]. [0] https://en.wikipedia.org/wiki/Currying https://en.wikipedia.org/wiki/Currying
  - Sharlin 2y ago
    Yep, that’s one of the more mind-blowing "tricks" as it were. Maybe less moreso, but still nifty, is that |T -> bool| = |bool|^|T| = 2^|T| …which also happens to be the number of subsets of a set of size |T|. And indeed that’s what a predicate function is, a subset-generator; for every subset there is exactly one predicate that picks the members of that subset from the larger set.

derriz 2y ago

I’m pretty sure Miranda did not allow the user to directly define term rewriting rules for algebraic data types. Obviously this is from decades ago so my memory could be faulty but I used it a lot for a year or two and do not remember that feature.

syrak 2y ago
That's surprising! I (author of the blog) just repeated what's in the 1985 paper. The feature might actually have been removed, or never even been implemented. One would have to find an implementation to check.
- derriz 2y ago
  Could be. This overview from the end of 1986 - https://www.cs.kent.ac.uk/people/staff/dat/miranda/Overview.html https://www.cs.kent.ac.uk/people/staff/dat/miranda/Overview.... - fairly matches my recollection of the language and doesn't mention such a feature.
  - syrak 2y ago
    Thanks! Here we go: "Note: In versions of Miranda before release two (1989) it was possible to associate "laws" with the constructors of an algebraic type, which are applied whenever an object of the type is built. For details see Turner 1985, Thompson 1986. This feature was little used and has since been removed from the language. "
    - derriz 2y ago
      Cool - mystery solved!
    - 082349872349872 2y ago
      fwiw I unwittingly retrod this path; looking back at early versions of my algebraic type library there were all sorts of provisions for automatic smart constructors (commutativity, identities, etc., surely inspired by Goguen) that got dropped from later versions for lack of use.

kragen 2y ago

i'd forgotten that clu had pattern matching! it's interesting and surprising that full-fledged adts come from hehner's universal algebra

burakemir 2y ago

Let's define a mapping F to act as a "signature-step" of an algebraic data type with operations op as a map (functor) from X to Sum_op X^arity(op). This involves a sum of products (or coproduct of products). See "Recursive types for free" https://homepages.inf.ed.ac.uk/wadler/papers/free-rectypes/free-rectypes.txt https://homepages.inf.ed.ac.uk/wadler/papers/free-rectypes/f...