Definability and Continuity
In How Many Functions are There of Type Bool -> Bool?, I stated "The trick is to remember that if f is continuous, then f _|_ =/= _|_ implies that for all x, f x = f _|_". That is false. It would have been true had I said "… remember that if f is definable in Haskell, then …". The correct statement for continuous functions is: for all x, f x ≥ f _|_. The "≥" here is that used in domain theory to talk about CPOs.
In addition to only considering functions definable in Haskell, I was also only considering flat CPOs, in which each element is comparable only to itself and _|_. An example of a CPO that is not flat:
data Wrap = Wrap Unit data Unit = Unit
In the CPO Wrap_|_, _|_ < Wrap _|_ < Wrap Unit. Though Wrap_|_ has three values, just like Bool_|_, there are only nine functions (continuous or definable in Haskell) of type Wrap_|_ -> Bool_|_. Furthermore, there are eleven continuous functions of type Wrap_|_ -> Wrap_|_, and all are definable in Haskell. (Thanks to Stefan O'Rear for pointing that out).
Clearly, the codomain isn't treated opaquely as it was in the last post: in order to count functions, we need to know the ordering on the codomain.
I have some more thinking to do about counting, continuity, and definability before I can make any more assertions about the cardinality of function types.
Update:
Stefan O'Rear pointed out an error in which I claimed certain functions were not definable in Haskell, when they actually are. A better example of a function that is continuous but not definable in Haskell is:
parallel_or _ True = True parallel_or True _ = True parallel_or False False = False
No comments:
Post a Comment