awesome post! one suggestion: following your explanation it seems like the type constructors are more responsible for determining whether it is sum or product

awesome post! one suggestion: following your explanation it seems like the type constructors are more responsible for determining whether it is sum or product type instead of the data constructors. this tripped me up when i was trying to figure out why function types didn't have a size of a * b, and instead b^a. then i remembered that Add takes the same amount of arguments as Mul in the type constructor despite it being a sum type. i would hint more that what determines the size of a type isn't the type constructor but more the different data constructors, e.g.: data T a b = Foo a | Bar a b | Baz b | Qux (a -> b) <=> T = a + a*b + b + b^a i'm already anticipating your recursive type post :) data Rec a b = One a | Two a b (Rec a b) | Three b <=> T = a + a * b * T + b T - T * a * b = a + b T * (1 - a * b) = a + b T = (a + b) / (1 - a * b) ... in haskell's ADT's how do you get the inverses of a type? then we could solve for the size of the recursive type Rec a b.