3 ms·

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

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.

SkiFire13 1y ago
> 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 1y ago
  > 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 1y ago
    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.
nickpsecurity 1y ago
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-programs/ https://bertrandmeyer.com/2015/07/06/new-paper-theory-of-pro...

SkiFire13 1y ago

> 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 1y ago
> 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 1y ago
  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.

nickpsecurity 1y ago

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-programs/ https://bertrandmeyer.com/2015/07/06/new-paper-theory-of-pro...