Countable Ordinals in Haskell

In Haskell: What happens when you divide infinity by 2?, Eric Kidd asks:

...
2. Is it possible to represent any other (more interesting and/or more correct) definitions of infinity in Haskell?
3. What’s the best way to think about the infinite ordinals?

The code below is my answer to those questions for countable ordinals only. I'm not sure if it makes sense to talk about representing uncoutable sets on the kind of computers we have now: We can talk about infinite countable sets as computable limits of finite objects, but what would an uncountable set look like? They can't be objects of Nat -> Bool, since every object of this type is represented in some finite number of bits. It seems like we are stuck in a universe where Goedel's V=L is true.

{-# OPTIONS_GHC -fglasgow-exts #-}

{- See:
  http://en.wikipedia.org/wiki/Ordinal_arithmetic
  http://en.wikipedia.org/wiki/Large_countable_ordinals

  To add later:
  http://citeseer.ist.psu.edu/487179.html
-}


module Countable where

data Finite = Z
           | S !Finite

{- A countable ordinal is 0, a successor, or a limit of a countable
  sequence. This definition is weak, as the countable sequence should
  be strictly increasing, but that's hard to express. One way to do so
  would be to interpret (Limit f) as the limit of
  (sum i = 0 to n) (1 + f i). Note: this addition is not commutative.
  This would complicate things, however, so I'll leave it for a later
  extension.
-}
data Ordinal = Zero
            | Succ !Ordinal
            | Limit (Finite -> Ordinal) deriving (Show)

{- I believe that there is no computable Eq or Ord instance for Ordinals.
  Comments?
 
  We make an approximation here by taking the nth value of the limit.
  This calculation is very slow, and, of course, will equate a lot of
  ordinals that are not actually equal.
-}

nth :: Ordinal -> Finite -> Integer
nth Zero _ = 0
nth (Succ x) n = 1+(nth x n)
nth (Limit f) n = nth (f n) n

instance Show (Finite -> Ordinal) where
   show f = show [f Z,
                  f (S Z),
                  f (S (S Z)),
                  f (S (S (S Z)))]

instance Eq Ordinal where
   x == y = (show x) == (show y)

{- The basic ordinal arithmetic. Addition and multiplication are not
  commutative.
-}
addOrdinal :: Ordinal -> Ordinal -> Ordinal
addOrdinal x Zero = x
addOrdinal x (Succ y) = Succ (addOrdinal x y)
addOrdinal x (Limit y) = Limit (\z -> addOrdinal x (y z))

multiplyOrdinal :: Ordinal -> Ordinal -> Ordinal
multiplyOrdinal x Zero = Zero
multiplyOrdinal x (Succ y) = addOrdinal (multiplyOrdinal x y) x
multiplyOrdinal x (Limit y) = Limit (\z -> multiplyOrdinal x (y z))

expOrdinal :: Ordinal -> Ordinal -> Ordinal
expOrdinal x Zero = Succ Zero
expOrdinal x (Succ y) = multiplyOrdinal (expOrdinal x y) x
expOrdinal x (Limit y) = Limit (\z -> expOrdinal x (y z))

-- The first infinite ordinal
finite :: Finite -> Ordinal
finite Z = Zero
finite (S x) = Succ (finite x)

omega = Limit finite

-- Apply a f some number of times, starting at z
apply Zero f z = z
apply (Succ n) f z = f (apply n f z)
apply (Limit g) f z = Limit (\x -> apply (g x) f z)

-- With apply, we have more succinct definitions of arithmetic
addOrdinal' x y = apply y Succ x
multiplyOrdinal' x y = apply y (flip addOrdinal x) Zero
expOrdinal' x y = apply y (flip multiplyOrdinal x) (Succ Zero)

-- Enumerates the fixed points of a function.
fix Zero f = apply omega f Zero
fix (Succ n) f = apply omega f (Succ (fix n f))
fix (Limit g) f = Limit (\x -> fix (g x) f)

-- Some larger ordinals:
epsilon n = fix n (expOrdinal omega)

-- The Veblen heirarchy:
veblen Zero b = expOrdinal omega b
veblen (Succ a) b = fix b (veblen a)
veblen (Limit a) b = Limit (\x -> veblen (a x) b)

-- Feferman-Schutte ordinals
gamma n = fix n (flip veblen Zero)