Earlier quoted context omitted.
Data encapsulation (e.g. via ADTs) does not equal "OO".
I would argue that OO is polymorphism + innate object identity. Though the latter only matters if you have mutability; but then, whether OO without mutability is "true OO" is one of those deeply philosophical questions.
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.