Size-indexed `count`
Closed this issue · 1 comments
byorgey commented
Should we make a version of count
that counts parameterized types by size, i.e. countBySize : (Type -> Type) -> (N -> N)
? For example, suppose we define type T(a) = Unit + a * T(a) * T(a)
. Then count(T)
(once we implement #175 ) would unhelpfully just say infinity. But countBySize(T) : N -> N
could produce the Catalan numbers (presumably).
byorgey commented
Note that currently, we do not even allow writing T
by itself, and we don't have kinds like Type -> Type
. So some bigger changes would be needed to support this. I'm not sure it would really be worth all those changes just to support this, so I will close it for now.