disco icon indicating copy to clipboard operation
disco copied to clipboard

Size-indexed `count`

Open byorgey opened this issue 2 years ago • 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).

byorgey avatar Mar 19 '22 14:03 byorgey

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.

byorgey avatar Mar 28 '23 17:03 byorgey