I find the dividing line in formalism; we can always find similarities with language-level features from OO, but OO is by definition an informal set of ideas ab

I find the dividing line in formalism; we can always find similarities with language-level features from OO, but OO is by definition an informal set of ideas about how programming is best done and understood, rooted deeply in empiricism, not formal theory and analysis. If I can model your type/language model as a higher-kinded dependently typed lambda calculus (e.g. using Boehm-Berarducci encoding for non-turing complete recursive ADT definitions), then it's not OO -- it's functional programming, rediscovered.