|
|
|
|
|
|
by jonlong
686 days ago
|
|
|
"Free algebra" here comes from universal algebra/category theory, which is quite distinct from the "free algebra" of ring theory (having nothing in particular to do with sums and products). Unfortunately "algebra" might be the most overloaded term in mathematics. (The article says in the second paragraph: "the name comes from universal algebra". The wiki article you linked disambiguates itself with universal algebra right at the top.) "Algebraic data type" in this sense is synonymous with "inductive data type". The values of an algebraic data type do not form a free ring or any ring. You cannot generally add or multiply them. You may write a particular type with constructors intended to serve this purpose, but the laws defining a ring will not hold. A separate fact is that types (not their values) belong to a free semiring "up to isomorphism" (where sum and product are the categorical coproduct and product). It is this fact that seems to have been conflated with the "algebra" of "algebraic data types". The disambiguation of this with the sense from universal algebra is the very purpose of the article. |
|
|
Also, you have to love this introduction:
> If we can have electronic music, why not electronic category theory? 'Music has charms to soothe the savage breast', said Congreve Has category theory less charm? Can we not make the electrons dance to a categorical tune?
You have to love his whimsy.
I've been playing with lately Maude (Based on OBJ and Clear) and it really seems like the motivation for algebraic data types has been about driving categorical algebras / universal algebras from the beginning. At some point it clicked how it felt like I was defining categories (modules), objects (sorts) and morphisms (ops) and then adding constraints writing equations.
I don't know Maude or category theory well enough to say it qualifies as an "electronic category theory" for some defined set of categories (small?), but I can see that vision, and how it's a little disappointing this vision isn't better understood.
FYI, Burstall sought out Jim Thatcher from the ADJ group and Thatcher, who referred Burstall to Goguen (Thatcher was focused on stopping the Vietnam war), who was the ADJ group's practicing logician / category theorist. From what I read, the reason Goguen was even at the ADJ group in the first place is MacLane recommended him for the position while Goguen was studying under him in Chicago.
When you consider the timeline in 1977 when Burstall/Goguen first met. They figured out the semantics for this language very quickly, define institutional model theory, which formalized a minimal definition of "what is a logic?" and then used that as the basis for creating Clear, which inspired Burstall's Hope and Goguen's OBJ.
The fact that they did all that in such short order is very telling (IMO) for how long they had been each been concocting schemes to get universal algebras and category theory into computer science.
https://link.springer.com/chapter/10.1007/BFb0022493