[Haskell-cafe] Basic question concerning data constructors
gale at sefer.org
Tue Jan 1 10:43:18 EST 2008
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,
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
> 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.
More information about the Haskell-Cafe