One observation from talking to industrial teams: PL has a lot of cool concepts that get lumped together into the same language or community, and industrial language designers then need to decouple them from features they don't want
Conversation
As an example, it seems like most people who want dependent types for practical programming actually don't care about soundness too much, they just want a helpful and very natural annotation system, basically
4
16
And inductive types, someone asked me if these had ever been implemented outside of a proof assistant, and how they differ from ADTs fundamentally (not just in terms of implementation, which I know), and I didn't really know the answer
1
5
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
1
4
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
Replying to
Do you mean how 'ADT' also sometimes refers to 'Abstract Data Types', which is a different thing to 'Algebraic Data Types'?