StackOverflow has a bunch of nonsense about inductive types allowing for dependency while ADTs do not, but that's not a property of inductive types, that's a property of the particular languages they exist within
Conversation
I conclude that ADTs are inductive types in other type systems but the communities gave them different names for weird reasons. ADTs in practice come with limited recursors but that also isn't fundamental
3
7
I mean ADTs in the Haskell sense, the term seems to be broader in PL, making things even more confusing
4
5
i think "ADT" roughly means "you can define types by A = p(A) for p a polynomial" with some variation on what p can look like, whereas "inductive type" means "you can define types with an inductive universal property"
2
What do you mean by polynomial?
1
1
something along the lines of p(X) = A + B × X + C × X² + D × X³
1
Literally with sum and product types?
2
1
Are there any ADTs that cannot be defined as inductive types? I'd guess not?
If you make the sums and products dependent, do you get something as expressive as inductive types & families, or not?
2
1
i think usually when people say "ADT", they specifically mean *non-dependent* sums and products—or at least that's what the term connotes to me
3
2
Yeah I’d had in my mind that ADTs+identity types = inductive types (aka. GADTs).