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)_ZFC}| >_ZFC |N|
|{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!

Region, Effect and Closure Inference, Part 2

Part 1

Michael Stone was correct in his comments to part 1. Ben Lippmeier elaborated to me in an email:

In those slides,
(%) is the kind of regions.
(!) is the kind of effects.
($) is the kind of closures.

The symbol represents the kind, as well as the name space of the R/E/C variables.
…
I don't have a paper for this stuff at the moment, it's still under development - but the type system is based on some other work that has been around for a while:
The Type and Effect Discipline
Jean-Pierre Talpin, Pierre Jouvelot

Polymorphic Type, Region and Effect Inference
Jean-Pierre Talpin, Pierre Jouvelot

Polymorphic type inference and assignment
(For the closure typing)
Xavier Leroy

The type system is a merge of the ones described in the above two papers, but with some extra stuff added on to make it practical to use in a real compiler.

Ordinals, part 2

Part 1

Peter G. Hancock reminded us of the obvious way to define uncountable ordinals. A rough translation into a single data type, rather than a family:

data Ordinal n = Zero (Nat n)
               | Succ (Ordinal n)
               | forall t . Limit (Less t n) (Ordinal t -> Ordinal n)

The parameter n is the "class" of the ordinal. We need the helper definitions:

data Nat n where
    Z :: Nat Z
    S :: Nat n -> Nat (S n)
data Z
data S n

data Less a b where
    LessZ :: Nat b -> Less Z (S b)
    LessS :: Less a b -> Less (S a) (S b)

embed :: Ordinal n -> Ordinal (S n)
embed (Zero x) = Zero (S x)
embed (Succ x) = Succ (embed x)
embed (Limit e f) = Limit (onemore e) (embed . f)
    where
      onemore :: Less a b -> Less a (S b)
      onemore (LessZ x) = LessZ (S x)
      onemore (LessS p) = LessS (onemore p)

Then we can define the first uncountable ordinal as

omega_1 = Limit (LessS (LessZ Z)) embed

and the sequence of ωs up to ω_ω as

omega_n :: Nat n -> Ordinal n
omega_n Z = Zero Z
omega_n (S n) = Limit (plusone n) embed
    where
      plusone :: Nat n -> Less n (S n)
      plusone Z = LessZ Z
      plusone (S n) = LessS (plusone n)

Hancock has many other interesting ways to represent ordinals, including as surreal numbers (with code), in which we can provide a more precise answer the the question I was originally responding to, What happens when you divide infinite by two? In the case of surreal numbers, you get, simply, ω/2, just as you do with the hyperreals. Hancock also provides a datatype for the ordinals up to Γ₀ without resorting to embedded functions, which means we can do things like computably compare them.

Compiler Proof of Referential Transparency

Programs in languages with mutation can make optimizations that Haskell programs can't, at least not without compiler magic, unsafePerformIO, or wrapping return types in the IO monad. Simple examples that spring to mind are memoization and splay trees. Here, operations that should have no semantic effects (calling a fib function or doing a find on a splay map) do have actual effects. It would be nice if Haskell programmers could write these optimizations and prove them safe with the type system, then use these functions as if they were referentially transparent.

My idea for this a few months ago was to use quotient types, since quotient types equate two actually different things that are functionally the same under some view. A Fibonacci function with a memoization table up to 100 looks the same to a caller as one with no memoized values at all, so they are equal under some quotient.

Other things came up, and I put off this idea for a while, and I have now seen a really cool way for Haskell programmers to deal with local effects. Ben Lippmeier's talk at the SAPLING June 2007 meeting (talk summary) explains region and effect inference for Haskell-like languages without sacrificing referential transparency or having to use the IO monad. This insight wouldn't solve the splay tree issue, because reading a splay tree does modify data that is not local to the reading function, though that modification should be opaque to clients.

I can't wait to see the full paper(s) and the implementation. Until I can, I'll have to settle for the slides from an earlier talk with more motivation.