
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.
Data types consist only of computable elements. Since there are only countably many computable functions, 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