Cardinality of the untyped lambda calculus embedded in Haskell

Question

Haskell accepts the definition of the following type

data Lam = Func (Lam -> Lam)

which intends to represent untyped lambda-terms. For example, Church's booleans are in this type

trueChurch :: Lam
trueChurch = Func (\x -> Func (\y -> x))
falseChurch :: Lam
falseChurch = Func (\x -> Func (\y -> y))

The constructor Func :: (Lam -> Lam) -> Lam has this inverse function

lamUnfold :: Lam -> (Lam -> Lam)
lamUnfold (Func f) = f

and those two functions define a type isomorphism between Lam -> Lam and Lam. This is surprising when we look at the cardinals (the sizes) of those types. Because of the Church booleans above, the cardinal of Lam is at least 2, so there are more elements in Lam -> Lam than in Lam -> Bool. The latter is the type of subtypes of Lam, i.e. the powerset of Lam, and by Cantor's theorem it already has much more elements than Lam does. How does the existence of type Lam not violate Cantor's theorem ?

Part of the answer might be in domain theory. If I understand correctly, the elements of Lam -> Lam would not be all set-theoretic functions (which are bigger than Lam by Cantor's theorem), but only continuous functions. If so, what is the topology that defines this continuity, and why are Haskell terms of type Lam -> Lam continuous for it ?

Answer 1

Probably the simplest way to resolve the paradox is to observe that not every (set-theoretic) function is representable as a lambda term.

Every valid lambda term can be obtained by choosing a finite number of grammar productions from an at most countable set and applying them at most finitely many times. As such, the set of all lambda terms is a countable union of countable sets, and therefore it is itself countable.⁰ The argument transparently applies to the Haskell type: the only way to obtain terms of type Lam is to invoke the constructor, and at any given point in time, even if your program doesn’t terminate, the constructor may have been invoked only a finite number of times. As such, during its whole execution, the program may encounter at most countably infinite number of different Lam values. In practice, given that computer memory is finite, the number of terms your programs will actually be able to manipulate will be a little smaller.

Set-theoretically, nothing stops you from considering a bit string obtained by tossing a coin a countably infinite number of times to be a valid function ℕ → 𝟐: it satisfies the set-theoretical definition of a function, since it assigns exactly one element of the codomain (the result of the coin toss) to each element of the domain (the position in the bit string). But given that constructing such a function requires making an infinite number of arbitrary choices¹, it has no corresponding lambda term.

(More formally: add a symbol f to the language of ZFC, and for each natural number n, randomly choose one of ‘f(n) = 0’ or ‘f(n) = 1’ as an axiom. If we pick a finite subset of axioms defining f, it is obviously consistent with ZFC that a function satisfying that finite subset exists. By the compactness theorem, it is consistent with ZFC that a function f satisfying all the axioms exists.)

There is no need to invoke complicated concepts like continuity. All the above follows just from considerations of cardinality itself while paying attention to where lambda terms (and type terms in Haskell) come from.

---

⁰ This is technically false if you start with an uncountable set of symbols for variables. But even then, you can choose a countably infinite subset of lambda terms to which every lambda term in the full set will be α-equivalent. The issue also disappears if you use de Bruijn indices instead of variable symbols.

¹ Assuming the coin tosses are truly nondeterministic and independent, of course.

Answer 2

If I understand correctly, the elements of Lam -> Lam would not be all set-theoretic functions (which are bigger than Lam by Cantor's theorem), but only continuous functions.

Yes, that's a common answer to the apparent paradox.

More in general, types are types, with their logical theory (type theory), while sets are sets (working as in set theory).

One is tempted to interpret types as sets, i.e. to constructs models of the lambda calculus within sets.

I suggest you read the milestone paper "Polymorphism is not set theoretic" by Reynolds. This shows that is you have "forall" types as in System F, and you interpret functions as sets in the "obvious" way, you get a contradiction, by a similar argument you made (Cantor's, roughly). Indeed, Reynolds constructs T ~= (T -> Bool) -> Bool.

Reynolds suggests indeed, one of the option is to interpret function types as a "subset" of functions on sets, e.g. continuous functions as you mentioned.

If so, what is the topology that defines this continuity

Scott topology.

and why are Haskell terms of type Lam -> Lam continuous for it ?

Roughly, because all the basic operations (lambda abstractions, applications, ...) are continuous, so you get a composition of continuous operators which has to be continuous.

Note that defining a proper formal semantics of Haskell is a daunting task. Even focusing on System F only, which is much simpler in comparison, models are already rather complex.

You could start from the simply-typed lambda calculus and learn about their categorical models: Cartesian closed categories (CCCs). Working in, say, the category of Scott-continuous functions is a special case of CCC. The CCC general structure makes you understand that, after you have a basic structure (essentially Currying and little else) you can use that to create a full-model, interpreting any (typed) lambda term.

Answer 3

I'm not convinced there's much merit resolving this with notions of Scott continuity. Haskell doesn't have the kind of formal semantics that would be required for these mathematical arguments. There is a bit of a philosophical war on whether this means Haskell is broken or rather theorists keep overthinking stuff, to put tongue-in-cheek. IDK.

Some issues showing that the Cantor argument just doesn't grip here:

• Arguably, Lam has in fact only cardinality 1, because there's no way you could actually distinguish two values. The only thing you can possibly do with x :: Lam is to apply the contained function to another y :: Lam to get... yet another z :: Lam. Sure, all these may have different code and runtime etc., but they're all equivalent in terms of you never get any Haskell values that would have observably different WHNF or something like that.
  This doesn't exactly settle the discussion because you could readily add another constructor and make a similar argument, but it won't be quite as simple.

• Haskell functions are not in fact functions, specifically they're not total. I could also write an “isomorphism”

  f :: Bool -> Maybe Bool
  f False = Just True
  f True = Just False
  
  f' :: Maybe Bool -> Bool
  f' (Just False) = True
  f' (Just True) = False
  f' Nothing = f' Nothing
  

  Good luck finding an x such that f (f' x) terminates with a value not equal to x. (Of course it just won't terminate at all for x = Nothing, but now good luck solving the halting problem...)