I'm very sorry to say this, but… a category theory perspective points out a way in which they're not "sufficient". The exponential in a category theory context

I'm very sorry to say this, but… a category theory perspective points out a way in which they're not "sufficient". The exponential in a category theory context is basically "like a set of functions", in the same way that the product in a category theory context is "like a set of tuples". The fact that the notions are distinct means that functions are one example of an extremely important concept which is "not an ADT". Category theory has a wealth of other concepts which suggest more general non-ADT properties, too. For example (ignore the jargon): * Finite limits are a generalisation of finite products (i.e. the ADT product type), where we additionally require intersection types. * Finite colimits are a generalisation of finite sums (i.e. the ADT union type), where we additionally require quotient types - and I'm not aware of any language, other than maybe Lean and friends, which has user-space quotients! Think of trying to define the rational numbers in user-space, but without forcing the user to deal with normalisation.