Just curious: what is the cardinality of an inductive data type (e.g. data T = C1 | C2 T T | C3 T) in general?

@Bubbler What do you mean by cardinality here? Are you counting only finite ones instances?

@xnor Yes, finite instances.

OK, so these are finite rooted trees where nodes have 0, 1, or 2 children, right?

I think you can get a generating function for the number of such trees with n total nodes by solving the equation T=x*(1+T+T^2) for T as a function of x, where the desired count is the coefficient of x^n

Like this, but with a slightly different quadratic: cs.stackexchange.com/a/372

Oh, interesting.

Actually, it looks like that answer also handles your class of trees at the end

I meant the size of {x|x is a finite element of T} (that is, the size of the entire infinite set).

Oh, that should just be countably infinite

One way to see this is that there's a finite number of trees of any given number of nodes

Yeah, right.

Another way to see it is that we can encode each tree as a finite string over a finite alphabet by writing out the graph of which nodes points to which node

That wasn't clear right away, but I can imagine something like a prefix notation will work