Constructability, Uncountability, and ω-Haskell
My last post about the uncountable ordinals ended up on the programming subreddit, where someone who I think is Lennart Augustsson said:
Wow, I didn't realize you could do this. Now I have to wrap my brain around in what sense you can represent uncountable ordinals in Haskell since there are only a countable number of Haskell programs. It must be something like constructive reals...
I think he's exactly right, and I think it has something to do with V=L, models, and how many functions are definable in Haskell. I'm going out of my comfort zone on this, so please correct me if I make any incorrect or nonsensical statements. I'll use as my example the powerset of the natural numbers, which is certainly uncountable, and already definable in Haskell with
data Nat = Z | S Nat type Powerset t = t -> Bool
From the viewpoint of ZFC, there are an uncountable number of ZFC functions from the natural numbers to the booleans. From the viewpoint of Haskell, there are an uncountable number of Haskell functions from the natural numbers to the booleans. But, from the world of ZFC, the number of Haskell functions from the natural numbers to the booleans is countable: we can simply order them by their definitions lexicographically. Since every function definable in Haskell has a finite definition and the cardinality of a countable union of finite sets is countable, the function definitions of type Nat -> Bool are countable.
|{f : f <- (N -> 2)Haskell}| >Haskell |N|
|{f : f <- (N -> 2)Haskell}| =ZFC Σn <- N |all n-bit functions from N -> Bool| = |N|
From the viewpoint of Haskell, though, this can't be proven; functions are opaque, so we have no way to order or count them. This might not be true if we use some of the unsafe features of Haskell that would allow us to look at the actual assembly corresponding to a function.
We could, I suppose, imagine a programming language which was not limited to finite-length function definitions. ω-Haskell would not only have types with seemingly uncountable numbers of inhabitants, but each inhabitant would also be definable. Yuk!
5 comments:
We can also imagine having an operation of type
getNonComputableOrdinal :: IO (Ordinal A)
where the ordinal is determined, e.g., by a random process.
I don'T think I understand what you're getting at.
evilness, thats what he's getting at.
Pure, Functional, Unadulterated Evilness.
~~jfredett (Joe)
Forgive me for giving you a hard time, but I (a random mathematician) have some questions with some of your statements...
You said:
"From the viewpoint of ZFC, there are an uncountable number of ZFC functions from the natural numbers to the booleans."
Isn't that only if we accept the continuum hypothesis?
The continuum hypothesis is independent of the axioms for ZF(C)...
"From the viewpoint of Haskell, there are an uncountable number of Haskell functions [from the natural numbers to the booleans.]"
--- emphasis added
Why? Is this provable or a conjecture?
"But, from the world of ZFC, the number of Haskell functions from the natural numbers to the booleans is countable: we can simply order them by their definitions lexicographically."
Can't you implement this lexicographic ordering in Haskell?
Just curious...
'"From the viewpoint of ZFC, there are an uncountable number of ZFC functions from the natural numbers to the booleans.'
Isn't that only if we accept the continuum hypothesis?"
No. CH is about the relative sizes of aleph_1 and c. My statement is only that c > aleph_0.
"'From the viewpoint of Haskell, there are an uncountable number of Haskell functions [from the natural numbers to the booleans.]'
--- emphasis added
Why? Is this provable or a conjecture?"
It's sloppy, and possibly meaningless.
"'But, from the world of ZFC, the number of Haskell functions from the natural numbers to the booleans is countable: we can simply order them by their definitions lexicographically.'
Can't you implement this lexicographic ordering in Haskell?"
I think in ZFC as you can enumerate all constructible ZFC functions from the natural numbers to the booleans, but c is still greater than aleph_0 because ZFC by itself can't show that the enumeration is an enumeration of all ZFC functions from the natural numbers to the booleans.
I think I was trying to say that that is true of Haskell, but if you step outside, you get some extra power.
My wording was imprecise, to say the least.
Post a Comment