[gugagore]

FYI the use of "subtype" here does not, as far as I know, have much connection to the concept in class-based object oriented programming languages.

https://lean-lang.org/doc/reference/latest/Basic-Types/Subty...

A crucial difference between type theory (as its known in Lean) and set theory is that an inhabitant/element is of exactly one type.

[ImprobableTruth]

Caveat: Coercions exist in Lean, so subtypes actually can be used like the supertype, similar to other languages. This is done via essentially adding an implicit casting operation when such a usage is encountered.

[codethief]

I'm not quite following. According to the OP and the docs you linked, a subtype is defined by a base type and a predicate. In other words: You can view it as a subset of the set of elements of the base type. That's pretty much the standard definition of a subtype.

Object-oriented programming languages are not that different: The types induced by classes can easily be viewed as sets: A child class is a specialized version of its parent's class, hence a subtype/subset thereof if you define all the sets by declaring `instanceof` to be their predicate function.

[nickpsecurity]

B. Meyer made an attempt to formulate many concepts in programming using simple, set theory. It might help in discussions like this. I say might since I'm not mathematically-inclined enough to know for sure.

https://bertrandmeyer.com/2015/07/06/new-paper-theory-of-pro...

[SkiFire13]

> 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.

[codethief]

> 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.

[gugagore]

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.