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 ?

CodePudding user response：

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.

CodePudding user response：

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...)