[didibus]

I actually think this is a great little series of articles.

Something I've found confusing with algeabric data types is the fact that they are not mathematical concepts. They originate as a programming construct and were invented as part of a programming language. They were then given a name that makes it sounds mathematical, but it was just an attempt at giving some kind of metaphorical meaning to them. Same as if I name a search engine Odin, because Odin was the God of wisdom. But if you thought it had anything to do with Norse mythology you'd similarly get confused.

People tried to find correspondence for them with mathematical theories. Thus, in Set theory they could correspond to Disjoint Unions of Cartesian Products. Or in category theory, they could correspond to Coproducts of products.

I guess you could say they came out of type theory, but I'm not sure of the history here fully. Did the extensions to simply typed Lambda calculus first came out of the theory or did it retroactively built a theory from the programming construct?

At any rate, my point is, these mathematical correspondence are very confusing. And I think it's wrong to try and understand these things from the mathematical angle unless you're a mathematician trained in one of the corresponding mathematical theories.

As such I think the article does a good job.

[cbdumas]

While I don't know the history of the term "algebraic data type", I do know that the algebraic structure of ADTs is much deeper than what this article presented. For instance this structure supports some limited notion of a derivative[1]! And purely algebraic manipulation of ADT "equations" can actually be used to generate some non-obvious results [2]. So I think it's probably wrong to say that ADTs were just "given a name that sounds mathematical".

1. https://codewords.recurse.com/issues/three/algebra-and-calcu... 2. http://www.math.lsa.umich.edu/~ablass/7trees.pdf

[didibus]

That's all true from the fact that there are real correspondences with math theories. But like, that's the whole point of applied math no? To find correspondences with other things so that we can then leverage and apply the math principles to that thing?

I'm sure there's quite many things in programming language where you can use such correspondence to your advantage, not just ADTs. But we don't teach it starting from the mathematical correspondence and then back.

To put it more simply, most programming isn't thought by first teaching learners about theoretical computer science. Generally it happens either in parallel or you learn the theory after the fact. But for some reason, when it comes to functional programming it seems most teachers want to start with teaching you the theory.

And my above point is that, even historically, it is not always true that theory came first. Often times, the construct were invented and used practically from finding solutions to concrete problems, and later a theory around it was developed. In the case of ADTs, I'm not 100% sure which came first, but I know they were first implemented in the programming language Hope. Not sure if the theory was there prior or not.

[cbdumas]

I think you might be right in this case that practical use preceded theoretical understanding but that's not really my point. Software development certainly has examples of pseudo-math (for example there was a trend a few years back to write JavaScript that could run on both the server and the client. For reasons passing understanding, this was called "isomorphic" by some practitioners). All I meant was that ADTs are not that.

[didibus]

Ah I see. I believe you are correct. The correspondence seems to hold quite well, and even the name algeabric was pretty aptly chosen in this instance.

I'd be curious to know if there's an original paper on ADTs somewhere about it.

[gowld]

What makes you say it's not mathematical?

https://math.stackexchange.com/questions/50375/whats-the-mea...

[didibus]

I actually prefer the second answer in that stack exchange, the one from Gilles. It basically says what I'm saying:

It is not that there are no mathematical correspondence, but ADTs are not constructs of any mathematical theories. There's no ADT in set theory. There's no ADT in category theory. The only place you might find them is in type theory, but that's unclear to me if that is the theory that defined them, or simply the theory used to define them mathematically after their invention in computer science. And like Gilles answer suggests, ADTs brings some concepts that complicates the mathematical formalism for them.

This is why the whole sum type and product type thing is loosy washy. You can say Java classes are product types, but they are not quite like Haskell's product types, etc. They aren't an implementation of a very well defined mathematical theory. Unlike say how Java and Haskell both have support for set theory and algebra built in.

[TheAsprngHacker]

> There's no ADT in category theory. The only place you might find them is in type theory

I wouldn't say that this is true. Category theory has a definition of product of objects, sum/coproduct of objects, terminal object (unit type), and initial object (empty type). There is a correspondence between type and category theory where a certain type theory is the internal language of a certain category: https://ncatlab.org/nlab/show/computational+trinitarianism

Product: https://ncatlab.org/nlab/show/cartesian+product

Coproduct: https://ncatlab.org/nlab/show/coproduct

Terminal object: https://ncatlab.org/nlab/show/terminal+object

Initial object: https://ncatlab.org/nlab/show/initial+object