disco-lang/disco

Size-indexed `count`

Closed this issue · 1 comments

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).

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.