This essay says that inheritance is harmful and if possible you should “ban inheritance completely”. You see these arguments a lot, as well as things like “prefer composition to inheritance”. A lot of these arguments argue that in practice inheritance has problems. But they don’t preclude inheritance working in another context, maybe with a better language syntax. And it doesn’t explain why inheritance became so popular in the first place. I want to explore what’s fundamentally challenging about inheritance and why we all use it anyway.
As you already figured out the types are sets with a certain number of elements.
Two types are isomorphic if you can write a function that converts all elements of the first one into the elements of the second one and a function which does the reverse. You can then use this as the equality.
The types with the same number of elements are isomorphic, i.e True | False = Left | Right. For example, you can write a function that converts True to Left, False to Right, and a function that does the reverse.
Therefore you essentially only need types 0, 1, 2, 3, …, where type 0 has 0 elements, type 1 has 1 element, etc. and all others are isomorphic to one of these.
Let’s use (*) for the product and (+) for the sum, and letters for generic types. Then you can essentially manipulate types as natural numbers (the same laws hold, associativity, commutativity, identity elements, distributivity).
For example:
2 = 1 + 1 can be interpreted as Bool = True | False
2 * 1 = 2 can be interpreted as (Bool, Unit) = Bool
2 * x = x + x can be interpreted as (Bool, x) = This of x | That of x
o(x) = x + 1 can be interpreted as Option x = Some of x | None
l(x) = o(x * l(x)) = x * l(x) + 1 can be interpreted as List x = Option (x, List x)
l(x) = x * l(x) + 1 = x * (x * l(x) + 1) + 1 = x * x * l(x) + x + 1 = x * x * (l(x) + 1) + x + 1 = x * x * l(x) + x * x + x + 1 so a list is either empty, has 1 element or 2 elements, … (if you keep substituting)
For the expression problem, read this paper: doi:10.1007/BFb0019443