[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