Hacker News Reader

> You can view it as a subset of the set of elements of the base type.

Technically speaking the elements in the supertype are all distinct from the elements in the subtype and viceversa. They are not a subset of the other, hence why it's improper to consider one a subtype of the other.

View on HN

> Technically speaking the elements in the supertype are all distinct from the elements in the subtype and viceversa.

Emphasis on "technically". The embedding is trivial. The Lean docs linked by the GP suggest to put those technicalities aside:

> Even though they are pairs syntactically, Subtype should really be thought of as elements of the base type with associated proof obligations.

Right, though the embedding is trivial, the conceptual distinction is not. In Lean, a subtype is a refinement that restricts by proof. In OOP, a subclass augments or overrides behavior. It's composition versus inheritance. The trivial embedding masks a fundamental shift in what "subtype" means.

Reply on news.ycombinator.com