Andrew Bromage wrote:
[*] Theoretical nit: It's not technically a "set".
Consider the data type:
data Foo = Foo (Foo -> Bool)
This declaration states that there's a bijection between the elements of Foo and the elements of 2^Foo, which by Cantor's diagonal theorem cannot be true for any set. That's because we only allow computable functions, and Foo -> Bool is actually an exponential object in the category Hask.
I wrote:
Data types consist only of computable elements. Since there are only countably many computable functions,
What I meant by that is that there are only countably many lambdas, and we can define a "computable value" as a lambda. The classical definition of "general recursive function" refers to functions in Integer -> Integer to begin with, so there can only be countably many values by construction.
every data type has at most countably many elements. In particular, it is a set.
The least fixed point under these restrictions is not a bijection between Foo and 2^Foo. It is only a bijection between Foo and the subset of computable 2^Foo.
-Yitz